On January 19, 2011 15:28:33 Conor McBride wrote:
In each case, the former has (++) acting on lists of strings as pure values, while the latter has (++) acting on strings as values given in []-computations.
The type [String] determines a domain, it does not decompose uniquely to a notion of computation and a notion of value. We currently resolve this ambiguity by using one syntax for pure computations with [String] values and a different syntax for [] computations with String values.
Just as we use newtypes to put a different spin on types which are denotationally the same, it might be worth considering a clearer (but renegotiable) separation of the computation and value aspects of types, in order to allow a syntax in which functions are typed as if they act on *values*, but lifted to whatever notion of computation is ambient.
Yes. That makes sense. Thank you both for the clarification. The idea of explicitly separating the two aspects of types is an interesting one. The automated approach I had been thinking of was to always take the simplest context possible. (i.e., for the above, list of strings as pure values). To this end I've been working on a measure for the complexity of the application operator. I've got a draft at http://www.sharcnet.ca/~tyson/haskell/papers/TypeShape.pdf I'm still working on my thinking on polymorphic types though, so everything from section 2.2 onwards is subject to change (especially 2.3 and the conclusion). Cheers! -Tyson