[Agda] Agda Observational equality using primUnsafeTrustMe?

[Thorsten Altenkirch]

Hi Dominique,

I have been thinking about something like this but didn't realize it could be done so easily. I think this is an interesting idea.

It certainly breaks a number of things, e.g. subject reduction. But does it break termination?

Conor was always opposed to any such tricks because it breaks a number of things in the implementation. But he can talk for himself.

Cheers,
Thorsten

On 7 Jan 2011, at 14:56, Dominique Devriese wrote:

> 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
> <agda-primUnsafeTrustMe.patch><test.agda>_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda