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.
Conversation
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.
1
1
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
"I want staging"
Mum: "we have staging at home"
Staging at home: `const fn foo<const x: Int>() -> T { ... }`
not sure I get what staging means here? would you mind explaining? 😅
1
(I have a metaprogramming project going at $dayjob and if it's a concept I'm not familiar with, I'd like to know more)
1
Show replies