Hacker News Reader

What kinds of metaprogramming cannot be expressed via dependent types? AIUI, dependent types potentially dispense completely with the phase separation found in languages like C, so anything can be "evaluated at compile time" simply by writing ordinary programs that make sense within the language itself. Of course sometimes it is desirable to reintroduce a separate "run time" phase, but this can be done via program extraction.

View on HN

In general, dependently typed systems lack the ability to metaprogram at the syntactic level. This is particularly true we’re binding forms are concerned. The most thoroughly pursued type theoretic way to do this is to implement a modal type system, which is technically orthogonal to the dependency capabilities of the type system, but integration of the two is tricky.

What're the failings of elaborator reflection in providing this in your view? I haven't used it thoroughly, but I thought one could define custom binding forms with it (in Idris 1, at least).

Reply on news.ycombinator.com