idris - 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)
那么,是否有可能让 Idris 理解(并检查),即target c
总是Convertible
,只要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
推荐阅读
- command-line - 别名目录减一个文件
- python - 无休止的while循环和旧的删除代码(弹出)......很好“弹出”。
- angular - 如何写入圆环图中心的空白区域
- django - 将 XML 选项添加到 Django Admin 上的导出选项
- echarts - 如何动态更新 echarts 绘图主题
- c++ - 带有模板的构造函数专业化
- java - 使用数组作为存储过程调用的输入 throw Java
- python - 在 python 中使用 sklearn 自己的估计器进行网格搜索 CV
- c# - Chrome cookie 不是最新的
- java - 如何使用 Maven 在测试范围内设置环境变量?