[bitc-dev] Instance coherence: the shape of a solution
Jonathan S. Shapiro
shap at eros-os.org
Mon Apr 16 14:55:00 PDT 2012
On Mon, Apr 16, 2012 at 2:40 PM, Geoffrey Irving <irving at naml.us> wrote:
> After reading this first I was a bit queasy about "lying to the user",
> but I suppose all of that can be naturally interpreted in terms of
> convertibility relations. I.e., (x -> y) is the most general type of
> closures, and procedures and function objects are all convertible to
That's actually a very good way to look at it. In that view, some of the
other cases are subtypes and we have the option to do specialization for
This actually raises a notation question:
In type theory, we write 'b <: 'a to mean that type 'b is a subtype of
type 'a. In this case, we are writing that type 'b is a *specific* subtype
But when we write 'a alone, we generally mean "any type having 'a as a
supertype", and we tend to mean this in the "open" sense. When 'a is
written alone, it can be seen as a kind of open union type.
What seems odd to me is that we typically lose the ability to write
"exactly 'a". Though now that I think about it, I suppose we could write:
'a <: 'a
> I do think there would be annoying syntax required when returning
> functions or packing them into data structures, since you'll end up
> having to explicitly say what type you want stored in many cases.
Or let the inference system deduce it for you...
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the bitc-dev