> some foundational issues around impredicative universe polymorphism
Could you elaborate on those?
Conversation
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
Yeah, definitely finding that 😂.
Do wonder if I should at least be starting to model this stuff in a proof system. That's yet another rabbit hole to head down! And from what I hear the proofs can be a pain - lots of mutual recursion and stuff. 😬
1
I think at this point most people involved in Coq development, at least, agree that a majority of the stuff in it should be in a proof assistant (maybe should have been from the beginning). I strongly recommend you try to prove as much as you possibly can; it'll save you later.
1
1
Do you have any recommendations of a proof system? I was messing with Lean for a bit because it worked with VS Code nicely, but they don't have as many libs for TT development atm - like variable binding and such. :/
1
Thankfully I've been writing down my judgements, but it would be nice to have some confidence in the actual metatheory! brendanzab.github.io/pikelet/append
1
One thing I've been toying with (that I should probably actually do) would be to use a tool like Iris to encode the (rough) logic of the reduction machine as an imperative program.
1
Then separately, you might design a language in Iris whose semantics were those of the abstract machine, and try to prove them observationally equivalent (using some sort of contextual refinement, maybe?).
3
So what I'm thinking is that I might just keep plugging away with the Rust implementation, but not get too fancy with any optimizations and caching - keep things pretty close to the syntax-directed algorithm I've defined.
Then I'd be wanting to start proving the metatheory of that syntax-directed algorithm. I'd defer more fancy iris stuff to when I want to start pushing for more performance on the implementation.
1
1
Initially the programs should be small (as I'm experimenting), and it'd be easier to get by with less performance. But I would at least have a plan towards better foundations.
1
Show replies