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

[Nicolas Pouillard]

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
>

-- 
Best regards,
-- NP