[Haskell-cafe] Proposal: Applicative => Monad: Call for consensus

[Conor McBride]

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