[bitc-dev] Instance coherence: the shape of a solution
Jonathan S. Shapiro
shap at eros-os.org
Mon Apr 16 13:41:29 PDT 2012
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,
> > 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
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.
> > Why is this polluting the type system? Where should this distinction be
> > expressed, if not in the type system?
> I happily withdraw my concern, and agree that types are the correct
> place for them to go.
I was tweaking your nose here a bit, but there *is* a valid concern at the *
human* level: as the expressiveness of the types becomes too rich, humans
cease to be able to read them. In some cases, adding new expressiveness
actually *reduces* the value of types - even those that don't *use* the new
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the bitc-dev