相关疑难解决方法(0)

使用GHC.TypeLits,我们可以编写一个简单的类型级编号列表(或矢量).

> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, DataKinds, ScopedTypeVariables #-}

> import GHC.TypeLits

> data Vec :: * -> Nat -> * where
>   VNil :: Vec e 0
>   (:-) :: e -> Vec e n -> Vec e (n+1)

这是规范的矢量定义TypeLits.直观地说,追加操作应如下所示:

> vecAppend :: Vec e n -> Vec e m -> Vec e (n + m)
> vecAppend VNil vec = vec
> vecAppend (a :- as) vec = a :- vecAppend as vec …