Wolfram Kahl wrote:
> Jeffrey R. Lewis" <[EMAIL PROTECTED]> writes:
> >
> > foo :<= C a => a -> b roughly equiv to foo :: C _a => _a -> _b
> >
> > I can easily imagine that you might want some variables to be a bound, and
> > others to be exact, as in
> >
> > foo :: C a => a -> _b
> >
> > I don't think the above can be expressed with Claus' proposal.
> >
>
> You could, by being more explicit than usual:
>
> > foo :<= forall b => C a => a -> b
Glad to be shown wrong ;-) This is quite reasonable. With ::, the default for a
type variable is an implicit `forall' on the outside. With :<=, the default for
a type variable is that it is a bound (a `metavariable' in earlier posts). A
side comment. What Claus' post made clear to me is that we're not talking about
any `new' concepts here (a `metavariable' is just the usual notion of an
unquantified type variable), we're really just looking for a nice notation for
old concepts that our language doens't allow us to write down.
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.
--Jeff
