[Agda] Records and irrelevant fields

[wren ng thornton]

On 9/20/10 6:31 PM, Andreas Abel wrote:
> Interestingly, the bind operation cannot be defined directly,
>
> bind : {A B : Set} -> Squash A -> (A -> Squash B) -> Squash B
> bind (squash a) f = f a -- a cannot be used here!
>
> but in terms of map and join (as in the textbooks).
>
> bind sa f = join (map f sa)
>
> That's a bit weird. (Not the first weirdness, as we have seen.)

Given the differences in how Coq and Agda treat irrelevance/Prop, that 
actually makes sense (to me). You can't pull the a out and apply f 
because you don't *know* f will be safe (in some obscure sense) and 
return a new Squash; whereas once you map f, safely keeping it over in 
Squash land, then you can join the layers without any worry that a might 
escape. The fact that we can use both methods for the (relevant) 
identity monad is sort of an oddity in the first place.

It's a bit curious though--- that Agda makes join easy and bind hard, 
whereas Coq makes bind easy and join hard. It almost makes sense in as 
much as the Coq version has the constructor be of a type similar to, 
squash : A -> .(Squash A), whereas the Agda version makes the argument 
irrelevant instead of the result. But it's still curious...

-- 
Live well,
~wren