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.
Conversation
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 { ... }`
1
2
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
TBH I need to understand more about it, but here I think you can consider it's a bit of code that is 'staged'. ie. it won't be compiled until you provide it with a constant argument.
1
I do believe there might be a connection between 'staged programming' and Rust's 'angle bracket' parameters (which are always monomorphised), but I'm not really sure of the precise connection. There's a bibliography of related stuff here:
3
1
1
Was also wondering about this stuff here:
Quote Tweet
Has there been any work on looking at the relationship between monomorphised, static polymorphism (like in C++ and Rust, etc), and staged programming? I think the interesting thing here is that instead of inlining stuff, we sort of memoize each instantiation?
Show this thread
There is 'multistage programming' where programs are broken up into multiple stages of code generation - kind of like type-safe macros. Here we just have compile time and runtime so I was referring to it as 'staging'. But yeah I could have no idea what I'm talking about.
1
this sounds like nanopass. but than the first thing you said sounds like partial evaluation.
2
1
Show replies