Jonathan S. Shapiro wrote:
> How difficult, conceptually, would it be to introduce existential types?
Conceptually, it is not hard. But from the point of view of
implementation, I think it is a non-trivial amount of implementation.
> How much work and complexity does it add to the inference engine?
I think that the impact on type inference itself should be minimal,
because (1) All existential types must be explicitly declared
(2) The values of existential types can only be used in a way that the
abstracted type cannot be divulged or instantiated.
> Is there a syntax that you would recommend?
First, we can add extra annotations to structure declarations as in:
(defstruct pr2 (forall ('a)) fst: (ref 'a) snd:(fn (ref 'a) ()))
with the understanding that the pr2 shall only construct values that
work on any 'a.
Otherwise, we can add syntax like
(exists ('a)
(defstruct pr2 fst: (ref 'a) snd:(fn (ref 'a) ())))
similar to the syntax we now have for universal quantification:
(forall ('a)
(defstruct (pr1 'a) fst: (ref 'a) snd:(fn (ref 'a) ())))
Again similar to universal quantification, we can have constraints:
(exists ((Eq 'a) (Num 'a))
(defstruct pr2 fst: (ref 'a) snd:(fn (ref 'a) ()))).
Another formulation can be
(pack (<conxrete-type>, <expression>) as <existential-type>)
but this can be reduced to the structure declaration+construction.
Existential structures can be constructed as usual:
(let* ((fint (lambda (x:(ref int)) ())
(fbool (lambda (x:(ref bool)) ())
(p1 (pr2 (dup 10) fint))
(p2 (pr2 (dup #t) fbool))
... (== p1 p2) ... )
However, we cannot use `.' selection on such structures.
This is because one might write:
(p1.snd (begin (set! p1 p2) p1.fst))
However, we can use a match like construct which makes a copy.
(open (p p1) (p.snd p.fst))
Obviously, here also, the only useful thing we can do with p.fst is to
apply it to p.snd.
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
