On Jan 7, 2008 1:37 AM, Simon Peyton-Jones <[EMAIL PROTECTED]> wrote: > Sadly, it's not true in Haskell, is it? > (error "urk") : [] > also has type (forall a. [a]).
It is a bit sad, but I think that's The Curse of The _|_, which infects any attempt to add static assurance. > It's nicer if static properties have static witnesses, and involve no runtime > activity. Maybe The Curse doesn't infect everything. What methods of assuring static properties in GHC have static witnesses? I think no: GADTs, lightweight static capabilities, forall a . [a] trick, nested/non-regular types I think yes: associated types, class constraints > You have a type (NonEmpty (NonEmpty a)). If you expand that out, I think you > get a > forall n1. List (forall n2. List a n2) n1 > So you're instantiating the element type of the outer list with a polytype, > which requires impredicativity too, not just existentials! It's true, but that seems to work without a hiccup right now Jim _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
