日记 2019-10-13 Smarter Witnesses for Type Classes
Smarter Witnesses for Type Classes¶
昨天看导师的讲typeclass实现的博客, 第一段就是
The awareness of low-level implementation details brings the appreciation of an abstraction and the intuitive explanation for it.
大概这会成为未来两个月内的重要激励之一.
然后, 对于type class constraint的witnesses, 我想出来一个新的算法, 这里记录一下.
Notation¶
基础是利用dict passing实现type classes.
我们用简单的类ML代码来描述(实际上是近期设计的Remu的语法):
type a eq = {
eq : (a, a) -> bool
}
val (==) : {a eq} -> (a, a) -> bool
let (==) = fn eq -> eq.eq
1 == 2
其中 {a}
表示implcit argument.
不用在意二元运算函数的signature, 下面不会提到.
Instance Resolution & Variables As Instances¶
观察下面这段代码,
val f : {a} -> b
let f = fn ...
val g : b
let g = ...
val func : a -> a -> ...
func f g
可以知道 f
和 g
的类型(即 {a} -> b
和 b
会进行一次unification,
此时可通过变换 func f g
的AST来查找instance.
用简化的AST表示上述过程, 就是 func f g
的AST从
App(
App(
Sym(func)[typ1],
Sym(f)[type2], # type1 = {a} -> b
)[type3],
Sym(g)[type4]
)[type5]
变成
App(
App(
Sym(func)[type1],
App(
Sym(f)[type2], # type1 = a -> b
SearchInstance(type0) # type0 = a
)[type2_] # type2 = b
)[type3],
Sym(g)[type4]
)[type5]
只需在 SearchInstance
中利用scoping信息, 在可访问的scope内,
找出一个类型最 general 的variable, 其类型能和 type1
的 domain 部分
进行unification.
“The Most General Instance” Problem & “Overlapping Instance” Problem¶
这里主要问题是如何找类型 最general 的instance:
作用域内可能存在有多个variable(i.e. instance), 使得其类型均可与implicit argument做unification; 此时, 应该挑出一个受约束最小的instance, 否则, 存在多个备选的instance之间存在重叠(overlapping instances).
算法的主要思路是, 通过定义一个类似subtyping(but actually not)的类型运算, 记为 <
,
其中 a < b
表示 a, b
进行unification之后, b不发生更新.
而 <
读作”小于”, 则基于”小于”所实现的 minimum
可以求出最general的instance.
伪代码(也是实际代码…)如下:
def minimum(implicit_argument_type, scope):
most_general_type = implicit_argument_type
most_general_instance = None
for instance, type in scope.list_typed_variables:
if most_general_type < type:
most_general_type = type
most_general_instance = instance
elif type < most_general_type == False:
raise "Overlapping Instance"
if most_general_instance == None:
raise "Cannot resolve type class instance"
return most_general_instance
读者可以发现, 在算法中, overlapping instances的问题被自动地解决了.
overlapping的情形, 实际上是两个备选instance的类型 a, b
满足
assert a < b == false
assert b < a == false
优化¶
如果全部变量都参与instance resolution, 编译器的开销就太大了. 所以用`instance`关键字mark一下.
val show_int : 'a show
let show_int = {show = ...}
instance show_int # allow treating `a` as an instance
val show : {a show} -> a -> string
let show = fn show_inst value = show_inst.show value
show 1
该算法和相应语言设计的好处¶
- 简单轻量: 不需要引入term unification, 且对于HM的扩展非常小.
- 语法上方便初学者理解type class实现的本质, 使用上依然承诺简洁, 不像OCaml和F#一样需要大量boilerplate.
- 不引入Haskell那样的
class
和instance
语言构造, 使得core lang体积减小. - 自动的消除了orphan instance的问题; 毕竟, instance就是作用域内可访问的变量.
不足之处¶
Haskell里多个class的约束 (ClsA a, ClsB a) => ...
, 其顺序是insignificant的.
这个问题我没有解决, 但打算用row polymorphisms来搞:
也就是把
val adhoc_func : {a clsA, a clsB} -> ...
转成
type a bothClses = a clsA with a clsB
val multicls : {a clsA} -> {a clsB} -> a bothClses
let multicls = fn instA instB -> instA with instB
val adhoc_func : {a bothClses} -> ...