小编Joh*_*Poe的帖子

对于某些应用程序，我需要长度为$ 2 ^ n $的向量。为了使长度与某些操作相匹配，我使用ist应用实例定义了我的类型，如下所示：

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, FlexibleContexts #-}
data Nat = Z | N Nat
data Vector n t where
  S :: t -> Vector Z t
  V :: Vector n t -> Vector n t -> Vector (N n) t

instance Functor (Vector n) where
  fmap f (S t ) = S (f t)
  fmap f (V t t') = V (fmap f t) (fmap f t')

instance Applicative (Vector Z) where
  pure = S …