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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe