Rank-2 polymorphism and pattern matching
jbapple+ghc-users at gmail.com
Mon Jan 7 05:09:21 EST 2008
On Jan 7, 2008 1:37 AM, Simon Peyton-Jones <simonpj at microsoft.com> 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
More information about the Glasgow-haskell-users