The key observation to me was that the traditional Datalog/Prolog way of unifying is through syntactic equality, which is a bit too simple to express the kind of equality needed in Rust and elsewhere. You can express it in Datalog, but as it gets farther away from the source, error-generation suffers.
"Insightful observation" doesn't quite do it justice ;) There's a whole discipline in discrete math dealing with the possibilities and limitations of equational theories and reasoning. And it could be said their limitations gave rise to the various constraint formalisms that were introduced in the 80s and 90s as Prolog extensions and sometimes (syntactic) generalizations.
Well then, please elaborate because I know nothing of the discipline you describe and it certainly sounds interesting (though it also sounds a little fussy).
I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;) I can point you to some classic works/authors in the field, though (and I'm sure some fellow HNers can provide some more): Gauss, Knuth, Bendix, Gröbner, Buchberger, Bachmaier, Euclid, Ganzinger, Davis, Putnam, Robinson, and Colmerauer for Prolog 2. There are also category theory papers relevant to reasoning about data structures, and of course Damas, Hindley, Miller for type theories. The way is the goal here.
> I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;)
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
> The key observation to me was that the traditional Datalog/Prolog way of
unifying is through syntactic equality, which is a bit too simple to express
the kind of equality needed in Rust and elsewhere.
I was surprised by this comment because Horn logic, although syntactically
restricted, has Universal Turing Machine expressivity and it's difficult to
see what Rust needs to do that needs more expressive power than a UTM(!).
Reading the post I understand that the author is speaking about unification in
particular, not Horn clauses and resolution, where unification is typically
used, however there is still a subtle error, which is the identificatin of
unification as "syntactic equality". While unification can be used to decide
whether two terms are syntacticall equal, in the sense that if they are, they
will unify, unification on its own is not syntactic equality.
First of all, say that T₁ = f(χ) and T₂ = f(α) are two terms. Note that χ is a
variable and α is a constant. Clearly T₁ ≠ T₂ and that is true for "syntactic"
equality, because χ ≠ α.
Now suppose that θ = {χ/α} is a substitution of the variables in {T₁,T₂}.
Now, θT₁ = Τ₂. Read θT₁ as "T₁ with θ applied". In other words, T₁ is equal to
T₂ _if_ χ is substituted with α. A unification algorithm (normally, Robinson's
unification algorithm) is used to establish that two terms are equal given a
substitution of their variables. In particular, a substitution of variables
that allows two terms to unify is a "unifier". Note that unifiers can be
composed, so for example, if T₃ = f(χ,υ), T₄ = f(α,β), φ = {χ/α} and ψ = {υ/β}
then φT₃ ≠ T₄ but φψT₃ = T₄.
I noticed in the examples of Rust-in-Prolog given in the link above that the
author subtly fudges the syntax of Prolog, for example Bar, which is normally
a variable in Prolog, is used as a constant, whereas ?A and ?B which would be
not-variables in Prolog (but partially ground terms) are used as variables. I
wonder if this is part of a now-divide-by-zero step in the author's reasoning,
that I can't figure out exactly because I don't know any Rust. For example,
what is "?A" and what is "Bar" in the context of Rust?
In any case, the author is of course correct that unification is not type
equality- but then, nothing is except for type equality. As far as I
understand these things anyway- I'm not a type nerd. Bottom line, you can't
implement "type equality" as any other kind of "equality" and you'll have to
jump through hoops -the hoops of defining your higher-level notion of
equality- in what ever language you choose.
you'll have to jump through hoops -the hoops of defining your higher-level notion of equality- in what ever language you choose.
Right. The author is just disappointed that Prolog does have a built-in "equality" that isn't the equality they want. A nice solution in Prolog would be to write a meta-interpreter or to do term rewriting on the input program. This would allow the author to write
Yes. I just don't see why this is such a big hassle. Particularly because -I'm guessing- whatever the Rust compiler does to decide type equality can't be less hassle-y than that.
But, I might misunderstand the problem since, again, I don't know Rust.
Comments
Niko Matsakis had an insightful observation about this approach in a similar post (which is referenced by OP):
http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowe...
The key observation to me was that the traditional Datalog/Prolog way of unifying is through syntactic equality, which is a bit too simple to express the kind of equality needed in Rust and elsewhere. You can express it in Datalog, but as it gets farther away from the source, error-generation suffers.
"Insightful observation" doesn't quite do it justice ;) There's a whole discipline in discrete math dealing with the possibilities and limitations of equational theories and reasoning. And it could be said their limitations gave rise to the various constraint formalisms that were introduced in the 80s and 90s as Prolog extensions and sometimes (syntactic) generalizations.
Well then, please elaborate because I know nothing of the discipline you describe and it certainly sounds interesting (though it also sounds a little fussy).
I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;) I can point you to some classic works/authors in the field, though (and I'm sure some fellow HNers can provide some more): Gauss, Knuth, Bendix, Gröbner, Buchberger, Bachmaier, Euclid, Ganzinger, Davis, Putnam, Robinson, and Colmerauer for Prolog 2. There are also category theory papers relevant to reasoning about data structures, and of course Damas, Hindley, Miller for type theories. The way is the goal here.
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
This seems to be a newer version with similar contents but different authors: http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
This is specific to unification and not to broader equational reasoning.
Thanks.
I was surprised by this comment because Horn logic, although syntactically restricted, has Universal Turing Machine expressivity and it's difficult to see what Rust needs to do that needs more expressive power than a UTM(!).
Reading the post I understand that the author is speaking about unification in particular, not Horn clauses and resolution, where unification is typically used, however there is still a subtle error, which is the identificatin of unification as "syntactic equality". While unification can be used to decide whether two terms are syntacticall equal, in the sense that if they are, they will unify, unification on its own is not syntactic equality.
First of all, say that T₁ = f(χ) and T₂ = f(α) are two terms. Note that χ is a variable and α is a constant. Clearly T₁ ≠ T₂ and that is true for "syntactic" equality, because χ ≠ α.
Now suppose that θ = {χ/α} is a substitution of the variables in {T₁,T₂}. Now, θT₁ = Τ₂. Read θT₁ as "T₁ with θ applied". In other words, T₁ is equal to T₂ _if_ χ is substituted with α. A unification algorithm (normally, Robinson's unification algorithm) is used to establish that two terms are equal given a substitution of their variables. In particular, a substitution of variables that allows two terms to unify is a "unifier". Note that unifiers can be composed, so for example, if T₃ = f(χ,υ), T₄ = f(α,β), φ = {χ/α} and ψ = {υ/β} then φT₃ ≠ T₄ but φψT₃ = T₄.
I noticed in the examples of Rust-in-Prolog given in the link above that the author subtly fudges the syntax of Prolog, for example Bar, which is normally a variable in Prolog, is used as a constant, whereas ?A and ?B which would be not-variables in Prolog (but partially ground terms) are used as variables. I wonder if this is part of a now-divide-by-zero step in the author's reasoning, that I can't figure out exactly because I don't know any Rust. For example, what is "?A" and what is "Bar" in the context of Rust?
In any case, the author is of course correct that unification is not type equality- but then, nothing is except for type equality. As far as I understand these things anyway- I'm not a type nerd. Bottom line, you can't implement "type equality" as any other kind of "equality" and you'll have to jump through hoops -the hoops of defining your higher-level notion of equality- in what ever language you choose.
Right. The author is just disappointed that Prolog does have a built-in "equality" that isn't the equality they want. A nice solution in Prolog would be to write a meta-interpreter or to do term rewriting on the input program. This would allow the author to write
and have it be interpreted asYes. I just don't see why this is such a big hassle. Particularly because -I'm guessing- whatever the Rust compiler does to decide type equality can't be less hassle-y than that.
But, I might misunderstand the problem since, again, I don't know Rust.