Compile time enforced finite lists

Question

I would like to make a type that represents lists with a finite number of elements.

Now the naïve way to do this is with strict evaluation:

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

With this infinite lists are equivalent to bottom.

However I want a type which prevents the creation of such lists altogether. I would ideally like to have any attempts to build an infinite list cause a compile time error.

I can begin to see how this might be done if I build sized lists using GADTs and 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

If we try and build something like

a = Cons 1 a

We get a type error since this requires a type n ~ 'Succ n.

The issue with this is that it is not a single list type but rather a class of types, one for each size of list. So for example if I wanted to write a version of take or drop on this list I would need to start getting into some serious dependent typing.

I would like to unify all of these separate types under a single type which still enforces finitude at compile time.

Can this be done?

Answer 1

This can be done with Liquid Haskell, which provides termination checks.
Type signatures look like this in Liquid Haskell:

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

The termination metric is an integer vector that is supposed to decrease each recursive call (lexicographical ordering). If not specified, LH will use the first integer argument as the termination metric.
Termination checking can be disabled with lazy annotation {-@ lazy (function name) @-}:

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

Answer 2

Yep, just use an existential to forget the finite length afterwards:

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

Of course, take and drop will have some boilerplate...

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')

But you still can't make an infinite one:

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

Answer 3

There's also the "ghosts of departed proofs" approach, which involves a tagged newtype with carefully exposed smart constructors, and working in continuation-passing style with continuations polymorphic in the type tag:

{-# LANGUAGE DeriveFunctor, RankNTypes, RoleAnnotations #-} 
module FinList (FinList,empty,toFinList,cons) where 
-- FinList constructor should NOT be public, or else everything breaks!

newtype FinList name a = FinList { getFinList :: [a] } deriving Functor

-- Don't allow Data.Coerce.coerce to turn FinList X a into forall x. FinList x a
type role FinList nominal representational

empty :: forall a r. (forall name . FinList name a -> r) -> r
empty f = f (FinList [])

toFinList:: forall a r. Int -> [a] -> (forall name. FinList name a -> r) -> r
toFinList n as f = f (FinList (take n as))

cons :: forall a r name'. a -> FinList name' a -> (forall name. FinList name a -> r) -> r
cons a (FinList as) f = f (FinList (a:as))

This should prevent clients of the FinList module from creating circular definitions.