Yes I want nice modules so bad. Namespaces are also interesting but I don't understand them as much. Also interested in how stuff like staged computation interacts with package managers. Like it would be cool to be able to avoid depending on packages that have been inlined away.
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
same boat here :( my best idea so far is to treat them like (non-extensible) records.
1
1
The fact that they’re extensible records seems (almost) the whole point, otherwise you can just use Coq modules. “Open” namespaces _can_ be encoded in Coq, exploiting its lookup rules — much more easily than anything in math-comp, and I do it by hand, but it’s still annoying.
2
Yeah, not sure I understand the 'not being extensible thing'. I'm sort of thinking of namespaces like in Lean, C++, etc. Like you can split namespaces over multiple files and build them up incrementally. But we might be talking about different things?
2
1
One thing I want to figure out is a nice way to scope data constructors under the name of a type, like in Rust and Lean. Would be cool to have some sort of systematic approach to extending 'paths' like this, but I dunno what that would look like…
1
Like, I kind of think of the 'path' as like a 'bookmark' that makes it easy for the programmer to find stuff in a sort of soup of nodes… like, it's more of a user interface thing? I dunno though
1
But if it's only a user interface thing, then it's less… uhhh… 'first class'. Which could be good, but I dunno.
1
A joy of a dependently-typed language is that first-class abstractions don't just have a cost at runtime (which can be optimized away), but also at proof time. And now your inliner is a piece of ltac or proof automation, that is either way a cost.
1
1
Wanted: partial evaluation and staging for proof search.
And I don't mean the idealized proof search of a logic, but the one from a proof assistant, and one supporting domain-specific proof automation.
1
1
3
Yes me too! That would be so neat.
I mainly want this for dependently typed metaprogramming, levitation, and faster codegen, but yeah, having it for proofs would be really cool too.
1
OTOH...
"I want staging"
Mom: "we have staging at home"
Staging at home: Coq's "Eval cbv in <term>"
1
2
Show replies