既然 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

（剧透警告）

《平凡的世界》 虽然讲的人都不太平凡，但居然末尾是个悲剧，死了癌症了很多人，我真的不再觉得看那个电视剧有啥意思了

剧透一点意思都没有，被人强行剧透了很无聊

是我爸剧透的。开始他说是悲剧，后来又说谁谁谁死了。
我讨厌看那种情况，所以以后干脆就别看算了，我还以为只是风波迭起，没想到真能全写死

不过《平凡的世界》是部好剧，向大家推荐。 #recomended #media
同样，《庆余年》和十台、十二台的科普也是极好的
中央一台 12:30 起有看