Unification (2018)
eli.thegreenplace.net
eli.thegreenplace.net
``` expr = foo[bar[k], baz[V]]; expr /. foo[x_, baz[y_]] :> {x, y} ```
But in real-world use cases, this paradigm quickly exposes some unhandled edge cases, or cases where the evaluation becomes prohibitively expensive. Nowadays I use TypeScript, and this has ignited some curiosity into finding out if TS does anything to optimize for this in type inference.
With bidirection type checking, I think it only needs the unification when solving inserted implicits. So a plain dependent type theory wouldn't need it, but once you add implicit parameters, you do need it. They usually use pattern unification, which solves a subset of higher order unification problems, for those unification problems.
Obviously, since f(f) = f it should be a -> a as well. But to infer it without actually evaluating it, using the standard Hindley-Milner algorithm, we reason as follows: the two f's can have different specific types, so we introduce a new type variable b. The type of the first f will be a substitution instance of a -> a, the type of the second f will be a substitution instance of b -> b. We introduce a new type variable c for the return type, and solve the equation (a -> a) = ((b -> b) -> c), using unification. This gives us the substitution {a = (b -> b), c = (b -> b)}, and so we see that the return type c is b -> b.
But if we use pattern matching rather than unification, the variables in one of the two sides of the equation (a -> a) = ((b -> b) -> c) are effectively treated as constants referring to atomic types, not variables. Now if we treat the variables on the left side as constants, i.e. we treat a as a constant, we have to match b -> b to the constant a, which is impossible; the type a is atomic, the type b -> b isn't. If we treat the variables on the right side as constants, i.e. we treat b and c as constants, then we have to match a to both b -> b and c, and this means our substitution will have to make b -> b and c equal, which is impossible given that c is an atomic type and b -> b isn't.
I already disagree with this syntax.
Prolog does unification of the proof goal with the rule head. It's necessary there but not with datalog.
But I still agree with you about the capitalization. Some formats, like KIF, use a '?' prefix instead, and I've seen some HRF notations that mix the '?' prefix with non-KIF formatting (':-' operator and '.' terminator).