[bitc-dev] Instance coherence: the shape of a solution
irving at naml.us
Mon Apr 16 14:40:11 PDT 2012
On Mon, Apr 16, 2012 at 1:41 PM, Jonathan S. Shapiro <shap at eros-os.org> wrote:
> On Mon, Apr 16, 2012 at 1:25 PM, Geoffrey Irving <irving at naml.us> wrote:
>> On Mon, Apr 16, 2012 at 1:16 PM, Jonathan S. Shapiro <shap at eros-os.org>
>> > If you said: the type system should preserve the ability to treat these
>> > interchangeably where their compile-time constant-ness is not an issue,
>> > then
>> > I wholly agree. That doesn't mean that they need to have the same type.
>> I completely agree that their types are actually, fundamentally
>> different. However, the result is that the type of map has to become
>> something like
>> map :: f -> List x -> List (f x)
>> instead of
>> map :: (x -> y) -> List x -> List y
> I'm not clear why that should be. What I'm suggesting is that there are (and
> in fact always have been) two distinct arrow types: one describing
> procedures and the other describing closures. It has historically been true
> that the distinction between these two arrow types could be ignored for all
> purposes of interest, so there was no benefit to specializing the type
> system excessively.
> Then a third arrow type came along, in the form of type class methods.
> Now we can easily enough introduce distinct notation for these three arrow
> types. Further, we can then introduce something like a kind class letting
> all of them be used interchangeably in your original notation. In this
> interpretation, the meaning of
> 'a -> 'b
> is "a function or method accepting things of type 'a and producing things of
> type 'b, without regard to the effects of the function or the constantness
> of the function".
> It's merely a choice of how to interpret the notation. So in the end, I'm
> not sure why the notation
> map :: (x -> y) -> List x -> List y
> needs to change here when we intend to be polymorphic over effects and
> The place that needs to change when we want explicit instantiation is the
> internal type of map, where we need to document our intention.
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. The worry then becomes ending up with a type system as
powerful as subtyping, with all the complexities thereof. Of course,
if we want subtyping and inheritance anyways, that might not be 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.
This is probably inevitable, though.
More information about the bitc-dev