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

[Andreas Abel]

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/