[Agda] Records and irrelevant fields

[wren ng thornton]

On 9/17/10 2:37 PM, Dan Doel wrote:
> As an additional weirdness point, Mishra-Linger notes in his thesis that the
> EPTS Squash is not a monad in the basic theory:
>
>    data Squash (A : Set) : Set where
>      squash : .A ->  Squash A
>
>    elim :  (A : Set) (P : Squash A ->  Set)
>         ->  (.(x : A) ->  P (squash x)) ->  (b : Squash A) ->  P b
>
>    join : (A : Set) ->  Squash (Squash A) ->  Squash A
>    join = elim (Squash A) (\_ ->  Squash A) ?
>
> What to fill in the hole is the issue. It needs to have type
>
>    .(Squash A) ->  Squash A
>
> But \x ->  x fails for this. We also cannot do tricks with elim, because (at
> best) it will reduce down to writing .A ->  A. So, in the default system,
> Squash A is not interchangeable with Squash (Squash A), and so on.

We just need to extend our notion of monads beyond just those which are 
endofunctors. Because Squash (effectively) doesn't take the category of 
types to itself, and that's all that causes the problem. We can, 
however, make a Kleisli triple out of it (return = squash, _>>=_ = elim 
A (\_ -> Squash B)). This is one of the places where Kleisli triples are 
a more powerful definition than (endo)monads. It's still a monad, just 
not an endomonad.

In Coq I've always called this type Pf : Set -> Prop, though Coq makes 
explicit that it's not an endofunctor. And now I should go off and read 
Mishra-Linger and Sheard...

-- 
Live well,
~wren