The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

On 09/01/2014 10:18, "Altenkirch Thorsten"
<psztxa AT exmail.nottingham.ac.uk>
 wrote:

>>
>>
>>
>>Higher-order datatypes are a bit more difficult, and I admit I never
>>worked it out. I believe it's possible though.
>>
>>>> The fact that the implementation is behind the theoretical
>>>>capabilities
>>>> is just that, an implementation problem.
>>> The eliminators are like axioms in set theory and it is worthwhile to
>>> translate any extension by reducing them to the axiom instead of adding
>>> new ones even though they may be semantically justified.
>>That's fair, but I don't see why eliminators have a more powerful
>>ontological status than sized-types.
>
>It is maybe not the ontological status but they are a hell easier to write
>down!
>
>Do I believe in a foundational system which consists of pages with rules
>full of greek (and other alphabets) and super sub and whatever scripts?
>
>Actually I also don't like the schemes for datatypes either, hence I would
>like to reduce everything to fixed collection of type formers (we have
>done a fair bit of this using containers).
>
>So my target type theory is 0,1,2,Pi,Sigma,Id,U_n with eliminators. Ok we

I forgot W :-(

>will need to consider extensions for induction recursion and HITs but they
>should also presented by a finite collection of constants with
>eliminators.
>
>I know there are some gaps in between what we like to do and what we know
>it is safe to do but I think we should be able to narrow this gap.
>
>Thorsten
>
>>They require work to be derived as
>>well, and the correctness proofs for them are quite similar to that for
>>sized types. This seems like a matter of preference. Obviously I'm not
>>neutral in this matter though.
>>
>>Best,
>>
>>Cody
>>
>>
>>
>>> Thorsten
>>>
>>>
>>>> Best,
>>>>
>>>> Cody
>>>>
>>>>
>>>>> V.
>>>>>
>>>>>
>>>>> On Jan 6, 2014, at 6:27 PM, Cody Roux 
>>>>> <cody.roux AT andrew.cmu.edu>
>>>>>wrote:
>>>>>
>>>>>> The thing about Coq is that it's very disturbing not to have a
>>>>>> Set-theoretic interpretation where Prop is the set of Booleans
>>>>>>{True,
>>>>>> False}. Agda of course doesn't have these qualms, but the fact that
>>>>>> this
>>>>>> issue appears in Coq without use of anything fancy (impredicativity,
>>>>>> etc) makes me still a bit worried. In particular there should be a
>>>>>> Set-theoretic model for Agda where Empty -> Box and Box -are- equal:
>>>>>> with a sufficiently clever interpretation of inductives, I believe I
>>>>>> can
>>>>>> get [[Empty -> Box ]] = [[Box]] = { {} } (where {} is just the empty
>>>>>> set). Can someone with more Agda knowledge try to type the original
>>>>>> problematic term?
>>>>>>
>>>>>>
>>>>>> Hypothesis Heq : (False -> False) = True.
>>>>>>
>>>>>> Fixpoint contradiction (u : True) : False :=
>>>>>> contradiction (
>>>>>> match Heq in (_ = T) return T with
>>>>>> | eq_refl => fun f:False => match f with end
>>>>>> end
>>>>>> ).
>>>>>>
>>>>>>
>>>>>>
>>>>>> On 01/06/2014 06:12 PM, Altenkirch Thorsten wrote:
>>>>>>> Hi Maxime,
>>>>>>>
>>>>>>> your postulate seems correct since certainly Empty → Box and Box
>>>>>>>are
>>>>>>> isomorphic and hence equal as a consequence of univalence.
>>>>>>>
>>>>>>> However, I think the definition of loop looks suspicious in the
>>>>>>> presence
>>>>>>> of proof-relevant equality: if we replace rewrite by an explicit
>>>>>>>use
>>>>>>> of
>>>>>>> subst, loop isn't structural recursive anymore. Hence my diagnosis
>>>>>>> would
>>>>>>> be that rewrite is simply incompatible with univalence.
>>>>>>>
>>>>>>> Cheers,
>>>>>>> Thorsten
>>>>>>>
>>>>>>> On 06/01/2014 20:42, "Maxime Dénès" 
>>>>>>> <mail AT maximedenes.fr>
>>>>>>>  wrote:
>>>>>>>
>>>>>>>> Bingo, Agda seems to have the same problem:
>>>>>>>>
>>>>>>>> module Termination where
>>>>>>>>
>>>>>>>> open import Relation.Binary.Core
>>>>>>>>
>>>>>>>> data Empty : Set where
>>>>>>>>
>>>>>>>> data Box : Set where
>>>>>>>> wrap : (Empty → Box) → Box
>>>>>>>>
>>>>>>>> postulate
>>>>>>>> iso : (Empty → Box) ≡ Box
>>>>>>>>
>>>>>>>> loop : Box -> Empty
>>>>>>>> loop (wrap x) rewrite iso = loop x
>>>>>>>>
>>>>>>>> gift : Empty → Box
>>>>>>>> gift ()
>>>>>>>>
>>>>>>>> bug : Empty
>>>>>>>> bug = loop (wrap gift)
>>>>>>>>
>>>>>>>> However, I may be missing something due to my ignorance of Agda.
>>>>>>>>It
>>>>>>>> may
>>>>>>>> be well known that the axiom I introduced is inconsistent. Forgive
>>>>>>>> me if
>>>>>>>> it is the case.
>>>>>>>>
>>>>>>>> Maxime.
>>>>>>>>
>>>>>>>> On 01/06/2014 01:15 PM, Maxime Dénès wrote:
>>>>>>>>> The anti-extensionality bug is indeed related to termination.
>>>>>>>>>More
>>>>>>>>> precisely, it is the subterm relation used by the guard checker
>>>>>>>>> which
>>>>>>>>> is not defined quite the right way on dependent pattern matching.
>>>>>>>>>
>>>>>>>>> It is not too hard to fix (we have a patch), but doing so without
>>>>>>>>> ruling out any interesting legitimate example (dealing with
>>>>>>>>> recursion
>>>>>>>>> on dependently typed data structures) is more challenging.
>>>>>>>>>
>>>>>>>>> I am also curious as to whether Agda is impacted. Let's try it :)
>>>>>>>>>
>>>>>>>>> Maxime.
>>>>>>>>>
>>>>>>>>> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>>>>>>>> Which bug was this?
>>>>>>>>>>
>>>>>>>>>> I only saw the one which allowed you to prove
>>>>>>>>>>anti-extensionality?
>>>>>>>>>> But
>>>>>>>>>> this wasn't related to termination, or?
>>>>>>>>>>
>>>>>>>>>> Thorsten
>>>>>>>>>>
>>>>>>>>>> On 06/01/2014 16:54, "Cody Roux" 
>>>>>>>>>> <cody.roux AT andrew.cmu.edu>
>>>>>>>>>>wrote:
>>>>>>>>>>
>>>>>>>>>>> Nice summary!
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>>>>>>>>>> Agda enforces termination via a termination checker which is
>>>>>>>>>>>>more
>>>>>>>>>>>> flexible but I think less principled than Coq's approach.
>>>>>>>>>>> That's a bit scary given that there was an inconsistency found
>>>>>>>>>>>in
>>>>>>>>>>> the Coq termination checker just a couple of weeks ago :)
>>>>>>>>>>>
>>>>>>>>>>> BTW, has anyone tried reproducing the bug in Agda?
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> Cody
>>>>>>>>>> This message and any attachment are intended solely for the
>>>>>>>>>> addressee
>>>>>>>>>> and may contain confidential information. If you have received
>>>>>>>>>>this
>>>>>>>>>> message in error, please send it back to me, and immediately
>>>>>>>>>>delete
>>>>>>>>>> it. Please do not use, copy or disclose the information
>>>>>>>>>>contained
>>>>>>>>>> in
>>>>>>>>>> this message or in any attachment. Any views or opinions
>>>>>>>>>>expressed
>>>>>>>>>> by
>>>>>>>>>> the author of this email do not necessarily reflect the views of
>>>>>>>>>> the
>>>>>>>>>> University of Nottingham.
>>>>>>>>>>
>>>>>>>>>> This message has been checked for viruses but the contents of an
>>>>>>>>>> attachment
>>>>>>>>>> may still contain software viruses which could damage your
>>>>>>>>>>computer
>>>>>>>>>> system, you are advised to perform your own checks. Email
>>>>>>>>>> communications with the University of Nottingham may be
>>>>>>>>>>monitored
>>>>>>>>>> as
>>>>>>>>>> permitted by UK legislation.
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>> _______________________________________________
>>>>>>>>> Agda mailing list
>>>>>>>>> Agda AT lists.chalmers.se
>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>