[Agda] Agda Observational equality using primUnsafeTrustMe?

[Conor McBride]

On 9 Jan 2011, at 14:44, Thorsten Altenkirch wrote:

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

As we cannot, in general, tell truth from falsity, this question
is effectively the same as

   "why does it matter if termination fails?"

I'll tell you tomorrow,

Conor




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