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))
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))
but in the general case we are going to need to resolve this sort of
thing, and the wide reliance on type classes is going to start making
this syntax pretty awkward when the methods involved are not pure.
Suggestions on a syntax here? Problem is that it needs to be something
we can input as well as output, so that types for external procedures
can be written in interfaces.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
