| > 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? Yes f (MkT (x::a) (f::a->Int)) = ... You can imagine that either (a) both bind 'a' to the skolem, but must do consistently; or (b) that (x::a) binds 'a', and (f::a->Int) is a bound occurrence. It doesn't matter which you choose, I think. Simon
On Wed, Feb 08, 2006 at 05:48:24PM -0000, Simon Peyton-Jones wrote:
| > 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). [...] f (MkT (x::a) (f::a->Int)) = ...
You can imagine that either (a) both bind 'a' to the skolem, but must do consistently; or (b) that (x::a) binds 'a', and (f::a->Int) is a bound occurrence. It doesn't matter which you choose, I think.
Another possibility would be to allow an optional explicit quantifier before the data constructor, mirroring the old datatype syntax for existentials: data T = forall a. MkT a (a->Int) f (forall a. MkT x f) = ...
participants (2)
-
Ross Paterson -
Simon Peyton-Jones