[Agda] Agda Observational equality using primUnsafeTrustMe?

[Thorsten Altenkirch]

Ok, even if we only postulate ext : ((x: A) -> f x = g s) -> f = g and add an equality ext p = refl then p may be a lie but subst (ext p) reduces which can cause non-termination. 

I guess the real question is why does it matter if termination fails after you have assumed some lies.

Thorsten

On 9 Jan 2011, at 10:20, Conor McBride wrote:

> 
> On 9 Jan 2011, at 02:51, Dan Doel wrote:
> 
>> On Friday 07 January 2011 7:04:49 pm Conor McBride wrote:
>>> 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?
>>> 
>>> Since it now is tomorrow, I can confirm that, yes, it does
>>> break termination.
>> 
>> To elaborate slightly on Conor's answer, the question is roughly the same as
>> asking, "is it safe to erase/be lazy in equality proofs?" And the answer to
>> that, for open terms, is "no."
> 
> Let me give some more clues. Firstly, the condition that all postulates are
> consistent is no talisman against error. One need merely *hypothesize* a
> lie to create trouble. The world of open terms is a dangerous place where
> all lies are true and functions from the empty type can be persuaded to
> return canonical values. In that setting, an excess of trust is lethal.
> 
> All the best
> 
> Conor
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda