|
|
|
|
|
|
by zozbot234
424 days ago
|
|
|
> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem. I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program. |
|
|
Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure.
> inherently involve a kind of compile-time evaluation.
compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.