Starting from Jeffrey R. Lewis' <[EMAIL PROTECTED]> wish to
let partial type declarations express binding of SOME type variables
> > foo :: C a => a -> _b
and modulating the syntax proposed by Claus Reinke <[EMAIL PROTECTED]>,
> > foo :<= C a => a -> b
I suggested the following notation to express this desire:
> foo2 :<= forall b => C (a b) => (a b) -> b
This can also be seen as syntactic sugar
for an assertion that can be checked at compile-time
(a type judgement assertion):
> assert (exists a => foo2 :: forall b => C (a b) => (a b) -> b)
This way we get even closer to existing syntax,
although it is of course a departure from
the original intention of Koen Claessen <[EMAIL PROTECTED]>
to hide subtleties of Haskell's type system from DSL users.
So building on such an explicit assertion syntax,
we might easily adapt some variation of any of the proposals as syntactic sugar.
Nevertheless, I think that the distiction between
> assert (exists a => foo1 :: forall b => C a => a -> b)
and
> assert (exists a => foo2 :: forall b => C (a b) => (a b) -> b)
should not be blurred.
Am I too puristic here?
Cheers,
Wolfram
