Jeffrey R. Lewis" <[EMAIL PROTECTED]> wrote:
>
> Anyway, the only thing missing now in the above proposal
> is a similar flexibility with contexts.
> Say, you want `b' to be a bound, and thus use :<=,
> but you want the context to be exact
> (i.e. you don't want extra context elements to be allowed).
> I can't think of any particularly compelling notation for
> "the context is `C a' and no more".
> In this case, the combination of allowing `...' to extend contexts,
> and _a (or similar annotation) for unquantified type variables seems
> more natural.
Getting more and more explicit,
we may well distinguish between
> assert (exists a :: * -> *,
> D :: * -> Context
> E :: * -> Context
> F :: Context
> =>
> foo3 :: (forall b :: *
> =>
> C (a b), D (a b), E b, F
> =>
> (a b) -> b))
and
> assert (exists a :: * -> *,
> D :: * -> Context
> E :: * -> Context
> =>
> foo3 :: (forall b :: *
> =>
> C (a b), D (a b), E b
> =>
> (a b) -> b))
or any other specialisations.
Now the DSL user really gets lost,
and we should consult Simon Marlow
for an appropriate layout rule for types ;-)
But the expressivity is ours ;-)
Have fun,
Wolfram
