Conor McBride conor at strictlypositive.org
Wed Jan 19 21:28:33 CET 2011

```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

```