如何解决如何将 Haskell 类型族转换为 Idris 类型函数?
假设我们有一些 Haskell 类型族将类型映射到其他一些类型:
data (a :: Type) :+: (b :: Type) = a :+: b
type family MapType (a :: Type) :: Type
type instance MapType Int = Integer
type instance MapType Integer = Integer
type instance MapType (a :+: b) = (MapType a,MapType b)
class HasConvert a where
convert :: Proxy a -> a -> MapType a
instance (HasConvert a,HasConvert b) => HasConvert (a :+: b) where
convert :: Proxy (a :+: b) -> (a :+: b) -> (MapType a,MapType b)
convert _ (a :+: b) = (convert (Proxy @a) a,convert (Proxy @b) b)
-- etc etc
如何为此编写 Idris 等价物?如果我开始这样写:
MapType : Type -> Type
MapType Int = Integer
然后它无法编译,因为 Idris 无法对类型进行模式匹配。 如何解决这个问题?
解决方法
取决于您的用例是什么:
data MapTypeProof : Type -> Type where
Proof0 : (a = Int) -> MapTypeProof a
Proof1 : (a = Integer) -> MapTypeProof a
Proof2 : (c = (a :+: b))
-> MapTypeProof a
-> MapTypeProof b
-> MapTypeProof c
MapType : MapTypeProof a -> Type
MapType (Proof2 _ p q) = (MapType p,MapType q)
MapType _ = Integer
MapType' : (a : Type ** MapClassProof a) -> Type
MapType' (_ ** mcp) = MapClass mcp
可以工作。调用函数看起来像:MapType Int (Proof0 Refl)
.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。