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

[James Chapman]

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> 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
> 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/20141208/4f03b14c/attachment.html