On Mon, Apr 16, 2012 at 2:40 PM, Geoffrey Irving <[email protected]> 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...
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
