Hi Tyson (So OT, I'm switching to cafe.) On 19 Jan 2011, at 18:24, Tyson Whitehead wrote:
On January 17, 2011 16:20:22 Conor McBride wrote:
Ahem
: )
The unfortunate pain you pay for this additional power is manually having to specify the application (<$> and <*>) and merging (join). If the compiler could figure this all out for you based on the underlying types, wow!
To achieve such a thing, one would need to ensure a slightly more deliberate separation of "value" and "computation" in the presentation of types. In Haskell, we use, e.g., [Int], for
* pure computations of lists of integers * nondeterministic computations of integers
[..]
I'm pretty sure I know what "pure computations of lists of integers" is, but I'm not so sure about "nondeterministic computations of integers".
If it is not too much of an effort, could you clarify with a quick example?
Viewing [] as a monad, you can view [1,2] as a nondeterministic integer with possible values 1 and 2. Lifting operations to this monad gives you "all possible combinations" computation, so, as SHE would have it, (| [1,2] + [3,4] |) = pure (+) <*> [1,2] <*> [3,4] = [4,5,5,6] It's not hard to come up with examples where lifted and unlifted both make sense. With a bit of help from Twitter, we have (courtesy of Andy Gimblett) (["under","over"] ++ ["state","wear"]) = ["under","over","state","wear"] but (|["under","over"] ++ ["state","wear"]|) = ["understate","underwear","overstate","overwear"] and (courtesy of Dan Piponi) (["plan","tan"] ++ ["gent","king"]) = ["plan","tan","gent","king"] but (|["plan","tan"] ++ ["gent","king"]|) = ["plangent","planking","tangent","tanking"] 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. After types for representation, let us have types for explanation. All the best Conor