On Wed, 2008-10-08 at 14:42 -0700, Pal-Kristian Engstad wrote:
> Jonathan S. Shapiro wrote:
> >> 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.
> I agree that labels would be much preferable, since it gives semantics
> through the name of the value. But the above at least gives a canonical
> type representation that can internally for type equalities.
Perhaps, but it is not clear why any *external* representation of this
is required.
> > consider that in some examples the
> > function f will in turn take a function g, and *that* function may also
> > require a type variable.
> >
> I'm not quite sure I follow. Do you mean that labels will be shared
> within the outer function type, so that you have something like
>
> g: (f : 'a -> 'b, f: 'a -> 'b) -> 'c
>
> Not sure what that would mean exactly.
No, that is not what I meant. What I meant was that a simple linear
numbering scheme is insufficient, because arbitrary nesting needs to be
considered. In your later note to me you extended your notation to cover
that.
Overall, my comment is that positional schemes are fine for internal use
and very bad for humans.
But your question above raises an interesting issue. Consider:
(define (simple b f g)
(if b (f) (g)))
in this example, the effects of f and g get unified, so if we write the
type of simple as:
simple: (forall ((%simple >= %f)
(%simple >= %g))
(fn b:bool f:(fn -> 'a) g:(fn -> 'a) -> 'a))
we have a problem. It would be correct to write this as:
simple: (forall ((%simple < %f))
(fn b:bool f:(fn -> 'a) f:(fn -> 'a) -> 'a))
but this is undesirable, because relabeling the arguments breaks the
human intuition about the relationship between the argument names and
the parameter names. I am not sure if that is actually bad, but I
suspect that it is. Swaroop and I talked about this last night, and came
up with:
simple: (forall ((%simple >= %f)
(%f == %g))
(fn b:bool f:(fn -> 'a) f:(fn -> 'a) -> 'a))
with the intended meaning that the %f==%g records a unification without
perturbing the user-visible names. When constraints accumulate, equality
constraints get dropped, because they don't really survive in the type
once the variables involved have been unified.
shap
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
