haskell - ghc wiki、未来功能和类型列表

Question

当我遇到这个非常有趣的例子时，我正在浏览关于 TypeNats 的 GHC wiki部分。他们正在创建类型列表：

type family Get (n :: Nat1) (xs :: [*]) :: *
type instance Get Zero     (x `: xs) = x
type instance Get (Succ n) (x `: xs) = Get n xs

我想了解更多关于这方面的信息。我假设这个特性在 7.6.1 中没有实现（至少它没有为我编译），并且浏览票证被证明是相当压倒性的。知道我应该寻找什么吗？

Answer 1

这段代码在 GHC 7.6 中几乎可以正常工作——您需要打开一些扩展，并使用 ' 而不是 `（显然语法已经改变？）。这个例子编译：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

data Nat1 = Zero | Succ Nat1

type family Get (n :: Nat1) (xs :: [*]) :: *
type instance Get Zero     (x ': xs) = x
type instance Get (Succ n) (x ': xs) = Get n xs

如果您只关心类型列表，而不关心这些 TypeNat，您可能会发现这样的示例更有用：

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

如此处所述。最相关的 GHC 扩展是DataKinds，最相关的论文可能是Giving Haskell a Promotion。