[Haskell-cafe] Finite but not fixed length...

[Brent Yorgey]

On Wed, Oct 13, 2010 at 12:13:29PM +0400, Eugene Kirpichov wrote:
> Hm. This is not actually an answer to your question, just a
> "discussion starter", but still.
> 
> The code below typechecks, though actually it shouldn't: there's no
> type "n" such that "ones" is formed by the FL from some value of type
> List Int n.
> Or should it?
> 
> {-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-}
> module Finite where
> 
> data Zero
> data Succ a
> 
> class Finite a where
> 
> instance Finite Zero
> instance (Finite a) => Finite (Succ a)
> 
> data List a n where
>   Nil :: List a Zero
>   Cons :: (Finite n) => a -> List a n -> List a (Succ n)
> 
> data FiniteList a where
>   FL :: (Finite n) => List a n -> FiniteList a
> 
> nil :: FiniteList a
> nil = FL Nil
> 
> cons :: a -> FiniteList a -> FiniteList a
> cons a (FL x) = FL (Cons a x)
> 
> list123 = cons 1 (cons 2 (cons 3 nil))
> 
> ones = cons 1 ones -- typechecks ok

Fascinating.  Doing

  ones' = Cons 1 ones'

of course does not typecheck (as expected) with an occurs check error
(can't unify n = S n).  But

  ones = cons 1 ones

does typecheck.  And it makes sense: I can see why cons has the type
it does, and given that type for cons this definition of ones is
perfectly well-typed.  But the upshot, which I had never considered,
seems to be that existentially quantified types are allowed to be _|_.

-Brent