[Agda] Quotient types in Agda, if you Trust Me

[Andrew Pitts]

On 13 May 2015 at 16:16, Dan Licata <drl at cs.cmu.edu> wrote:
> Hi Matteo,
>
> Oops, the second datatype and the #out and #in functions were supposed to be indented into the private block, but they weren't.  I think the updated version on github prevents this problem?

Phew. I was trying to get a version of Matteo's example to work for
quotient.agda instead of hithacks.agda, but couldn't.

> Assuming the injectivity/disjointness analyses could be disabled, how would your proposal for private pattern matching be different than a private datatype?

I agree. Private pattern matching would still allow the
injectivity/disjointness property of private constructors to leak out
and cause a public contradiction, wouldn't it.

Andy


>
> -Dan
>
> On May 13, 2015, at 11:05 AM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
>
>> On Wed, May 13, 2015 at 3:00 PM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
>>>
>>> [..]
>>>
>>> So here's a challenge.
>>>
>>> Can anyone fill the hole in
>>>
>>> open import quotient
>>>
>>> data Empty : Set where
>>>
>>> contradiction : Empty
>>> contradiction = {!!}
>>>
>>> without any further use of primTrustMe or postulate?
>>>
>>> [..]
>>
>> After commenting out the open holes in hithacks.agda, on my system
>> (Agda 7b727e0) this is accepted:
>>
>> module challenge where
>>
>> open import hithacks
>>
>> txe : ∀ {l1}{X : Set l1}{l2}{Y : X → Set l2}{f g : (x : X) → Y x} →
>>        f == g → ∀ x → f x == g x
>> txe id _ = id
>>
>> contradiction : Void
>> contradiction = ne (txe (ap (λ f x → f x) (ap #out (seg <>))) _)
>>  where open Private
>>        ne : _ → Void
>>        ne ()
>>
>> At AIM XX I proposed to add the possibility to define datatypes and
>> functions over
>> them inside a specially marked block, while disabling pattern matching
>> for them outside
>> the block.
>>
>> Do you agree this could be an useful feature?
>>
>> I don't know whether it would be difficult to implement: for sure, I
>> don't know how to
>> implement that myself. :-)
>>
>> Best,
>> Matteo
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>