使用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 :::

使用List就像[]你自己编写的任何类似的数据结构一样自然:

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