3 ms·
>Statically typed code is only type-safe as long as you don't use any meta programming techniques. MetaOCaml: http://en.wikipedia.org/wiki/Objective_Caml#MetaO
by thesz 16y ago
>Statically typed code is only type-safe as long as you don't use any meta programming techniques.
MetaOCaml: http://en.wikipedia.org/wiki/Objective_Caml#MetaOCaml http://en.wikipedia.org/wiki/Objective_Caml#MetaOCaml
TemplateHaskell: http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/template-haskell.html http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/temp...
"A Verified Staged Interpreter is a Verified Compiler (Multi-stage Programming with Dependent Types)": http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.3609 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.3...
I think that metaprogramming techniques would only gain from strong types.
I don't agree with most points of your comment, but I do not think I have strong arguments against.
- fauigerzigerk 16y agoThe MetaOCaml example is certainly interesting but what it does is increase speed, not reliability. In this case, the type (in some general sense) of n is known at compile time, so the compiler can guarantee that whatever is generated at runtime conforms to that type. But that's not the type of meta programming that depends on runtime discovery of entirely new information, say, an ORM that discovers changes in the database schema. That's the type of meta programming that made Rails so popular and productive (and slow) for some cases. Obviously, it is impossible to provide compile time guarantees about something that is unknown at compile time. But I tend to agree with you that it is desirable to have correctness proofs at compile time wherever possible.