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!
Conversation
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
Was just wondering if you had any more to elaborate on this?
1
I'm not an expert here but it seems primitive projections are the correct way to use coinductive types, since they give you eta laws but not dependent elimination (which can be used to violate subject reduction). So you don't want to treat them like (positive) inductive types.
1
1
Thanks for all your help and pointers btw! Really appreciate it!
1
1
Is it coinductive maybe because the projections have to account for the substitutions on the previous fields of the record?
I don't really have any intuition for coinductive types at all, but my understanding is that their coinductive nature doesn't really show up until you define the record type corecursively (at which point, it's sort of definitional).
1
1
Or a less opaque way to say it is: if you defined a positive inductive record type to be self-referential, you would never be able to instantiate it (since record types can have only one constructor). So the only meaningful semantics for such a type are coinductive.