[Haskell-cafe] Finite but not fixed length...
Brent Yorgey
byorgey at seas.upenn.edu
Wed Oct 13 12:39:40 EDT 2010
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
More information about the Haskell-Cafe
mailing list