你造么，这是我当年在本地最好的初中上学的时候班主任对我说的话。

现在把它送给你

最后祝你 身体健康

标题我都想好了，《地区头校班主任对学生说了这么一句话，竟改变了他的一生！》

哈哈哈哈哈哈 闹着玩的，我又不做媒体

既然 iseki 都被大佬喷了，那我就在这里直播 y=1; x=y=z 的 unify 过程 #PLT

首先说说我们的目标是求得 x=1; y=1; z=1，使用的方法是 unification —— 利用相等关系，让两个 Value(Val/Var) 在一个 State 里实际上划上等号

而一个 Var 呢，我们可以认为是一个 "Symbol"，它的 equals 实现为全等 (x === y)，就可以了。

microKanren 有 six primitives: State, Variable, fresh(introduce), Eq, Either, Both
前三个是最基础的 unification 需求，后三个是关系式编程(relational programming) 里最重要的关系

毕竟是在 Telegram 直接写了，我就不说 Either 和 Both 这种高级操作了（它们能 satisfyIn 的 state 都可能不只一个）

fun main(vararg args: String) {
  val xyz = State()
  xyz.intro("x", "y", "z") {
    val (x, y, z) = it
    y.eq(Val(1))
    x.eq(y); y.eq(z)
  }
  println(xyz) //State{x: 1, y: 1, z: 1}
}

在 Kotlin 里面以 EDSL 的风格 去完成……
首先我们依赖的需要知道啥东西能够 unify 又怎么去 unify，或者说我们得对 Value 的子类型实现 unifyIn(state, other) 操作

我们知道相等关系是有对称性(symmetric) 的 (x=y, y=x)，所以“解构”式的操作只需要有一边定义就 OK 了，然后因为 Kotlin 是强类型的可以加入类型检查。

typealias Consumer<T> = (T) -> Unit
typealias MonoTriple<T> = Triple<T, T, T>
typealias MonoPair<T> = Pair<T, T>

typealias StateMap = MutableMap<Value.Var, Any?>
typealias Variable = Value.Var

class State(private val map: StateMap = mutableMapOf()): StateMap by map {
  fun intro(x1: String, x2: Sting, op: Consumer<MonoPair<Variable>>) {
    val xs = bind(x1, x2)
    op(Pair(xs[0], xs[1]))
  }
  fun intro(x1: String, x2: String, x3: String, op: Consumer<MonoTriple<Variable>>) {
    val xs = bind(x1, x2, x3)
    op(Triple(xs[0], xs[1], xs[2]))
  }
  fun bind(vararg names: String): List<Value.Var> {
    val variables = names.map(::Variable)
    for (variables
    return variables
  }
  override fun toString() = "State$map"
}

interface Unifible<T> {
  fun unifyIn(state: State, other: Unifible<T>)
}

sealed class Value(open val value: Any?) {
  data class Val(value: Any?): Value(value) {
    override fun toString() = "Val($value)"
  }
  data class Var(val name: String, val binding: State) {
    override fun equals(other: Any?) = this === other
    override fun hashCode() = super.hashCode()
    override fun toString() = "Var($name)"
  }
}

艹我写不下去了，太长了

具体怎么实现 unify 以及 unify 的对称性的代码复用留给 iseki 大佬自己研究去吧，我重写我的 ParserKt 去了……

提示一下，
Var unify with Value 都是 assignIn(state, other.value)
Val unify with Value 都是 check，如果 equals 就直接完了，否则 exception
对称性 this unify other; other unify this 的时候出异常可以 catch 然后上 has-exception logical or
此外我写错了一些地方，草

你可是自己说要学习的哦 🌚

OK，plt圈子都是大佬，我这种萌新瑟瑟发抖就行了

傻瓜，这有什么大佬的……

@ice1000 那个是真大佬，人家现在写的直白了，但绝对不会给你额外的解释

我不一样，如果你有不懂的随时找我
只要我明白你就可以随便请教喽（虽然我懂得不多呃）

unify 就是像 ES6 的 let [a, b] = [1, 2] 一样，利用相等关系解出实际值
相等关系具有传递性(transitvity) 和对称性(symmetric) （貌似是这么拼？）

那个 SSA:Static Single Assignment 也很有意思

其实你学的越多，越发现关系式和很多技术，包括函数式编程的许多理念都有很大关系

比如说范畴论，举出一个最简单的例子就是七大姑八大姨…… 一个家庭的范畴
然后换到关系式里，你可以问 『侄女之父 = A之兄』里的 A 和你是什么关系，而求解的过程必须得有 P=A之兄 的解构过程吧？
unify 就可以利用这个等号从 P 里面提出 A （A = P之弟）
一个不是很准确的例子。

你去看那个 Hello, declarative world，很好看

Ruby 写的，强烈建议读三遍

#Haha #life #China