是否可以在Haskell上表达(Type,Value)对的类型？

Question

(类型,值)对的列表可以在Idris上表示为:

data List : Type where
  Cons : (t : Type ** t) -> List -> List
  Nil  : List

example : List
example = Cons (Nat ** 3) (Cons (Bool ** True) Nil)

在Haskell上表达这些语法的语法是什么？

Answer 1

请注意,如果构造此类List,则无法对元素执行任何操作,因为您无法对类型进行模式匹配.

然而,在Haskell中它是完全可能的 GADTs

data List where
    Cons :: t -> List -> List
    Nil  :: List

example :: List
example = Cons (3 :: Int) (Cons True Nil)

您可以使用约束扩展它,例如,Typeable这样您就可以获得运行时类型信息来对列表中的元素执行操作:

data CList (c :: * -> Constraint) where
    CCons :: Typeable t => t -> List c -> List c
    CNil  :: CList c

exampleC :: CList Typeable
exampleC = CCons (3 :: Int) (CCons True CNil)

或者你可以使用 HList

data HList (xs :: [*]) where
    HCons :: x -> List xs -> List (x ': xs)
    HNil  :: '[]

exampleH :: HList '[Int, Bool]
exampleH = HCons 3 (HConst True HNil)

特别是依赖对(或者总和!)(Idris docs)在Haskell中是可能的,但是我们必须为函数创建一个GADT!该http://hackage.haskell.org/package/dependent-sum是一个许多用

如果Idris版本是

data DPair : (a : Type) -> (P : a -> Type) -> Type where
   MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P

Haskell在以下情况下差别不大a = Type:

data DPair (p :: * -> *) where
   MkDPair :: p a -> DPair p

并p用a编码GADT.在上面的例子中,它被切成了定义.

您还可以使用除类型之外的其他内容作为第一个元素.但是你必须阅读有关 单身人士的内容.