Record 坦荡荡, Typeclass 常戚戚

前排提醒:你或许需要一个游标卡尺

这是一个类型类教程,尝试使用我改进过的 Literate Agda 后端生成网页 (如果想使用我改进的功能,请拉取 master 分支的 Agda 编译器然后 cabal install 编译。 我加的功能的使用说明见这个网页)。

为了让我能用我的手机正常显示自己的文章里的字符,本文会尽量使用非 Unicode 定义。

首先我们定义模块:

{-# OPTIONS --no-unicode #-}
{-# OPTIONS --without-K  #-}
{-# OPTIONS --cubical    #-}
module Typeclassopedia where

为了强迫自己事先熟悉 HoTT 的 Agda 实现, 我已经开始全面使用 HoTT-Agda 作为编程基础库(和标准库基本一致)。

(编辑于 2019 年 4 月:由于依赖冲突,现已改为对一个我自己写的基础库的使用)。

</a><pre class="Agda"><a id="720" class="Bound"> open import HoTT-Agda
比较自然数大小:

natEq : Nat -> Nat -> Bool natEq O O = true natEq (S ) O = false natEq O (S ) = false natEq (S n) (S m) = natEq n m – {-# BUILTIN NATEQUALS natEq #-}
不熟悉这个库的读者不必担心,本文用到的定义都属于看名字就知道的那种
(基本上在标准库或者内置库里面都有一个名字一样的,另外 `idp` 是 identity path,在代码上和 `refl` 的定义是一样的)。

泛化一个阶变量(Girard 悖论你好),免得到处写隐式参数:

variable i : Level
有个函数 `of-type` 和 Idris 的函数 `the` 语义一致:先传入一个类型,再传入这个类型的实例:

: (A : Type i) (u : A) -> A = of-type
HoTT-Agda 提供了这种便利的语法来间接使用 `of-type`:

= 233 :> Nat = lzero :> ULevel = unit :> Unit = idp :> (O == O)
## 实例参数

module InstanceArgument where
注:我的第一册书里译作*即时*参数,因为在英语中这个名字是一语双关的(
因为查找实例使用的算法比较快,所以 instance 此处有*即时*之意。
但这个特性又用于查找类型实例,所以 instance 又有*实例*之意),
现在决定改为取相对来说更内涵的含义。

实例参数类似隐式参数,只不过它们使用两层大括号:

postulate f : {{ x : Nat }} -> Nat
手动传值也是两层:

_ = f {{ 233 }} :> Nat
隐式参数一般是通过后面的参数往前推导得到的,实例参数则使用另一种方式:
**直接在上下文里查找变量。**

听起来很暴力,但其实也没有那么暴力啦,只有:

+ 放在 `instance` 代码块里的定义
+ 局部变量

才属于被查找的对象,我们称之为实例。
Agda wiki 说构造器也会,但目前看编译器的行为应该是不允许了。

放在 `instance` 代码块里的定义的例子:

– instance 代码块定义 instance rua : Nat rua = 233 – 喏,自动传入啦 _ = f :> Nat
局部变量:

= let jojo = O in f :> Nat = f :> Nat where jojo = O
如果作用域内有两个满足需求的实例,就会报错。

## 依赖记录

module DependentRecord where
这里*依赖*是形容词,不是动词。英文原文是 dependent record ,
表示后面成员的类型可以依赖前面成员的 `record` 。

Haskell 中的类型类使用 `class` 关键字定义,比如 `Eq` 类型类:

```haskell
class Eq t where
  (==) :: t -> t -> Bool
```

立即使用 `record` 表达:

record Eq {a} (A : Type a) : Type a where field === : A -> A -> Bool infixl 32 ===
由于 Agda 的 `record` 就是带参数的 `module` ,我们可以把它的成员定义 `open` 出来:

module EqAsExplicitArgument where open Eq
可以简单地看出,被 `open` 出来的 `_===_` 的类型:

<a id="2587" href="Typeclassopedia.html#2587" class="Function">_</a> <a id="2589" class="Symbol">=</a> <a id="2591" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="2597" href="HoTT-Agda.html#628" class="Function">:&gt;</a> <a id="2600" class="Symbol">(</a><a id="2601" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="2604" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a> <a id="2608" class="Symbol">-&gt;</a> <a id="2611" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a> <a id="2615" class="Symbol">-&gt;</a> <a id="2618" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a> <a id="2622" class="Symbol">-&gt;</a> <a id="2625" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a><a id="2629" class="Symbol">)</a>
要使用的话,先搞个实例,然后 Haskell 里当成 constraint 用的情况改成参数就是了:

<a id="DependentRecord.EqAsExplicitArgument.natEqInstance"></a><a id="2700" href="Typeclassopedia.html#2700" class="Function">natEqInstance</a> <a id="2714" class="Symbol">:</a> <a id="2716" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="2719" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a>
<a id="2727" href="Typeclassopedia.html#2700" class="Function">natEqInstance</a> <a id="2741" class="Symbol">=</a> <a id="2743" class="Keyword">record</a> <a id="2750" class="Symbol">{</a> <a id="2752" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="2758" class="Symbol">=</a> <a id="2760" href="Typeclassopedia.html#771" class="Function">natEq</a> <a id="2766" class="Symbol">}</a>
我们还可以使用优美的余模式(copattern):

<a id="DependentRecord.EqAsExplicitArgument.natEqInstance&#39;"></a><a id="2812" href="Typeclassopedia.html#2812" class="Function">natEqInstance&#39;</a> <a id="2827" class="Symbol">:</a> <a id="2829" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="2832" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a>
<a id="2840" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="2846" href="Typeclassopedia.html#2812" class="Function">natEqInstance&#39;</a> <a id="2861" class="Symbol">=</a> <a id="2863" href="Typeclassopedia.html#771" class="Function">natEq</a>
根据 `Eq` 类型类,定义不等于(就不 point-free 了,怕伤害不精通各种 arrow 操作的萌新):

<a id="DependentRecord.EqAsExplicitArgument.natNeq&#39;"></a><a id="2944" href="Typeclassopedia.html#2944" class="Function">natNeq&#39;</a> <a id="2952" class="Symbol">:</a> <a id="2954" class="Symbol">{</a><a id="2955" href="Typeclassopedia.html#2955" class="Bound">A</a> <a id="2957" class="Symbol">:</a> <a id="2959" href="Cubical.Core.Primitives.html#957" class="Function">Type</a> <a id="2964" href="Typeclassopedia.html#1103" class="Generalizable">i</a><a id="2965" class="Symbol">}</a> <a id="2967" class="Symbol">-&gt;</a> <a id="2970" class="Symbol">(</a><a id="2971" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="2974" href="Typeclassopedia.html#2955" class="Bound">A</a><a id="2975" class="Symbol">)</a> <a id="2977" class="Symbol">-&gt;</a> <a id="2980" href="Typeclassopedia.html#2955" class="Bound">A</a> <a id="2982" class="Symbol">-&gt;</a> <a id="2985" href="Typeclassopedia.html#2955" class="Bound">A</a> <a id="2987" class="Symbol">-&gt;</a> <a id="2990" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a>
<a id="2999" href="Typeclassopedia.html#2944" class="Function">natNeq&#39;</a> <a id="3007" href="Typeclassopedia.html#3007" class="Bound">eq</a> <a id="3010" href="Typeclassopedia.html#3010" class="Bound">a</a> <a id="3012" href="Typeclassopedia.html#3012" class="Bound">b</a> <a id="3014" class="Symbol">=</a> <a id="3016" href="Cubical.Data.Bool.Base.html#359" class="Function">not</a> <a id="3020" href="HoTT-Agda.html#1795" class="Function Operator">$</a> <a id="3022" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="3028" href="Typeclassopedia.html#3007" class="Bound">eq</a> <a id="3031" href="Typeclassopedia.html#3010" class="Bound">a</a> <a id="3033" href="Typeclassopedia.html#3012" class="Bound">b</a>
使用一下这个不等于:

<a id="3064" href="Typeclassopedia.html#3064" class="Function">_</a> <a id="3066" class="Symbol">:</a> <a id="3068" href="Agda.Builtin.Bool.html#154" class="InductiveConstructor">false</a> <a id="3074" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">==</a> <a id="3077" href="Typeclassopedia.html#2944" class="Function">natNeq&#39;</a> <a id="3085" href="Typeclassopedia.html#2700" class="Function">natEqInstance</a> <a id="3099" class="Number">0</a> <a id="3101" class="Number">0</a>
<a id="3107" class="Symbol">_</a> <a id="3109" class="Symbol">=</a> <a id="3111" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">idp</a>

<a id="3120" href="Typeclassopedia.html#3120" class="Function">_</a> <a id="3122" class="Symbol">:</a> <a id="3124" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a> <a id="3129" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">==</a> <a id="3132" href="Typeclassopedia.html#2944" class="Function">natNeq&#39;</a> <a id="3140" href="Typeclassopedia.html#2700" class="Function">natEqInstance</a> <a id="3154" class="Number">1</a> <a id="3156" class="Number">2</a>
<a id="3162" class="Symbol">_</a> <a id="3164" class="Symbol">=</a> <a id="3166" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">idp</a>
嗯,非常妙。

我们现在已经实现了一个非常不优美(不优美的原因是,我们要手动传入类型实例)
但比 Haskell 版本更灵活的类型类,并给它创建类型实例了!

module EqAsInstanceArgument where
在这个基础上,我们如果把那个 `(Eq A)` 做成实例参数,就可以让编译器自己去找类型实例,
实现 Haskell 中 `=>` 一样的效果了!

我们需要做两个手脚,首先 `open` 出来的 `_===_` 中的 `(Eq A)` 需要变成实例参数 `{{ Eq A }}`:

<a id="3459" class="Keyword">open</a> <a id="3464" href="Typeclassopedia.html#2326" class="Module">Eq</a> <a id="3467" class="Symbol">{{</a> <a id="3470" class="Symbol">...</a> <a id="3474" class="Symbol">}}</a>
没错,这个需求有点复杂,所以 Agda 专门做了个语法来简化这个流程。
当然,不代表我们不能手动实现这个语法糖实现的功能:

<a id="3557" class="Keyword">module</a> <a id="StupidImplementation"></a><a id="3564" href="Typeclassopedia.html#3564" class="Module">StupidImplementation</a>
       <a id="3596" class="Symbol">{</a><a id="3597" href="Typeclassopedia.html#3597" class="Bound">i</a><a id="3598" class="Symbol">}</a> <a id="3600" class="Symbol">{</a><a id="3601" href="Typeclassopedia.html#3601" class="Bound">A</a> <a id="3603" class="Symbol">:</a> <a id="3605" href="Cubical.Core.Primitives.html#957" class="Function">Type</a> <a id="3610" href="Typeclassopedia.html#3597" class="Bound">i</a><a id="3611" class="Symbol">}</a> <a id="3613" class="Symbol">{{</a> <a id="3616" href="Typeclassopedia.html#3616" class="Bound">eq</a> <a id="3619" class="Symbol">:</a> <a id="3621" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="3624" href="Typeclassopedia.html#3601" class="Bound">A</a> <a id="3626" class="Symbol">}}</a> <a id="3629" class="Keyword">where</a>
  <a id="3641" class="Keyword">open</a> <a id="3646" class="Keyword">module</a> <a id="EqInstances"></a><a id="3653" href="Typeclassopedia.html#3653" class="Module">EqInstances</a> <a id="3665" class="Symbol">=</a> <a id="3667" href="Typeclassopedia.html#2326" class="Module">Eq</a> <a id="3670" href="Typeclassopedia.html#3616" class="Bound">eq</a> <a id="3673" class="Keyword">public</a>
其次我们的类型实例需要被 `instance` 修饰:

<a id="3726" class="Keyword">instance</a>
  <a id="DependentRecord.EqAsInstanceArgument.natEqInstance"></a><a id="3741" href="Typeclassopedia.html#3741" class="Function">natEqInstance</a> <a id="3755" class="Symbol">:</a> <a id="3757" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="3760" href="Agda.Builtin.Nat.html#165" class="Datatype">Nat</a>
  <a id="3770" href="Typeclassopedia.html#3741" class="Function">natEqInstance</a> <a id="3784" class="Symbol">=</a> <a id="3786" class="Keyword">record</a> <a id="3793" class="Symbol">{</a> <a id="3795" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="3801" class="Symbol">=</a> <a id="3803" href="Typeclassopedia.html#771" class="Function">natEq</a> <a id="3809" class="Symbol">}</a>
嗯,由于我们已经把 `Eq` 以实例参数形式 `open` 出来,就用不了余模式了 QAQ。

然后再试试用这个类型类实现不等于。先显式传入,找找感觉(
实例参数必须 introduce 一个变量,不知道为什么。如果不想写,命名为下划线就是):

<a id="DependentRecord.EqAsInstanceArgument.natNeq&#39;"></a><a id="3952" href="Typeclassopedia.html#3952" class="Function">natNeq&#39;</a> <a id="3960" class="Symbol">:</a> <a id="3962" class="Symbol">{</a><a id="3963" href="Typeclassopedia.html#3963" class="Bound">A</a> <a id="3965" class="Symbol">:</a> <a id="3967" href="Cubical.Core.Primitives.html#957" class="Function">Type</a> <a id="3972" href="Typeclassopedia.html#1103" class="Generalizable">i</a><a id="3973" class="Symbol">}</a> <a id="3975" class="Symbol">-&gt;</a> <a id="3978" class="Symbol">{{</a><a id="3980" href="Typeclassopedia.html#3980" class="Bound">_</a> <a id="3982" class="Symbol">:</a> <a id="3984" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="3987" href="Typeclassopedia.html#3963" class="Bound">A</a><a id="3988" class="Symbol">}}</a> <a id="3991" class="Symbol">-&gt;</a> <a id="3994" href="Typeclassopedia.html#3963" class="Bound">A</a> <a id="3996" class="Symbol">-&gt;</a> <a id="3999" href="Typeclassopedia.html#3963" class="Bound">A</a> <a id="4001" class="Symbol">-&gt;</a> <a id="4004" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a>
<a id="4013" href="Typeclassopedia.html#3952" class="Function">natNeq&#39;</a> <a id="4021" class="Symbol">{{</a><a id="4023" href="Typeclassopedia.html#4023" class="Bound">eq</a><a id="4025" class="Symbol">}}</a> <a id="4028" href="Typeclassopedia.html#4028" class="Bound">a</a> <a id="4030" href="Typeclassopedia.html#4030" class="Bound">b</a> <a id="4032" class="Symbol">=</a> <a id="4034" href="Cubical.Data.Bool.Base.html#359" class="Function">not</a> <a id="4038" href="HoTT-Agda.html#1795" class="Function Operator">$</a> <a id="4040" href="Typeclassopedia.html#2371" class="Field Operator">_===_</a> <a id="4046" class="Symbol">{{</a><a id="4048" href="Typeclassopedia.html#4023" class="Bound">eq</a><a id="4050" class="Symbol">}}</a> <a id="4053" href="Typeclassopedia.html#4028" class="Bound">a</a> <a id="4055" href="Typeclassopedia.html#4030" class="Bound">b</a>
自动传入(终于能用上运算符语法了,嘤嘤嘤):

<a id="DependentRecord.EqAsInstanceArgument.natNeq"></a><a id="4098" href="Typeclassopedia.html#4098" class="Function">natNeq</a> <a id="4105" class="Symbol">:</a> <a id="4107" class="Symbol">{</a><a id="4108" href="Typeclassopedia.html#4108" class="Bound">A</a> <a id="4110" class="Symbol">:</a> <a id="4112" href="Cubical.Core.Primitives.html#957" class="Function">Type</a> <a id="4117" href="Typeclassopedia.html#1103" class="Generalizable">i</a><a id="4118" class="Symbol">}</a> <a id="4120" class="Symbol">-&gt;</a> <a id="4123" class="Symbol">{{</a><a id="4125" href="Typeclassopedia.html#4125" class="Bound">_</a> <a id="4127" class="Symbol">:</a> <a id="4129" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="4132" href="Typeclassopedia.html#4108" class="Bound">A</a><a id="4133" class="Symbol">}}</a> <a id="4136" class="Symbol">-&gt;</a> <a id="4139" href="Typeclassopedia.html#4108" class="Bound">A</a> <a id="4141" class="Symbol">-&gt;</a> <a id="4144" href="Typeclassopedia.html#4108" class="Bound">A</a> <a id="4146" class="Symbol">-&gt;</a> <a id="4149" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a>
<a id="4158" href="Typeclassopedia.html#4098" class="Function">natNeq</a> <a id="4165" href="Typeclassopedia.html#4165" class="Bound">a</a> <a id="4167" href="Typeclassopedia.html#4167" class="Bound">b</a> <a id="4169" class="Symbol">=</a> <a id="4171" href="Cubical.Data.Bool.Base.html#359" class="Function">not</a> <a id="4175" href="HoTT-Agda.html#1795" class="Function Operator">$</a> <a id="4177" href="Typeclassopedia.html#4165" class="Bound">a</a> <a id="4179" href="Typeclassopedia.html#2371" class="Field Operator">===</a> <a id="4183" href="Typeclassopedia.html#4167" class="Bound">b</a>
运算符重载了解一下,自定义优先级结合性了解一下:

<a id="4228" class="Keyword">infixl</a> <a id="4235" class="Number">32</a> <a id="4238" href="Typeclassopedia.html#4248" class="Function Operator">_=/=_</a>
<a id="DependentRecord.EqAsInstanceArgument._=/=_"></a><a id="4248" href="Typeclassopedia.html#4248" class="Function Operator">_=/=_</a> <a id="4254" class="Symbol">:</a> <a id="4256" class="Symbol">{</a><a id="4257" href="Typeclassopedia.html#4257" class="Bound">A</a> <a id="4259" class="Symbol">:</a> <a id="4261" href="Cubical.Core.Primitives.html#957" class="Function">Type</a> <a id="4266" href="Typeclassopedia.html#1103" class="Generalizable">i</a><a id="4267" class="Symbol">}</a> <a id="4269" class="Symbol">-&gt;</a> <a id="4272" class="Symbol">{{</a><a id="4274" href="Typeclassopedia.html#4274" class="Bound">_</a> <a id="4276" class="Symbol">:</a> <a id="4278" href="Typeclassopedia.html#2326" class="Record">Eq</a> <a id="4281" href="Typeclassopedia.html#4257" class="Bound">A</a><a id="4282" class="Symbol">}}</a> <a id="4285" class="Symbol">-&gt;</a> <a id="4288" href="Typeclassopedia.html#4257" class="Bound">A</a> <a id="4290" class="Symbol">-&gt;</a> <a id="4293" href="Typeclassopedia.html#4257" class="Bound">A</a> <a id="4295" class="Symbol">-&gt;</a> <a id="4298" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a>
<a id="4307" href="Typeclassopedia.html#4307" class="Bound">a</a> <a id="4309" href="Typeclassopedia.html#4248" class="Function Operator">=/=</a> <a id="4313" href="Typeclassopedia.html#4313" class="Bound">b</a> <a id="4315" class="Symbol">=</a> <a id="4317" href="Cubical.Data.Bool.Base.html#359" class="Function">not</a> <a id="4321" href="HoTT-Agda.html#1795" class="Function Operator">$</a> <a id="4323" href="Typeclassopedia.html#4307" class="Bound">a</a> <a id="4325" href="Typeclassopedia.html#2371" class="Field Operator">===</a> <a id="4329" href="Typeclassopedia.html#4313" class="Bound">b</a>
相信此时浏览器等宽字体设置为 Fira Code 的读者已经被爽到了(噫)。

简单地调用,证明一下性质:

<a id="4403" href="Typeclassopedia.html#4403" class="Function">_</a> <a id="4405" class="Symbol">:</a> <a id="4407" href="Agda.Builtin.Bool.html#154" class="InductiveConstructor">false</a> <a id="4413" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">==</a> <a id="4416" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">O</a> <a id="4418" href="Typeclassopedia.html#4248" class="Function Operator">=/=</a> <a id="4422" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">O</a>
<a id="4428" class="Symbol">_</a> <a id="4430" class="Symbol">=</a> <a id="4432" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">idp</a>

<a id="4441" href="Typeclassopedia.html#4441" class="Function">_</a> <a id="4443" class="Symbol">:</a> <a id="4445" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a> <a id="4450" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">==</a> <a id="4453" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">O</a> <a id="4455" href="Typeclassopedia.html#4248" class="Function Operator">=/=</a> <a id="4459" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">S</a> <a id="4461" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">O</a>
<a id="4467" class="Symbol">_</a> <a id="4469" class="Symbol">=</a> <a id="4471" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">idp</a>
完美!我们有类型类了!

嗯,数学作业要写不完了 QAQ