On Wed, 2008-10-08 at 11:11 -0700, Pal-Kristian Engstad wrote:
> (forall %f <= %map).
> map : (f: 'a -> 'b, List 'a) -> List 'b
>
> I'm not sure that putting the qualifier outside the function label makes
> things clearer.
> I think I would have preferred the syntax <value> : <type>, leading to:
>
> map : (forall %f <= %map).(f : 'a -> 'b, List 'a) -> List 'b
That is basically the way things are right now, and I agree that it is a
more consistent way of writing the type. I put forward the variant that
moved the "map" inside as an alternative to get a reaction.
What is a little (subjectively) weird if map is on the outside is that
(a) the forall constrains and scopes the entire type, but (b) the forall
names a variable that appears outside the forall.
> Since labels names in the type are arbitrary, you could also device a
> system where %% (for instance)
> refers to the effect type variable of the function itself, %<N> where
> <N> is the effect type variable
> of the N'th argument, and nesting through %<N>.<M>. Then you would get
>
> map : (forall %0 <= %%) . ('a -> 'b, List 'a) -> List 'b
>
Horrible. First, this is already incomprehensible (at least to me).
second, it does not generalize. consider that in some examples the
function f will in turn take a function g, and *that* function may also
require a type variable.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
