How to implement records

[andrejbauer]

Currently the record types are implemented so that they may contain any number of fields:

{ lbl1 : type1 ; ... ; lblN : typeN }

This is convenient for the user, but it makes the code hairy. Also, it's going to make record types hard to work with on the meta-level in tt. Here is another possibility: we define a primitive dependent sum which has just two fields with fixed names fst and snd:

{ fst : type1 ; snd : type2 }

(of course type2 depends on type1) We then provide sufficient sugar for the general records (as above) to be implemented as nested dependent sums. We would still have labels and all that, so to the user it would all look like it does now. But in addition any theorem stated about dependent sum would apply to any record type.

One drawback is that we would need to treat records with a single field differently.

I wonder how hard it would be to do this. Essentially we need to map teh labels lblN to suitable combinations of projections snd.snd. ....snd.fst.

[pthariensflame]

You could also look at how the Agda standard library implements records.

[andrejbauer]

I don't think that's related. I am talking about record types, and that piece of code seems to be about PERs.

[pthariensflame]

@andrejbauer Sorry! I linked to the README rather than the actual implementation. I thought you would pick up on that. :laughing: The implementation itself is here.

[andrejbauer]

This seems to be at the wrong level. The correct level would be to show me some Haskell code, as we are talking about how to write OCaml code that handles records in Brazil.

[pthariensflame]

Why is that the wrong level? It's very close to how it could be presented in Brazil "on the metalevel", as you put it. Regarding implementation in OCaml, why is having arbitrarily-sized records "hairy"?

Since you've pointed out what you intended, though, I'll look into how Agda implements its own record types. Maybe then I can be of some help. :smile:

[andrejbauer]

The implementation is hairy because every damn time you want to do anything with a record or a record type you have to write a little fold function.

[JasonGross]

If you're looking into how other languages implement records, I wonder if Adam Chilpala's Ur/Web might be a useful model ( http://www.impredicative.com/ur/); although it's not dependently typed, it has anonymous records (it calls them row types), and supports various metaprogramming operations on them.

[pthariensflame]

For the record (if you'll pardon the pun) here's what Agda does.

[andrejbauer]

Ah yes, in Agda you have to name record types. I was rather hoping that in Brazil Andromeda we could have anonymous records (rows?), so one could type {re = 2 ; im - 6} without first defining a type complex. I am generally a big fan of orthogonality -- I also think inductive types should be definable without having a name, although that might be harder (because sums can be hard to use when not given a name).

[jonsterling]

Might be worthwhile to look at Kopylov's work on dependent records from dependent intersection types in Nuprl/CTT. I don't know the extent to which Brazil could support something like that, but it seemed pretty neat.

Edit: After thinking about it some more, I don't think this approach will be applicable to Andromeda, since whilst you do have some manner of reflected equality, I do not believe you can (or would even desire to) express the untyped membership relation which makes it all go in Nuprl.

[andrejbauer]

Right, I think the underlying untyped calculus of Nuprl makes many things work smoothly, but we don't have that available. Is there another extensional dependent type theory proof assistant out there?

[jonsterling]

I'm not sure if there is... I talked to Bob Harper a few weeks ago, and he seems to believe that the only way to make equality reflection go smoothly is to use realizability with an untyped underlying syntax à la Nuprl. So this might be new territory as far as extensional proof assistants go…

[andrejbauer]

Here's another idea: http://research.microsoft.com/pubs/65409/scopedlabels.pdf

[jonsterling]

Thanks for the link, I'll give it a read! I need to resume thinking about records at some point soon, since we're really feeling the pain without them in JonPRL, and whilst I previously had intended to go the dependent intersection route I mentioned here last June, they are honestly just horrible to use in practice. Last time I spoke with Bob Constable, he still seemed very gung ho about them, but I suspect he has not actually used them except in theory.

[andrejbauer]

We're hoping to equate records and modules, more or less.

[andrejbauer]

A version of records has been implemented a while ago.