From 4378f58d3cab6e7b796f03a3b9861cdb8de46782 Mon Sep 17 00:00:00 2001
From: Cassie Jones <code@witchoflight.com>
Date: Thu, 26 Nov 2020 15:36:12 -0500
Subject: [PATCH] Fix some issues in the unification article

Thanks to Onel Harrison
---
 posts/2020/syntactic-unification.md | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/posts/2020/syntactic-unification.md b/posts/2020/syntactic-unification.md
index 342b62a..485b707 100644
--- a/posts/2020/syntactic-unification.md
+++ b/posts/2020/syntactic-unification.md
@@ -35,7 +35,7 @@ There are a few basic things we *need* to have.
 I'm going to write my examples in Python, so the types I'm going to work with are:
 
 - Variables: A `Var` class defined for this purpose.
-- Composite terms: Tuples and lists of terms.
+- Composite terms: Tuples of terms.
 - Atomic terms: Any Python type that can be compared for equality.
 
 The scheme example they demonstrate in the MicroKanren article uses variables, pairs, and arbitrary objects.
@@ -72,6 +72,8 @@ def unify(a, b):
     return None
 ```
 
+Here we return an empty environment because they're already equal, and nothing needs to be substituted.
+
 The variable cases can also be solved very easily.
 Trying to unify a variable with another term, we can just substitute that for the variable.
 When unifying `x = 1`, we get back `{ x: 1 }`.
@@ -178,7 +180,7 @@ We'll just always call it, and if the term isn't a key for the environment, we'l
 ```python
 def walk(env, term):
     if term in env:
-        term = term[env]
+        term = env[term]
     return term
 ```
 
@@ -213,7 +215,7 @@ Just change the `if` to a `while`!
 ```python
 def walk(env, term):
     while term in env:
-        term = term[env]
+        term = env[term]
     return term
 ```
 
@@ -299,6 +301,9 @@ We take our code that adds variables to the substitution, and add the occurs che
     if isinstance(a, Var):
         if occurs(a, b, env): return None
         return { **env, a: b }
+    if isinstance(b, Var):
+        if occurs(b, a, env): return None
+        return { **env, b: a }
 ```
 
 If we're using the occurs-check here, then we know a few things:
@@ -308,6 +313,7 @@ If we're using the occurs-check here, then we know a few things:
 
 This means that we can check if the literal variable `a` occurs literally in walked terms and subterms of `b`.
 If there's a variable in `b` that's a synonym of `a`, then it will walk to `a` because it was the result of walking.
+While it's safe to assume to that `a` has already been walked, note that we can't assume that `b` has already been walked since we're recursing over it.
 Then, the implementation looks like this:
 
 ```python
@@ -330,3 +336,8 @@ Now if we try...
 We correctly don't unify this.
 We've got sound unification over finite terms.
 This is useful to clean the situtation up, but I'm still a bit sad to see infinite terms go...
+
+----
+
+*Edit November 26, 2020.*
+Thanks to Onel Harrison for giving some clarity feedback and pointing out some typos.
-- 
2.43.2