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