list - 编译时强制有限列表

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

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

问题在于它不是一个单一的列表类型，而是一类类型，每个列表大小都有一个。例如，如果我想写一个版本 take或 drop在这个列表中，我需要开始一些严肃的依赖类型。

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

这可以做到吗？

Answer 1

这可以通过提供终止检查的 Liquid Haskell 来完成。
类型签名在 Liquid Haskell 中如下所示:

{-@ (function name) :: (refinement) [/ (termination metric)] @-}

终止度量是一个整数向量，应该减少每个递归调用(字典顺序)。如果未指定，LH 将使用第一个整数参数作为终止度量。
可以使用惰性注释禁用终止检查 {-@ lazy (function name) @-} :

{-@ lazy inf @-}
inf x = x : inf x