[Agda] Records and irrelevant fields

[Dan Doel]

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.)

But this structure applied to Squash is trivial. If we're conceiving of J 
being the . annotation, and T = Squash, then we get:

  eta_A   : .A -> Squash A
  ext_A,B : (.A -> Squash B) -> Squash A -> Squash B

And indeed, these are the types for your return and _>>=_ above. But when . is 
used this way, it is essentially Squash itself. And every functor is a monad 
relative to itself:

  J = T
  eta_A   : T A -> T A = the identity natural transformation
  ext_A,B : (T A -> T B) -> (T A -> T B) = again some kind of identity

and that's what the above structure on Squash is.

But, due to the vagaries of the erasure annotations, we can also write:

  eta' : A -> Squash A
  eta' x = squash x

because we can take a relevant argument and use it in an irrelevant spot. But 
this is an even weirder proposition if we think of Squash not being an 
endofunctor, because then eta' is a family of morphisms between objects of 
different categories. Or it's an attempt to make a transformation between the 
functors I : Set -> Set and Pf : Set -> Prop. Coq/Agda has not problem with 
that, but I'm not sure what to make of it categorically.

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).

----

On an unrelated note, I wrote:

> Perhaps this is on the right track?

Lest one think my arguments make the answer to this an unqualified, "yes," I 
think an instructive question about all this stuff is, "how should equality 
work?"

Mishra-Linger's thesis gives two versions of the 'CONV' rule for EPTSes, which 
is the rule that specifies judgmental equality, I think. The first is the 
standard 'terms are equal if they have the same beta normal form.' Second, he 
provides a "proof irrelevant" rule (insert caveats), which is, 'terms are 
equal if their *erasures* have the same beta normal form.'

I seem to recall that something like the latter was on the table for the Agda 
implementation. For instance, it'd be nice if records that held irrelevant 
coherence proofs were equal up to ignoring those proofs. However, I suspect 
that doesn't mesh with allowing static contexts to look at the irrelevant 
stuff. Here's a sketch:

  -- Squash as a record
  record Squash (A : Set) : Set where
    constructor poof
    field
      .choose : A

  -- Suppose s :r Squash A ==> choose s :c A

  someBool1 :r Squash Bool
  someBool1 = poof false

  someBool2 :r Squash Bool
  someBool2 = poof true

  eq :r someBool1 == someBool2
  eq = refl -- By proof irrelevance, poof = poof

  -- x :r T ==> x :c T, so eq :c someBool1 == someBool2
  -- But, choose someBool1 : Bool, choose someBool2 : Bool

  badeq :c choose someBool1 == choose someBool2
  badeq = cong choose eq -- ?

The question being, what happens with badeq? What is its compile-time type? Is 
it false == true? If so, it's bad to be able to prove that, even if you can 
only prove it in the static portion of the program. If not, well, what's 
stopping it?

In this case, the opacity of the datatypes seems to be what enables proof 
irrelevant equality.

-- Dan