I started a response to Swaroop's note, and it blew up in my face quite
quickly.
I started by observing that
(forall ((Arith 'a)) TYPE)
can be viewed as a short-hand for:
(forall (+:(%e1 fn ('a 'a) 'a)
-:(%e2 fn ('a 'a) 'a)
... other methods of Arith ...
... methods of other classes ...) DEFINITION)
This is simply a variant of Swaroop's approach:
> (deftypeclass (Arith 'a '%e1 '%e2)
> (represent '%e1 ('%+ '%-))
> (represent '%e2 '%*)
> (represent ('%e1 '%e2) '%+*)
>
> +: ('%e1 (fn ('a) 'a))
> -: ('%e1 (fn ('a) 'a))
> *: ('%e2 (fn ('a) 'a))
> +*: ('%e1 (fn ('a) ('%e2 (fn ('a) 'a)))))
that does not require introduction of new syntax.
If we expand it my way, then the required effect variables become
explicit, and getting them associated properly with the right variables
in the DEFINITION becomes straightforward. Still syntactically
intrusive, but straightforward.
Then I started down a rat-hole. I started to look at ways to drop
un-referenced methods, and I came up with:
(forall ((Arith 'a)
+:(%e1 fn ('a 'a) 'a)
... methods of other classes ...) DEFINITION)
with the intended meaning that (Arith 'a) was still required, but the
only particular method of Arith 'a whose effect mattered in DEFINITION
was "+"; because only + was applied. In this view:
[ELIDED EXPANSION EXAMPLE]
(define (add-one x)
(+ 1 x))
add-one: (forall (IntLit 'a)
(Arith 'a)
+:(%e1 fn ('a 'a) 'a))
(%e1 fn ('a) 'a))
[You can start to see here why region types did not work out well in
Haskell from a syntactic point of view].
At this point I started to pat myself on the back, because this syntax
is merely very bad rather then completely horrible, and at this point
anything that is not completely horrible feels like a success.
And the reason this works, I thought to myself, is that the type class
is fully defined if all of its type variables are bound....
At which point I thought to myself: oh crap, that just isn't true. If I
define a type class:
(deftypeclass (perverse-effects 'a)
f1: ('%e1 fn ('a) bool)
f2: ('%e2 fn ('a) bool))
it is perfectly legal to instantiate this once with an impure f1 and a
pure f2, and a second time with an impure f1 and an *impure* f2. If you
do this, and if a client function uses only F1, then there is a
resolution ambiguity. Yuck. In fact, the definition above is flatly
wrong. It should properly be:
(deftypeclass (perverse-effects 'a '%e1 '%e2)
f1: ('%e1 fn ('a) bool)
f2: ('%e2 fn ('a) bool))
Now in one sense this changes nothing. The resolution ambiguity existed
already for type variables, and nothing here changes it. To the extent
that this is true, my elided expansion above captures all of the
constraints that can actually be captured.
But still, this is quite nasty, and it is going to hit particularly hard
in the area of type classes, and type classes are particularly critical
in the use of this type of language.
The particular part that is nasty is that there is no way we can drop
the method expansions even when their effect is fully determined. Going
back to my example:
(define (add-one x)
(+ 1 x))
add-one: (forall ((IntLit 'a)
(Arith 'a)
+:(%e1 fn ('a 'a) 'a))
(%e1 fn ('a) 'a))
If we update the definition with an explicit constraint, we still have
to expand the + method:
(define (add-one x)
(+ 1 x)) : (pure fn ('a) 'a)
add-one: (forall ((IntLit 'a)
(Arith 'a)
+:(%e1<pure fn ('a 'a) 'a))
(pure fn ('a) 'a))
We can only drop that %e1 if we move it explicitly into the Arith class
constraint (where it should appear in any case), because we need to
state that we require an instance of (Arith 'a) having the property that
the effect on the specified instance of + must be compatible with PURE.
We CAN drop the expansion if the purity relationship goes in the other
direction. If the arithmetic type class requires pure instance methods:
(deftypeclass (pure-arith 'a)
+: (pure fn ('a 'a) 'a)
-: (pure fn ('a 'a) 'a)
... all methods pure ...)
then we would have:
(define (add-one x)
(+ 1 x))
add-one: (forall ((IntLit 'a)
(pure-arith 'a)
+:(pure fn ('a 'a) 'a))
(pure fn ('a) 'a))
In this case, we can drop the constraint
+:(pure fn ('a 'a) 'a)
because it is redundant. Having said (pure-arith 'a) we have already
stated it.
Because of this, I am now thoroughly convinced that the core type
constraints need to be pure at all points wherever possible, and that
where this is NOT possible, a real attempt should be made to design type
classes such that those methods that DO have effect types should use the
same effect type variable wherever it is possible to do so.
On very rare occasions, I am reminded that there is a *reason* for the
use of the bokken in a kendo dojo. A bokken is a dangerous weapon in its
own right -- more than dangerous enough to demand the full care and
attention of both sensei and student. But for all of that, it is much
less dangerous than the katana. An expert can kill with either. The
difference is that a *mistake* with the katana is much more likely to be
deadly than a mistake with the bokken. And of course, it is the nature
of a dojo that it is a place for mistakes, either in the course of
learning or for the purpose of teaching.
I begin to think that effect types are more in the nature of a katana,
and that we need to treat them with caution and respect. The negative
usability implications of arbitrary effect variables on type classes are
almost enough to suggest that the compiler should reject them unless
some additional bit of syntax is used to indicate that the developer
really intends to shoot off their foot.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
