什么是Haskell语法(类型级别运算符?)

Anu*_*ain 8 syntax haskell type-level-computation

是什么'[]':在Haskell代码意味着什么?一些例子 -

例1:

data OrderPacket replies where
  NoOrders :: OrderPacket '[]
Run Code Online (Sandbox Code Playgroud)

例2:

data Elem :: [a] -> a -> * where
  EZ :: Elem (x ': xs) x
Run Code Online (Sandbox Code Playgroud)

Sib*_*ibi 9

推荐列表和元组列表上的Haskell用户指南部分:

使用-XDataKinds,Haskell的列表和元组类型本身被提升为种类,并且在类型级别享受相同的方便语法,尽管前缀为引号:

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (*,*) -> * where
  Tuple :: a -> b -> Tuple '(a,b)

foo0 :: HList '[]
foo0 = HNil

foo1 :: HList '[Int]
foo1 = HCons (3::Int) HNil

foo2 :: HList [Int, Bool]
foo2 = ...
Run Code Online (Sandbox Code Playgroud)

(注意:由于中缀类型运算符(:'),HCons的声明也需要-XTypeOperators.)对于两个或多个元素的类型级列表,例如上面foo2的签名,引号可能会被省略,因为含义是毫不含糊.但是对于一个或零个元素的列表(如在foo0和foo1中),引用是必需的,因为类型[]和[Int]在Haskell中具有现有含义.

所以基本上它是以单引号为前缀的相同语法,但它在类型级别上运行.一些使用ghci上面代码的playup :

?> :t HNil
HNil :: HList '[]
?> :t HCons
HCons :: a -> HList t -> HList (a : t)
?> let x = 3 `HCons` HNil
?> :t x
x :: Num a => HList '[a]
?> let x = Tuple 3 "spj"
?> :t x
x :: Num a => Tuple '(a, [Char])
Run Code Online (Sandbox Code Playgroud)