Modules ~= records is the only correct way to go, IMO, at least conceptually (if we can work out some foundational issues around impredicative universe polymorphism, anyway). You do want other stuff from modules but you hope it can desugar to records.
Conversation
> some foundational issues around impredicative universe polymorphism
Could you elaborate on those?
1
If you have universe polymorphic constants in a functor, you get a type signature with non-prenex universe polymorphism. It's *probably* fine, but there's no set model for it yet and (in Coq anywayt) no syntax, either, precluding records as modules. Hopefully, that'll change!
1
1
Would this show up much in general programming? For context I'm working on a dependently typed programming language that uses dependent records for modularity: github.com/brendanzab/pik - less of a focus on theorem proving right now though.
1
Yeah, I've seen it :) No, this is something that wasn't even originally intended to be *possible* in Coq, so no, people aren't screaming urgently for a use case here. You are going to want a module system of some sort, of course, but be careful... dependent types are tricky.
2
1
If I were designing a "nice" module system, I'd probably start by seeing if I could manage to keep inductive types efficient if I allowed their declaration inline (see arxiv.org/pdf/1309.5767.). That inherently helps make inductive types "structural" for conversion purposes.
1
1
My pain at the moment is `record { t = String, x = "hello" } : Record { t : Type, x : String }` - the lhs infers to `Record { t : Type, x : String }` in my bidirectional checker.
1
Woops, I mean that currently this fails to typecheck: `record { t = String, x = "hello" } : Record { t : Type, x : t }`
1
Oh gosh, I was just about to give you advice on how to implement dependent records, since that's another place a lot can go wrong... in particular you probably want first class projections for records and to make records *negative* types, not sugar for inductive types.
2
1
Trying to go carefully, but seriously feeling this kitty right now:
GIF