Unification is an amazing CS algorithm. That doesn't mean that your language's operational semantics should be intimately tied to the intricate details of one specific instantiation! That is just too damned fragile.
-
-
-
Replying to @ezyang
Not just prolog. Also all statically typed languages whose type system is even more 'challenging' than prolog. Haskell with a few extensions. Or Coq.
0 replies 0 retweets 1 like -
This Tweet is unavailable.
-
But to do things at scale, it appears you have no choice but to play games with Coq's unifier. Or at least, that's what all the papers on large developments end up saying.
1 reply 0 retweets 1 like -
One needs to know one's unifier. Haskell? Robinson's algorithm will do, given that application is injective (but mind those type families). Agda? Get you Miller's algorithm, the sensible extension of Robinson to syntax-with-binding. Coq? Brittle, devious, capricious, gameable.
1 reply 0 retweets 11 likes -
Replying to @pigworker @jjcarett2 and
Idris is intentionally omitted from the above list. Currently undergoing surgery, I gather.
2 replies 0 retweets 0 likes
Indeed. The new version is an attempt at Miller's algorithm with tweaks for resolving interfaces. I'm hoping you'll be able to frighten^Wexercise it at some point when it becomes more stable...
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.