[bitc-dev] Opaque (Abstract?) types
naasking at higherlogics.com
Fri Jan 25 21:14:46 EST 2008
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:
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.
More information about the bitc-dev