ehatti

4 ms·

1.
Show HN: Querdex – A Crowdsourced Search Engine(querdex.com)
3 points by ehatti 1y ago|0 comments
2.
by ehatti 4y ago
I saw it a while back and thought the ideas were cool, but I didn’t check it out in enough detail to draw inspiration from it.
3.
by ehatti 4y ago
Unfortunately not! Embarrassingly, I haven't implemented pattern matching yet, which means functions like `sum` and `filter` can't be written. So far all my effort has gone towards the metaprogramming system. Bugfixing has me occu
4.
by ehatti 4y ago
Unfortunately there isn't, but I'll try my best here: In two level type theory, your language is actually two languages - a "meta language" (or meta level ) and an "object language" (or object level ). Addi
5.
by ehatti 4y ago
Because of the nondeterminism we get from the metalanguage being a logic language, we don't have to worry about applying optimizers in a particular order. You can compose optimizers together, produce the possible results, and then sele
6.
by ehatti 4y ago
Yes. As I’ve said elsewhere, the system is not limited to simple term rewrites.
7.
by ehatti 4y ago
The difference is that it’s much more general - the metalanguage is an actual logic language, not limited to simple rewrites. You can (read: will be able to, haha) prove properties about meta-level program transformations. For those interes
8.
by ehatti 4y ago
Not really. A detailed account of 2LTT can be found in this paper https://arxiv.org/abs/1705.03307 - 2LTT can be thought of as a general, type theoretic framework for metaprogramming.
9.
Show HN: Peridot – A functional language based on two-level type theory(github.com)
151 points by ehatti 4y ago|40 comments