(which two syntaxes do you mean? . and ::?)
Rust does conflate types and modules, aka `impl` blocks and "UFCS"
Conversation
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.
3
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
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
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
Show replies