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

[Andreas Abel]

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/