haskell - 使用 Type Nats 创建类型级别列表（在类型级别添加数字时遇到问题）

Question

只是为了好玩，我想创建一个知道它有多长的类型级别列表。像这样的东西：

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

import GHC.TypeLits

data family TypeList a (n::Nat)

data instance TypeList a (0) = EmptyList
data instance TypeList a (1) = TL1 a (TypeList a (0))
data instance TypeList a (2) = TL2 a (TypeList a (1))
data instance TypeList a (3) = TL3 a (TypeList a (2))

但是，我当然想将其概括为：

data instance TypeList a (n)   = TL3 a (TypeList a (n-1))

但这会产生错误：

    TypeList.hs:15:53: parse error on input `-'
    Failed, modules loaded: none.

另一种尝试：

data instance TypeList a (n+1) = TL3 a (TypeList a (n))

还会产生错误：

    Illegal type synonym family application in instance: n + 1
    In the data instance declaration for `TypeList'

我认为这样的事情一定是可能的。绝对可以使用以下符号：

data Zero
data Succ a

但我无法用更好看的版本弄清楚。

Answer 1

类型级别的Nat改进已在 GHC 7.8 中实现，现在可以实现了！

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

import GHC.TypeLits

data family List (n :: Nat) a
data instance List 0 a = Nil
data instance List n a = a ::: List (n - 1) a

infixr 8 :::

using与您自己编写List的任何类似数据结构一样自然：[]

λ. :t 'a' ::: 'b' ::: 'c' ::: Nil
'a' ::: 'b' ::: 'c' ::: Nil :: List 3 Char

Answer 2

正如它们在 GHC 7.6 中一样，类型级别的 Nats 不会让你做这种事情。尽管名称暗示了什么，但类型0 :: Natand之间目前或多或少没有关系（不像你的and ，你可以用它做有用的事情）。这在 GHC 的未来版本中会更好。1 :: NatZeroSucc Zero