[Agda] Prop in Agda 2.6 - again

[Jesper Cockx]

I guess most of the reasons why one would use a record type instead of a
single-constructor datatype still apply:
- You get the projections for free
- You can define new elements using copatterns
- You can make the record coinductive if needed

-- Jesper

On Wed, Jun 5, 2019 at 3:46 PM Andrew Pitts <andrew.pitts at cl.cam.ac.uk>
wrote:

> Dear Jesper,
>
> On 5 Jun 2019, at 13:34, Jesper Cockx <Jesper at sikanda.be> wrote:
>
> Hi Andy,
>
> When you define a datatype in Prop, the resulting type is automatically
> 'squashed', i.e. any two elements are equal. In contrast, for record types
> this is not possible because then it is impossible to define the
> projections. For your definition of ∃ in Prop, (true , _) is equal to
> (false , _) of type `∃ Bool (λ _ → ⊤)`, but their first projections are not
> equal. It would theoretically be possible to have such a record type but
> not give access to the projections and disabling eta-equality, but then you
> could've equally defined it as a single-constructor datatype.
>
>
> I see. So to paraphrase your explanation, Agda imposes a simple syntactic
> restriction on what record types can be declared to have type Prop in order
> to maintain the soundness of forcing all elements of an element of a Prop
> to be definitionally equal.
>
> I can think of a simple syntactic restriction that is less liberal than
> the current one: don’t allow record types in Prop! Is there an example of
> why my restriction is too restrictive? —- in other words a case where using
> a record of Prop type is really better than using a corresponding
> single-constructor datatype of type Prop?
>
> (I am thinking that one often uses a record type in Set instead of a
> single-constructor-datatype in Set, in order to get definitional eta
> expansion; but that’s automatic for elements of Prop, due to the
> definitional proof irrelevance.)
>
> Andy
>
>
>
> -- Jesper
>
> On Wed, Jun 5, 2019 at 1:09 PM Andrew Pitts <andrew.pitts at cl.cam.ac.uk>
> wrote:
>
>> Here is another question about Prop in Agda 2.6. Can anyone enlighten me?
>>
>> The documentation says
>>
>> "Just as for Set, we can define new types in Prop’s as data or record
>> types”
>>
>> However, although Agda 2.6 allows the declaration of the following
>> one-constructor datatype
>>
>> data ∃ {l m}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where
>>   _,_ : (x : A)(p : P x) → ∃ A P
>>
>> if instead I try to define a record type
>>
>> record ∃ {l m : Level}(A : Set l)(B : A → Prop m) : Prop (l ⊔ m) where
>>   constructor _,_
>>   field
>>     fst : A
>>     snd : B fst
>>
>> Agda complains (somewhat ungrammatically) that
>>
>> "Set l is not less or equal than Prop (l ⊔ m) when checking the
>> definition of ∃”
>>
>> So it doesn’t mind the parameter (A : Set l) when defining a datatype in
>> Prop (l ⊔ m), but does mind it when defining a record type.
>>
>> Why is that?
>>
>> Andy
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190605/6b33550f/attachment.html>