[Agda-dev] RFC: New semantics for record declarations

[Christian Sattler]

Apologies for resurrecting this old thread, but it is the latest reference
I could find.

Has a consensus ever been reached on improving the semantics for record
declarations? The current semantics is quite ugly it differentiates between
non-field declarations before and after the final record field and treats
the former ones as let-declarations. This prohibits many natural things
(see at least five issues on the issue tracker), e.g. declaring records
inside records, which is a very useful thing to have in the context of
iterated type dependency, e.g. when working with a type of internal
diagrams over a finite inverse category:

record Semisimplicial : Set₁ where
  record M₀ : Set where
  field X₀ : M₀ → Set
  T₀ = Σ M₀ X₀

  record M₁ : Set where
    field x₀₁ x₁₀ : X₀
  field X₁ : M₁ → Set
  T₁ = Σ M₁ X₁

  record M₂ : Set where
    field x₀₀₁ x₀₁₀ x₁₀₀ : X₀
    field x₀₁₁ : X₁ x₀₀₁ x₀₁₀
    field x₁₀₁ : X₁ x₀₀₁ x₁₀₀
    field x₁₁₀ : X₁ x₀₁₀ x₁₀₀
  field X₂ : M₂ → Set
  T₂ = Σ M₂ X₂

  record M₃ : Set where
    field x₀₀₀₁ x₀₀₁₀ x₀₁₀₀ x₁₀₀₀ : X₀
    field x₀₀₁₁ : X₁ x₀₀₀₁ x₀₀₁₀
    field x₀₁₀₁ : X₁ x₀₀₀₁ x₀₁₀₀
    field x₀₁₁₀ : X₁ x₀₀₁₀ x₀₁₀₀
    field x₁₀₀₁ : X₁ x₀₀₀₁ x₁₀₀₀
    field x₁₀₁₀ : X₁ x₀₀₁₀ x₁₀₀₀
    field x₁₁₀₀ : X₁ x₀₁₀₀ x₁₀₀₀
    field x₀₁₁₁ : X₂ x₀₀₀₁ x₀₀₁₀ x₀₁₀₀ x₀₀₁₁ x₀₁₀₁ x₀₁₁₀
    field x₁₀₁₁ : X₂ x₀₀₀₁ x₀₀₁₀ x₁₀₀₀ x₀₀₁₁ x₁₀₀₁ x₁₀₁₀
    field x₁₁₀₁ : X₂ x₀₀₀₁ x₀₁₀₀ x₁₀₀₀ x₀₁₀₁ x₁₀₀₁ x₁₁₀₀
    field x₁₁₁₀ : X₂ x₀₀₁₀ x₀₁₀₀ x₁₀₀₀ x₀₁₁₀ x₁₀₁₀ x₁₁₀₀
  field X₃ : M₃ → Set
  T₃ = Σ M₃ X₃

Cheers,
Christian

On Mon, Dec 8, 2014 at 11:09 AM, Andreas Abel <abela at chalmers.se> wrote:

> B' does not work since there are no record pattern matching top-level
> *declarations*.  If you try this outside of a record declaration, it does
> not work either:
>
>   postulate b : A
>   a' : Set
>   a a' = b
>
> The issue is that, currently, declaration between fields need to be
> interpreted both as let declarations and proper declarations inside the
> corresponding record module.
>
> My proposal would not get B' to work, but fix the other problem you
> mention, the lack of proper pattern matching definitions.
>
> Getting B' to work is orthogonal, in my opinion.  For this, we need to
> introduce a new form of declaration, the record pattern matching
> declaration (see snippet on top).
>
> Cheers,
> Andreas
>
>
> On 08.12.2014 08:15, James Chapman wrote:
>
>> I would like to pattern match on a record rather than opening inside a
>> record. I expected that this would work given the let based semantics
>> but I can't get it to work:
>>
>> module _ where
>>
>> record A : Set1 where
>>    constructor a
>>    field a' : Set
>>
>> h : A → Set
>> h x = let a a' = x in a'
>>
>> record B : Set1 where
>>    field b : A
>>    open A b
>>    field b' : a'
>>
>> {-
>> record B' : Set1 where
>>    field b : A
>>    a a' = b
>>    field b' : a'
>> -}
>>
>> The commented out record version doesn't work.
>>
>> I would also like to have proper pattern matching in records. There was
>> a previous proposal to achieve this by fixing let.
>>
>> Would your proposal lose the possibility of pattern matching on a record?
>>
>> James
>>
>>
>>
>> On Thu Dec 04 2014 at 11:14:10 AM Andreas Abel <abela at chalmers.se
>> <mailto:abela at chalmers.se>> wrote:
>>
>>     Well, the new semantics produces two internal modules and we need to
>>     ensure they do not show up when printing terms.  Given the fragility
>> of
>>     display forms, I am afraid they will...
>>
>>     On 04.12.2014 09:55, Nicolas Pouillard wrote:
>>      > I support lifting this restriction about let-like declarations in
>>     record
>>      > declarations. Do you see any drawback of your proposal?
>>      >
>>      > On 12/04/2014 12:10 AM, Andreas Abel wrote:
>>      >> W.l.o.g., a record declaration looks like this:
>>      >> (d1..d3 are declarations, [...] says explicitly what is in scope)
>>      >>
>>      >>   record R (p : P) : Set where
>>      >>     constructor c
>>      >>     d1[p]
>>      >>     field f1 : F1[p,d1]
>>      >>     d2[p,d1,f1]
>>      >>     field f2 : F2[p,d1,f1,d2]
>>      >>     d3[p,d1,f1,d2,f2]
>>      >>
>>      >> Current semantics:
>>      >>
>>      >>   postulate R : P -> Set
>>      >>   postulate c : (p : P) -> let d1 in (f1 : F1) ->
>>      >>                            let d2 in (f2 : F2) -> R p
>>      >>
>>      >>   module R (p : P) (r : R p) where
>>      >>     d1
>>      >>     f1 : F1
>>      >>     f1 = r.f1
>>      >>     d2
>>      >>     f2 : F2
>>      >>     f2 = r.f2
>>      >>     d3
>>      >>
>>      >> The drawback is that let only understands certain declarations. In
>>      >> particular, no fixity decls, no pattern matching etc.
>>      >>
>>      >> The following new semantics for record declarations would support
>>      >> arbitrary declarations:
>>      >>
>>      >>   postulate R : P -> Set
>>      >>
>>      >>   module #R0 (p : P) where
>>      >>     d1
>>      >>     module #R1 (f1 : F1) where
>>      >>       d2
>>      >>
>>      >>   postulate c : (p : P) (let open #R0 p ) (f1 : F1)
>>      >>                         (let open #R1 f1) (f2 : F2) -> R p
>>      >>
>>      >>   module R (p : P) (self : R p) where
>>      >>     open #R0 p public
>>      >>     f1 : F1
>>      >>     f1 = self.f1
>>      >>     open #R1 f1 public
>>      >>     f2 : F2
>>      >>     f2 = self.f2
>>      >>     d3
>>      >>
>>      >> Additionally, we can allow "self" to be in scope in d3.
>>      >>
>>      >> Comments welcome,
>>      >> Andreas
>>      >>
>>      >
>>
>>     --
>>     Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>>     Department of Computer Science and Engineering
>>     Chalmers and Gothenburg University, Sweden
>>
>>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>>     http://www2.tcs.ifi.lmu.de/~__abel/ <
>> http://www2.tcs.ifi.lmu.de/~abel/>
>>     _________________________________________________
>>     Agda-dev mailing list
>>     Agda-dev at lists.chalmers.se <mailto:Agda-dev at lists.chalmers.se>
>>     https://lists.chalmers.se/__mailman/listinfo/agda-dev
>>     <https://lists.chalmers.se/mailman/listinfo/agda-dev>
>>
>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160701/c576acfe/attachment.html