如何将Haskell类型族转换为Idris类型函数

Question

假设我们有一些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无法对类型进行模式匹配。如何解决这个问题？

Answer 1

根据您的用例是什么：

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)。