[Agda] Agda Observational equality using primUnsafeTrustMe?

[Dominique Devriese]

Hi all,

I'm fascinated by the issue of observational equality and
extensionality in Agda. I've read with interest Altenkirch, McBride
and Swierstra's 2007 PLPV paper "Observational Equality Now". What
I've been thinking about is the relation between their solution and
Agda's primTrustMe's construct.  Clearly, the latter is not concerned
with heterogeneous equality which Altenkirch et al work with, but this
difference does not seem fundamental.

More fundamentally, primTrustMe induces a check during reduction (not
type-checking) that its value arguments are definitionally equal,
which of course prevents it from being used in the proof of (for
example) extensional equality of functions. I'm wondering about what
happens if I just remove this reduction-time equality checking
(similar to how I understand the MAlonzo compiler handles
primTrustMe?). Clearly this is unsafe, but unsafety seems expected
when adding axioms to a theory? It intuitively feels safe to do for
properties that do not make the theory inconsistent (make bottom
provable).

To better understand this, I've done a quick-and-dirty experiment
implementation in the Agda codebase (patch attached if anyone is
interested, darcs diff -u for readability). What it does is add a
primUnsafeTrustMe primitive that is identical to primTrustMe except
for the removed reduction-time equality check. At first sight, it does
allow to formulate and exploit function extensionality while retaining
canonicity. I'm also attaching a test.agda file with some very simple
experiment code about this.

I'm trying to better understand the practical of theoretical
consequences of such a change. I'm not well versed in dependent type
theory, or its implementation aspects, so I hope a discussion on this
list might help clarify some points? Some specific questions I'm
thinking about:

* I have the intuition that primUnsafeTrustMe should be safe if you only
  use it to prove propositions that do not make the theory
  inconsistent, like function extensionality. Any thoughts?
* If someone were to use primUnsafeTrustMe to prove inconsistent
  propositions, then I would expect anything can happen (crash compiler,
  "launch the missiles"), but this feels similar to Haskell's unsafePerformIO
  primitive. Any further thoughts?
* Does such a change produce any undesirable interactions with other
  parts of Agda?
* Any thoughts on how this would extend to heterogeneous equality and
  coercions? A primUnsafeTrustMeHet primitive doesn't seem fundamentally
  different?

Hoping for an interesting discussion ;)
Dominique
-------------- next part --------------
A non-text attachment was scrubbed...
Name: agda-primUnsafeTrustMe.patch
Type: text/x-patch
Size: 1921 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110107/102b9738/agda-primUnsafeTrustMe.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.agda
Type: application/octet-stream
Size: 1017 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110107/102b9738/test.obj