编译时强制执行的有限列表

Question

我想制作一种表示具有有限数量元素的列表的类型。

现在最简单的方法是使用严格的评估：

data FiniteList a
  = Nil
  | Cons a !(List a)

有了这个无限列表就相当于底部。

但是，我想要一种完全阻止创建此类列表的类型。理想情况下，我希望构建无限列表的任何尝试都会导致编译时错误。

如果我使用GADTs和构建大小列表，我可以开始了解如何做到这一点DataKinds。

data Natural = Zero | Succ Natural

data DependentList :: Natural -> Type -> Type where
  Nil  :: DependentList 'Zero a
  Cons :: a -> DependentList n a -> DependentList ('Succ n) a

如果我们尝试构建类似的东西

a = Cons 1 a

我们得到一个类型错误，因为这需要一个 type n ~ 'Succ n。

问题在于它不是单个列表类型，而是一类类型，每个列表大小对应一个类型。因此，例如，如果我想编写此列表的一个版本take或drop在此列表上，我将需要开始进行一些严肃的依赖输入。

我想将所有这些单独的类型统一在一个类型下，该类型在编译时仍然强制执行有限性。

这能做到吗？

Answer 1

是的，只需使用存在式来忘记之后的有限长度：

data NonDependentList a where NonDependentList :: DependentList n a -> NonDependentList a

当然，take并且drop会有一些样板......

take :: Int -> NDL a -> NDL a
take n (NDL Nil) = NDL Nil
take n (NDL (Cons a as)) = case take (n-1) (NDL as) of
    NDL as' -> NDL (Cons a as')

但你仍然无法制作一个无限的：

ones = NDL (Cons 1 (case ones of NDL os -> os)) -- existential escapes its scope