[bitc-dev] Opaque (Abstract?) types

[Sandro Magi]

My first reply doesn't seem to have gone through, so I'll try again.

Swaroop Sridhar wrote:
> 1) My understanding is that the proposal was to introduce existential
> types only, without adding first class polymorphism.

I don't believe first-class polymorphism (FCP) is necessary for the technique described. Perhaps FCP in MLF makes the use of existentials more pleasant, but I don't think it's fundamental to the approach. I could be wrong though.

> 2) My consideration (of a possible implementation) was to achieve
> scoping through an explicit match construct, with pattern instantiations
> implemented through skolem constructors as in the case of existential
> types in Ocaml-light:
> 
> http://hal.inria.fr/docs/00/07/44/88/PDF/RR-2183.pdf

In skimming it, it looks like the standard approach to existentials using skolemization, also described in "First-Class Modules for Haskell" (though the latter takes the technique a bit further), which results in the scoping difficulties previously mentioned. The FCP with Existentials paper resolves those difficulties, but since I'm not familiar with BitC's constraints, perhaps it's not a good fit for you.

Sandro