如何解决IDRIS:是否可以通过接口限制功能输出?
我正在尝试为可以(在某种意义上,与问题无关)转换为其他值的值建立接口。当前,它的定义如下:
interface Convertible c where
target : c -> Type
convert: (item: c) -> (target item)
因此,在实现此接口时,必须同时提供转换和目标类型,这可能取决于转换的值。
在现实生活中,每个转化目标也自然可以转化-例如:
implementation Convertible () where
-- This is allowed,since we're implementing Convertible for unit type right now.
target _ = ()
convert _ = ()
implementation Convertible String where
-- This is allowed,since Convertible is already implemented for unit type.
target _ = ()
convert _ = ()
implementation Convertible Double where
-- This doesn't make sense,since Integer isn't Convertible.
target _ = Integer
convert item = cast $ floor item
此外,任何可转换值都可以“包装”为提供的类型,该类型也将可转换。但是,如果转换目标本身无法转换,则会导致以下问题:
data Wrapper : Type -> Type where
-- The type should be restricted here,otherwise we'll have signature clashes
-- fromInteger here is only as an example,but the real-life case is similar
fromInteger : (Convertible c) => c -> Wrapper c
-- This works,but is extremely unergonomic,so I'd like to avoid it:
-- fromInteger : c -> Wrapper c
-- ...but with the restriction on data type,we can't implement this:
implementation (Convertible c) => Convertible (Wrapper c) where
target (fromInteger inner) = Wrapper (target inner)
convert (fromInteger inner) = fromInteger (convert inner)
错误:
test.idr:32:35-61:
|
32 | convert (fromInteger inner) = fromInteger (convert inner)
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.Main.Wrapper c implementation of Main.Convertible,method convert with expected type
Main.Wrapper c implementation of Main.Convertible,method target c constraint (fromInteger inner)
Can't find implementation for Convertible (target inner)
因此,只要target c
是Convertible
,是否有可能使Idris理解(并检查)c
始终是Convertible
?
解决方法
也许可以使用auto
和%hint
来减少样板。
interface Convertible c where
target : c -> Type
p : (item : c) -> Convertible (target item)
convert: (item: c) -> target item
implementation Convertible () where
-- This is allowed,since we're implementing Convertible for unit type right now.
target _ = ()
convert _ = ()
p _ = %implementation
implementation Convertible String where
-- This is allowed,since Convertible is already implemented for unit type.
target _ = ()
convert _ = ()
p _ = %implementation
data Wrapper : Type -> Type where
-- The type should be restricted here,otherwise we'll have signature clashes
-- fromInteger here is only as an example,but the real-life case is similar
fromInteger : (Convertible c) => c -> Wrapper c
-- This works,but is extremely unergonomic,so I'd like to avoid it:
-- fromInteger : c -> Wrapper c
-- ...but with the restriction on data type,we can't implement this:
implementation (Convertible c) => Convertible (Wrapper c) where
target (fromInteger inner) = Wrapper (target inner)
convert (fromInteger inner) = let _ = p inner in fromInteger (convert inner)
p (fromInteger inner) = let _ = p inner in %implementation
implementation Convertible Double where
-- This doesn't make sense,since Integer isn't Convertible.
target _ = Integer
convert item = cast $ floor item
p _ = %implementation
失败Can't find implementation for Convertible Integer
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。