[Agda] Agda Observational equality using primUnsafeTrustMe?

[Conor McBride]

On 7 Jan 2011, at 17:05, Thorsten Altenkirch wrote:

> 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?

I'll tell you tomorrow.

Conor

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