[bitc-dev] Instance coherence: the shape of a solution

[Jonathan S. Shapiro]

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
> closures.


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
particular subtypes.

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
of 'a.

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...
URL: http://www.coyotos.org/pipermail/bitc-dev/attachments/20120416/1ed1bd76/attachment.html