It's kiiind of neat from an ergonomics perspective. Less names to come up with. Lean is interesting - each type adds a new namespace that you can add stuff to. Not sure how it works out though. Personally I prefer just going with modules==records though.
Conversation
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.
1
> 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
Was just wondering if you had any more to elaborate on this?
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
Show replies