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

[Andreas Abel]

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/