But if it's only a user interface thing, then it's less… uhhh… 'first class'. Which could be good, but I dunno.
Conversation
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 { ... }`
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:
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
1
1
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
Show replies
Yeah seen that one before… I should look at it again 😅
