On Mon, Apr 16, 2012 at 1:25 PM, Geoffrey Irving <[email protected]> wrote:
> On Mon, Apr 16, 2012 at 1:16 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > 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 constantness. 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 expressiveness. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
