Jonathan S. Shapiro wrote:
> I have just run into an example whose effect type I do not
> (syntactically speaking) know how to write. Consider:
>
> (define (add-one x)
> (+ 1 x))
>
> Ignoring effects, the proper type for this would be:
>
> (forall ((IntType 'a))
> (fn ('a) 'a))
>
> For effect typing, we need some way to say that the effect depends on
> the implementation of + for the particular type 'a. While the relevant
> effect variables are manifest in the declaration of IntType, it isn't
> clear how to emit them here in the type of add-one. Ignoring syntax, we
> would appear to need something like:
>
> (forall ((IntType 'a)
> ('%e (IntType 'a).+ ('a 'a) 'a))
> ('%e fn ('a) 'a))
The real type that we need to write here is:
(forall ((IntType 'a '%e))
('%e fn ('a) 'a))
where the IntType type class would be written as
(deftypeclass (IntType 'a '%e)
+: ('%e (fn ('a) 'a)))
In general, I agree with your concern that the number of type variables
introduces problems with positional correspondence here.
One solution is to say that the programmer should solve the problem for
himself by following some naming convention. For example:
;; I am ignoring the lexical restriction that effect variables cannot
;; contain +- etc
(deftypeclass (Arith 'a '%+ '%- '%*)
+: ('%+ (fn ('a 'a) 'a))
-: ('%- (fn ('a 'a) 'a))
*: ('%* (fn ('a 'a) 'a)))
which can help him remember the order of type classes.
Otherwise, we will have to introduce syntax such as
(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)))))
Now, we can produce the following translations that do not require
positional correspondence for type class arguments
(here, '%f is a fresh variable):
(Arith int32 ('%+ = '%g)) ==> (Arith int32 '%g '%f),
(Arith int32 ('%- = '%g)) ==> (Arith int32 '%g '%f),
(Arith int32 ('%- = '%g)) ==> (Arith int32 '%g '%f),
(Arith int32 ('%* = '%g)) ==> (Arith int32 '%f '%g),
(Arith int32 ('%+* = '%g)) ==> (Arith int32 '%g '%g)
> In this particular case, I actually think that it might be a good idea
> for the Arith typeclass to enforce a PURE restriction on the + operator,
> which would reduce this example to:
>
> add-one: (forall ((IntType 'a))
> (pure fn ('a) 'a))
I agree. The next best thing we can do is to require that all methods
methods of Arith have the same effect, so that the Arith type class will
require only one effect variable. My expectation is that for most type
classes, it would be sufficient for all methods to share the same effect
variable.
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
