[Agda] Records and irrelevant fields

[wren ng thornton]

On 9/18/10 12:32 AM, Dan Doel wrote:
> On Friday 17 September 2010 10:21:57 pm wren ng thornton wrote:
>> 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...
>
> I'm not certain what to make of this.
>
> For instance, I can make Squash a relative monad in the Monads Need Not be
> Endofunctors sense. In said paper, they define:
>
>    A monad relative to a functor J : C ->  D is
>      1) A functor T : C ->  D
>      2) A family of maps eta_A   : J A ->  T A, natural in A
>      3) A family of maps ext_A,B : (J A ->  T A) ->  T A ->  T B
>    (I think that's right.)

I'm thinking of a different generalization than that one. I haven't sat 
down and formalized my thoughts about it yet though, so I'm not sure if 
they could be reduced to one another.


> And I'm relatively sure we can't do the same modification to _>>=_. If we try:
>
>    _=<<_ : (A ->  Squash B) ->  Squash A ->  Squash B
>    f =<<  sq = elim (/\a ->  f a) sq -- Fail: an irrelevant a is being used in a
>                                    -- relevant spot.
>    f =<<  sq = elim (/\a ->  ? (squash (f a))) sq -- now we've back to doing
>                                                 -- Sq (Sq B) ->  Sq b
>
> Perhaps Coq would allow elimination of that sort (it seems likely that it
> would), but the way EPTSes work does not (primarily, I think, because it is
> not quite proof irrelevance that is modeled by an EPTS).

Coq does. Namely:

     Inductive Pf (A : Set) : Prop := pf : A -> Pf A.

     Definition Pf_bind {A B : Set} (xa : Pf A) (f : A -> Pf B)
         : Pf B := Pf_ind A (Pf B) f xa.

Notably, we cannot define Pf_join for this version. In order for Pf_join 
to be well-sorted we'd have to replace Set by Type (of course, the body 
of Pf_bind would be the same). Since all of Prop gets erased, Coq says 
it's fine to eliminate a Prop into Prop because the elimination will be 
erased as well.

But I'm not terribly familiar with EPTSes yet. I've had some thoughts on 
how to do irrelevance better than Coq (e.g., removing the Set/Prop 
distinction). I'd thought my ideas were along the same lines as EPTSes, 
though maybe not...

Hence why I should go read :)

-- 
Live well,
~wren