Scoped type variables
ross at soi.city.ac.uk
Wed Feb 8 11:06:41 EST 2006
On Wed, Feb 08, 2006 at 11:19:41AM -0000, Simon Peyton-Jones wrote:
> I agree with the "simplest thing" plan. But if HPrime is to include
> existentials, we MUST have a way to name the type variables they bind,
> otherwise we can't write signatures that involve them. Stephanie and
> Dimitrios and I are working on this scheme:
> b) A pattern type signature may bring into scope a skolem bound
> in the same pattern:
> data T where
> MkT :: a -> (a->Int) -> T
> f (MkT (x::a) f) = ...
> The skolem bound by MkT can be bound *only* in the patterns that
> are the arguments to MkT (i.e. pretty much right away).
I see -- my scheme was overly simple. But this too feels unsatisfactory.
What if we want to give signatures for both arguments? Will the a's
be the same?
More information about the Haskell-prime