有限递归"列表"类型

Question

在Haskell中重建列表类型很容易:

data MyList a = Cons a (MyList a)
               | Empty
               deriving (Show)

someList = Cons 1 (Cons 2 (Cons 3 Empty)) -- represents [1,2,3]

这允许构建无限列表.是否有可能以某种方式定义列表类型,只允许有限(但仍然是任意长度)列表？

这里的列表示例可以替换为任何其他可能无限的数据结构,如树等.请注意,我没有任何特定的应用程序,所以没有必要质疑这个的有用性,我只是好奇是否会有可能.

Answer 1

备选方案1:具有严格尾部的列表

data MyList a = Cons a !(MyList a) | Empty

试图建立一个无限的列表肯定会导致一个底层元素MyList a.

备选方案2:存在量化的固定长度列表

data Nat = O | S Nat
data List a (n :: Nat) where
   Nil :: List a O
   Cons :: a -> List a n -> List a (S n)
data MyList a where
   MyList :: List a n -> MyList a

我会说这也不允许无限列表.

这是因为我们不能在GADT上进行模式匹配where(或者通常是懒惰模式).

-- fails to compile
test :: MyList Int
test = MyList (Cons 1 list)
       where MyList list = test

以下是太严格了.

-- diverges
test2 :: MyList Int
test2 = case test2 of
          MyList list -> MyList (Cons 1 list)

以下使得存在量化类型变量"逃避"范围case:

-- fails to compile
test3 :: MyList Int
test3 = MyList $ case test3 of
          MyList list -> (Cons 1 list)