类型体操指北 (Haskell)

作为类型系统最复杂的非DT语言之一, Haskell有着强大的类型编程能力. 我们将从最简单的构造开始展示这些能力, 本文假定读者了解Haskell的基本语法. 本文使用的版本是GHC 9.0.2, 但在较旧的版本上这些代码也能运行.

首先我们需要打开以下拓展

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

并导入

1	`import Data.Kind(Type)`

读者不必完全熟悉这些拓展, 我们会慢慢介绍一些特别的语法.

Value, Type, Kind

我们已经很熟悉Haskell中的一系列值(value), 比如 2,3,True,(\x -> x * 2). 它们有各自所属的类型(type)

2             :: Num a => a 
3             :: Num a => a
True          :: Bool
(\x -> x * 2) :: forall a. Num a => a -> a

一个自然的想法是把类型也看作另一种值, 它们也有自己所属的类型, 此时这个类型就可以称为 Kind. 比如我们会这样记

1
2
3

Num a => a                :: Type
Bool                      :: Type 
forall a. Num a => a -> a :: Type

其中 Type 是这样一种"类型", 它的元素是所有类型, 比如 Int, Int -> Int, forall a. Num a => a.

Maybe 是 Type 的元素吗? 不是, 但 Maybe Int 是, 所以 Maybe 实际是一个 Type 到 Type 的函数.

Int    :: Type
Maybe  :: Type -> Type
[]     :: Type -> Type
(->)   :: Type -> Type -> Type
Either :: Type -> Type -> Type

在 ghci 中使用 :k t 查看类型t所属的kind, 输出结果中 Type 被记作 *.

我不知道 Kind 有什么好翻译, 所以干脆不翻译.

类型层面的ADT

读者一定很熟悉一些Haskell中的ADT, 比如

1	`data Bool = True \| False`

其中 Bool 是类型, True 和 False 是值, 我们希望把它们统一提高一层, 这样我们就能在类型编程时用上它们. DataKinds 拓展允许我们这样做. 只要开启这个拓展, Haskell就会自动为所有的ADT(包括自定义的和其他模块里的)创建一个高一层的副本. 以 Bool 为例, 打开 DataKinds 时, Haskell自动创建一个Kind Bool, 两个类型 'True 'False :: Bool, 这里单引号是用于区分值True值False和类型'True和类型'False(另一方面你永远不用担心类型Bool和KindBool会混淆). 这样就有,

'True                :: Bool
'False               :: Bool
'[]                  :: [a]
'[ 'True, 'False ]   :: [Bool]
'True ': '[]         :: [Bool] -- 这里需要打开 TypeOperators
'Just True           :: Maybe Bool 
'Just 'True          :: Maybe Bool -- 注意这两个 Maybe Bool 实际上不同
'Just Bool           :: Maybe Type
'( 'True, 'Nothing ) :: (Bool, Maybe a)

自然数

我们熟悉的数字类型 Int, Integer, Float, Double 都不是ADT, 无法被 DataKinds 提升, 我们自然的需求是搞一个能用的数字类型. 最简单的当然是我们的自然数.

1	`data Nat = Z \| S Nat deriving Show`

其中 Z 代表数字 \(0\), S k 代表自然数 \(k+1\), 其中这样我们可以用 S (S (S Z)) 代表数字 \(3\). 读者可以尝试自行实现自然数上的加法和乘法以作练习.

类型层面的数据结构

异构列表(Heterogeneous List)

类型列表, Haskell 中的列表类型 [] 就是 ADT, 所以它可以被自然提高到类型层面. 我们非常关注Kind [Type] , 它实际是一个由类型构成的列表. 有了这个它, 我们可以在 Haskell 中实现异构列表(Heterogeneous List).

infixr 4 :+:
data HList :: [Type] -> Type where -- 这里需要打开 GADTs 和 KindSignatures
  HNil  :: HList '[]
  (:+:) :: t -> HList ts -> HList (t ': ts)

这里给不熟悉 GADT 拓展的朋友们解释一下, 第一行是声明运算符的运算级, 没什么好说的; 第二行声明了 HList 的 Kind, 接受一个类型列表, 返回一个类型; where 之后的两行给出两个构造器, HNil 相当于一个空列表, :+: 相当于将一个元素添加到列表头. 重点在于构造器的类型, GADT 拓展的用途就是允许我们更精细地控制类型, :+: 的类型告诉我们, 它接受两个参数, 一个是任意类型 t 的元素, 一个是 HList ts 的元素(其中 ts 是任意类型列表), 然后返回一个 HList (t ': ts).

于是,

1 2	`1 :+: True :+: Just 2 :+: Nothing :+: HNil :: (Num n1, Num n2) => HList '[n1, Bool, Maybe n2, Maybe a]`

为了让我们的 HList 能够正常使用, 我们先来定义一些常用函数. 首先是 show,

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show t, Show (HList ts)) => Show (HList (t ': ts)) where
  show (x :+: xs) = show x ++ " :+: " ++ show xs

这段代码实质上是利用 Haskell 的类型类机制在类型上进行模式匹配, 每一个模式都要提供一个instance, 注意这里 Haskell 不会提供模式完整性检查, 请自己确保自己定义的instance能覆盖所有可能的情况.

现在我们试着来做一下HList的拼接, 首先考虑类型要怎么变化, 显然链表拼接的类型为

1	`hAppend :: HList ls1 -> HList ls2 -> HList (ls1 ++ ls2)`

其中 ++ 是普通列表的拼接, 但是 DataKinds 不会帮我们把一般的函数提升到类型层面, 我们需要手动实现类型列表的拼接.

1
2
3

type family TAppend (xs :: [Type]) (ys :: [Type]) :: [Type] where
  TAppend '[] ys = ys
  TAppend (x ': xs) ys = x ': TAppend xs ys

这里毫无疑问要使用 TypeFamilies 拓展, 这个拓展允许我们来写类型层面的函数. 一些语言(比如C++, Scala3)有type family类似物, 这些语言的类型系统往往都是图灵完备的.

有了 TAppend , 我们再使用先前的技巧在类型上进行模式匹配

class HAppend (ts1 :: [Type]) where
  hAppend :: HList ts1 -> HList ts2 -> HList (TAppend ts1 ts2)
  
instance HAppend '[] where
  hAppend HNil ys = ys
  
instance (HAppend ts) => HAppend (t ': ts) where
  hAppend (x :+: xs) ys = x :+: hAppend xs ys

这里 class 起到了标注类型的作用, instance 相当于按模式依次进行实现.

现在使用一个例子来展示异构列表的作用.

众所周知, Haskell中的 sequence 非常常用, 它的类型是 sequence :: Monad m => [m a] -> m [a](这不是最一般的类型, 但我们现在只考虑这个特化版本). 形象一点说就是把列表里的m"翻"出来. 这里用的是一般列表, 我们实际可以写一个异构列表版本的 sequence, 这里称为 hSequence. 先考虑hSequence的类型是什么, 一个自然的想法是

1	`hSequence :: Moand m => HList (map m ts) -> m (HList ts)`

同样我们需要把 map 提到类型层面

1
2
3

type family Map (f :: Type -> Type) (ts :: [Type]) :: [Type] where
  Map f '[] = '[]
  Map f (t ': ts) = f t ': Map f ts

然后定义函数

1
2
3

hAppend :: HList ts1 -> HList ts2 -> HList (TAppend ts1 ts2)
hAppend HNil ys = ys
hAppend (x :+: xs) ys = x :+: hAppend xs ys

大功告成.

定长列表(Vector)

我们经常面对下标越界异常, 是否有办法可以在编译期完全杜绝下标越界呢? 答案是肯定的, 这首先需要我们构造一个类型, 这个类型能携带列表的长度信息.

infixr 4 :::
data Vect :: Nat -> Type -> Type where
  VNil :: Vect 'Z a
  (:::) :: a -> Vect n a -> Vect ('S n) a

这里我们用到了之前DataTypes帮我们提升的自然数Kind.

用自然语言翻译一下:

1
2
3

类型 Vect n a 代表长度为 n 元素类型为 a 的列表构成的类型
  VNil 是空列表, 所以它的类型是 Vect 'Z a (记得我们之前把 'Z 定作 0)
  (x ::: xs) 相当于把元素 x 拼到列表 xs 前面, 并且这里列表的长度增长了一

同样按照上面的例子, 溜一下列表拼接

type family (:+) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :+ n = n
  ('S m) :+ n = 'S (m :+ n)

vAppend :: Vect m a -> Vect n a -> Vect (m :+ n) a
vAppend VNil ys = ys
vAppend (x:::xs) ys = x ::: vAppend xs ys

这里顺便定义了类型层面的自然数加法, 这个定义我们之后还要用.

在详细叙述使用Vector的正确姿势前, 我们先介绍一下依值类型.

依值类型(Dependent Type)

免责声明: 本文仅简单介绍一点依值类型(DT), 并解释如何在Haskell中"模拟"依值类型的写法, 实质上Haskell并不支持真正的依值类型. 并且如果你对依值类型在编程和数学中的应用感兴趣, Haskell以及本文也不是一个好的入门工具, 你应该去学习类型论并掌握一门真正的依值类型语言. 如果你对Haskell比较熟悉, Idris和Agda是不错的入门选择, 除此之外, Lean4也十分值得学习.

我们关注一个被称为依值函数的类型(也称作Pi类型), 直接的理解就是一个返回值类型依赖于参数值的函数. 这个类型可以记作 (x :: T) -> A 其中 T 是一个普通类型, A 是一个(可以)含有 x 的类型 Haskell目前不支持这样写法, 我们现在需要思考如何在Haskell中模仿这种函数.

在Haskell中模拟DT的技巧被称为 Singletons (好像有人叫单体类型), 实质上是构造一个代理类型将类型 (通常是 'Z, 'True 这种) 和值联系起来.

我们来构造一个 Bool 的Singleton.

1
2
3

data SBool :: Bool -> Type where
  STrue  :: SBool 'True
  SFalse :: SBool 'False

称此为"单体"的原因显而易见, 类型SBool 'True有且只有一个元素STrue, SBool 'False也只有一个元素SFalse. 这就将 b :: Bool 和 SBool b 联系了起来.

定义Singleton上的函数时要同时定义类型层面和值层面, 比如

type family Not (b :: Bool) :: Bool where
  Not 'True = 'False
  Not 'False = 'True

sNot :: SBool b -> SBool (Not b)
sNot STrue  = SFalse
sNot SFalse = STrue

sNot 就是一个Singleton风格的依值函数, 它相当于 (b :: Bool) -> SBool (not b).

现在考虑自然数的Singleton类型, 类似SBool, 我们可以流畅的写出来.

1
2
3

data SNat :: Nat -> Type where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

显然,

SNat 'Z 只有一个元素 SZ,
对于任何一个自然数k :: Nat, 并且 SNat k 只有一个元素 sk, 那么 SNat ('S k) 也只有一个元素 'SS sk.

这样数学归纳告诉我们对于任何自然数 n , SNat n 只有唯一一个元素. 可见 SNat 定义得很正确.

我们来定义一下加法和乘法,

type family (:+:) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :+: n = n
  ('S m) :+: n = 'S (m :+: n)

type family (:*:) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :*: _ = 'Z
  ('S m) :*: n = n :+: (m :*: n)

infixl 6 |+|
(|+|) :: SNat m -> SNat n -> SNat (m :+: n)
SZ   |+| n = n
SS m |+| n = SS (m |+| n)

infixl 7 |*|
(|*|) :: SNat m -> SNat n -> SNat (m :*: n)
SZ   |*| _ = SZ
SS m |*| n = n |+| (m |*| n)

我们用 :+:, :*: 表示类型层面得加和乘, 用 |+|, |*| 表示值层面的加和乘.

为了方便从类型层面的 Nat 向值层面的 SNat 进行转换, 我们可以这样做, 注意这里又用到了之前对类型进行模式匹配的技巧

data Proxy t = Proxy

class ToSNat (nat :: Nat) where
  toSNat :: Proxy nat -> SNat nat

instance ToSNat 'Z where
  toSNat Proxy = SZ
instance ToSNat n => ToSNat ('S n) where
  toSNat Proxy = SS (toSNat (Proxy :: Proxy n))

Proxy 实际上就是一个携带类型信息的 (), 所以说是类型的代理. 然后可以这样使用:

1	`toSNat (Proxy :: Proxy ('S ('S 'Z))) -- => SS (SS SZ)`

这里类型标注起到了输入类型参数的作用.

以Vector为例

我们继续定义一些 Vector 上的函数来展示我们 Singleton 的强大力量. 首先是从列表转换到Vector

fromList :: SNat n -> [a] -> Vect n a
fromList SZ     _        = VNil
fromList (SS n) (x : xs) = x ::: fromList n xs
fromList _ _ = error "Index out of range"

这个函数需要预先给定长度, 这揭示Haskell里模拟DT的根本性不足, 就是不能依赖于运行时的值.

然后是 replicateV, 它生成一个由重复元素组成的Vector.

1
2
3

replicateV :: SNat n -> a -> Vect n a
replicateV SZ     _ = VNil
replicateV (SS n) x = x ::: replicateV n x

安全的下标

即便安全如 Haskell, 它的列表类型仍是下标不安全的, 你可以写 [1,2] !! 2 来触发一个无法被类型系统发现的越界异常. 我们尝试用 Vect 改进这一点.

我们先定义一个可以限定上界的自然数类型

1
2
3

data Fin :: Nat -> Type where
  FZ :: Fin ('S k)
  FS :: Fin k -> Fin ('S k)

Fin n 是一个以 n 为上界的类型, 它有 n 个元素. 以实例来看:

1 2	`FZ :: Fin ('S ('S 'Z)) FS (FZ :: Fin ('S 'Z)) :: Fin ('S ('S 'Z))`

果然只有两个元素, 读者可以自行尝试写一个 FS (FS (FZ :: ???))) 并尝试写出 ???的内容来验证这一点(剧透: 你写不出来).

这个类型恰好可以被用来当作 Vect 的下标类型.

infixl 9 !
(!) :: Vect n a -> Fin n -> a
(x ::: _)  ! FZ     = x
(_ ::: xs) ! (FS f) = xs ! f
-- 写这个函数的时候 GHC 可能会犯二告诉你 pattern non-exhaustive,
-- 但是你把全部模式补上之后又会告诉你 pattern inaccessible. 
-- 我在较新版的 GHC 里遇到了这个问题, 老版里没遇到.

现在我们的的确确可以在编译期保证不会有人写出这样的代码 (1:::2:::VNil) ! (FS (FS FZ)).

定长矩阵

一个矩阵当然可以像向量那样定下长度

1	`type Mat m n a = Vect m (Vect n a)`

矩阵上也能做很多操作, 笔者在学线代时写了一系列矩阵相关函数, 详情请见(https://github.com/KonjacSource/DependentMat), 此处不多赘述.

定理证明

免责声明: 我们只能在Haskell里装模做样地做一些定理证明, 本文也仅供娱乐, 如果你对定理证明感兴趣, 还请学习Agda/Lean4/Coq, 对Haskell熟悉的读者可以快速上手Agda, 这里推荐PLFA(https://plfa.github.io), 并且此书有非常棒的中文翻译(https://zhuanlan.zhihu.com/p/77442536, https://agda-zh.github.io/PLFA-zh/), ; Lean4也是一个体验非常优秀的定理证明器, 很有拿来做通用编程的潜力, 有着非常丰富的数学定理库Mathlib; 然后笔者不会Coq, 不知道怎么安利.

实际上用Haskell的来写定理证明会有大量的语法噪音, 本文甚至可能成为劝退文, 所以如果你对这方面内容真的感兴趣, 不妨学会一门定理证明器之后再来阅读.

用编程语言(定理证明器实际也是编程语言)做定理证明的基础是Curry-Howard对应(下文称CH对应), 该对应指出: 命题对应类型, 证明对应类型的项. 我们以一个例子来阐述.

定义如下类型:

1
2
3

data (:<:) :: Nat -> Nat -> Type where
  LZ :: 'Z :<: 'S n
  LS :: m :<: n -> 'S m :<: 'S n

这个类型对应了小于关系, 在数学上, 小于关系可以看作依赖于两个自然数(我们可以不考虑其它数上的小于关系)的命题, 借助CH对应(类型⇔命题), 我们将它写作依赖于两个自然数的类型. 然后给出构造器(项), 借助CH对应(证明⇔项), 我们将其理解为证明小于关系的方式, 将其写作数学语言就可以说

LZ 可以证明 \(\forall n \in \mathbb{N}, 0 < n + 1\)
给 LS 一个 \(m < n\) 的证明, LS 还你一个 m + 1 < n + 1 的证明.

这就是我们对小于关系的定义, 通过指明如何证明一个关系成立来定义这个关系.

假如我们想要证明 \(2 < 4\) 该如何证明呢?

1 2	`twoLtfour :: 'S ('S 'Z) :<: 'S ('S ('S ('S 'Z))) twoLtfour = LS (LS (LZ :: 'Z :<: 'S ('S 'Z)))`

这里为了读者看得清晰标出了 LZ 的类型, 实际上Haskell可以自己推出来. 我们看一下这是怎么证明出来的, 请把下面代码块中的::读作"证明了".

-- 首先
LZ :: 'Z :<: 'S ('S 'Z)
-- 然后, 回忆 LS 的类型签名, 它相当于在不等式两边同时加了一
LS LZ :: 'S 'Z :<: 'S ('S 'Z)
-- 最后
LS (LS LZ) :: 'S ('S 'Z) :<: 'S ('S ('S ('S 'Z)))
-- Q.E.D.

相等性

我们以证明加法交换律作为本文的结束, 在此之前, 先定义相等性.

1
2
3

infixl 4 :~:
data (:~:) :: k -> k -> Type where
  Refl :: a :~: a

相等性可以作用在任何两个项上(当然我们这里只用到自然数, 所以你把 k 换成 Nat 也不打紧), 它唯一的构造器 Refl (自反性) 精准地捕捉了两个事物相等的条件, 即, 它俩就是一个东西.

我们定义三个常用操作

sym :: a :~: b -> b :~: a
sym Refl = Refl

trans :: a :~: b -> b :~: c -> a :~: c
trans Refl Refl = Refl

cong :: a :~: b -> f a :~: f b
cong Refl = Refl

它们的名字依次是对称性, 传递性, 合同性.

对称性 sym 的类型是 a :~: b -> b :~: a 即, 你给它一个 \(a = b\) 的证明, 它给你一个 \(b = a\) 的证明, 这就是所谓的蕴含(现在你知道函数对应蕴含了). 我们来看一下对称性是如何被证明的,

当你写下如下代码时

1	`sym x = _`

Haskell 会期望下划线处的类型是 b :~: a; 但当你把 x 换成 Refl 时, 期望的类型就变成了 a :~: a, 这时候就可以直接把 Refl 填进去了. 这中间发生了什么? 其实是当你用 Refl 做模式匹配的时候, Haskell就会化简类型, 它会看到 Refl 的类型是 a :~: a, 这时候它就知道该把变元 b 换成 a, 于是最终的结果类型就变成了 a :~: a.

trans 和 cong 的原理也是同样的, 读者可自行验证.

结合律

加法结合律是 \(\forall (a, b, c \in \mathbb{N}), (a + b) + c = a + (b + c)\), 写成类型就是

1	`assoc :: ((a :+: b):+: c) :~: (a :+: (b :+: c)) -- Haskell帮我们写了前面的"forall"`

由于我们需要在类型上进行模式匹配, 所以开一个类型类,

1 2	`class Assoc (a :: Nat) (b :: Nat) (c :: Nat) where assoc :: ((a :+: b) :+: c) :~: (a :+: (b :+: c))`

然后在 a 上做归纳(递归)来证明,

instance Assoc 'Z b c where
  assoc = Refl

instance Assoc a b c => Assoc ('S a) b c where
  assoc = cong @_ @_ @'S (assoc @a @b @c) -- 这里要开 TypeApplications

TypeApplications拓展允许我们使用@来把类型参数显式地应用过去.

首先看第一个情况, Assoc 'Z b c, 这个情况下 a = 'Z, 然后Haskell可以计算出 ((a :+: b) :+: c) = b :+: c 和 (a :+: (b :+: c)) = b :+: c, 所以 assoc 的类型就化简成了 (b :+: c) :~: (b :+: c), 用 Refl 就直接证明了.

第二个情况做了归纳, instance的声明表明 "要有 Assoc ('S a) b c 的类型类, 就要现有 Assoc a b c 的类型类"翻译一下就是"要证明对 ('S a) b c 的结合律, 需要先证明 a b c 的结合律", 这意味着我们可以安全地(不会死循环地)调用 assoc @a @b @c , 这实质就是在a上做数学归纳的过程.

先来看目标类型,

1 2	`instance Assoc a b c => Assoc ('S a) b c where assoc = _`

下划线处的类型应该是 ((('S a) :+: b) :+: c) :~: (('S a) :+: (b :+: c)), 由 :+: 的定义, Haskell可以将其化为最简形式 'S ((a :+: b) :+: c) :~: 'S (a :+: (b :+: c)).

来看一下是如何归纳的,

(assoc @a @b @c)                :: ((a :+: b) :+: c) :~: (a :+: (b :+: c))
cong @_ @_ @'S (assoc @a @b @c) :: 'S ((a :+: b) :+: c) :~: 'S (a :+: (b :+: c))
-- 回忆 cong 的类型, 有 (cong @_ @_ @f (xxx :: x :~: y) :: f x :~: f y)
-- 相当于在等式两边同时作用一个函数, 以后我们会不写这些参数, 而直接写 cong (assoc @a @b @c)
-- Haskell可以推导出来这些参数, 在下面的例子里 f 都是 'S

这恰好和上面的最简形式一致, 所以我们直接填进去得到

1 2	`instance Assoc a b c => Assoc ('S a) b c where assoc = cong @_ @_ @'S (assoc @a @b @c)`

就像先前提到的, Haskell无法自动检查 Assoc 的定义是否覆盖了所有的 Nat, 我们只能人工检查, 我们的定义显然是完整覆盖了的, 这是Haskell不能作为定理证明器的一个重要原因. 定理证明器可以像检查模式匹配完整性那样检查结合律的完整性. 另一个重要原因是Haskell不会进行停机检查, 你可以轻易地写出无限递归来通过类型检查, 这实际对应了循环论证, 定理证明器会确保你的函数一定在有限步内结束.

交换律

证明交换律之前先证明这样一个小引理: \(\forall n \in \mathbb{N}, n + 0 = n\), 翻译成类型,

1 2	`class Idr (n :: Nat) where idr :: (n :+: 'Z) :~: n`

证明也非常简单, 鼓励读者自行尝试, 答案如下:

instance Idr 'Z where
  idr = Refl

instance Idr n => Idr ('S n) where
  idr = cong idr -- 完整形式是 cong @(n:+:'Z) @n @'S (idr @n), Haskell替我们填写了这些参数

然后是另外一个引理: \(\forall (a, b \in \mathbb{N}), a + (b + 1) = (a + b) + 1\), 翻译成类型

1 2	`class SuccR (a :: Nat) (b :: Nat) where succR :: (a :+: 'S b) :~: 'S (a :+: b)`

对 a 归纳, 有

instance SuccR 'Z b where
  succR = Refl

instance SuccR a b => SuccR ('S a) b where
  succR = cong (succR @a @b)

现在来证明交换律: \(\forall (a, b \in \mathbb{N}), a + b = b + a\), 翻译成类型

1 2	`class Comm (a :: Nat) (b :: Nat) where comm :: (a :+: b) :~: (b :+: a)`

对 b 做归纳

instance Idr a => Comm a 'Z where
  comm = idr

instance (SuccR a b, Comm a b) => Comm a ('S b) where
  comm = let eq1 = succR @a @b 
             eq2 = cong (comm @a @b) 
         in trans eq1 eq2

先看 b 为 'Z 的情况, 此时Haskell能直接把目标类型化简为 a :+: 'Z = a, 这就是我们的第一个引理idr, 直接填上就能证明.

比较复杂的是 b 为 'S b 的情况, 我们把目标 (a :+: 'S b) :~: 'S (b :+: a) 分成两个式子:

(a :+: 'S b) :~: 'S (b :+: a)
分成
eq1 :: (a :+: 'S b) :~: 'S (a :+: b)
eq2 :: 'S (a :+: b) :~: 'S (b :+: a)

第一个式子就是我们证明的第二个引理 succR, 所以我们在约束上写SuccR a b; 第二个式子两边都去掉 'S 就是 comm @a @b, 所以我们在约束上写Comm a b, 然后再在comm @a @b类型的等式两边同时用cong加上'S函数, 就能得到 eq2.

最后再用等式的传递性连接 eq1 和 eq2 就能得到最终的结果:

1	`trans eq1 eq2 :: (a :+: 'S b) :~: 'S (b :+: a)`

完整代码

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-missing-export-lists #-}

module Test where

import Data.Kind (Type)

infixr 4 :+:
data HList :: [Type] -> Type where
  HNil  :: HList '[]
  (:+:) :: t -> HList ts -> HList (t ': ts)

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show t, Show (HList ts)) => Show (HList (t ': ts)) where
  show (x :+: xs) = show x ++ ":+:" ++ show xs

type family TAppend (ls1 :: [Type]) (ls2 :: [Type]) :: [Type] where
  TAppend '[] ys = ys
  TAppend (x ': xs) ys = x ': TAppend xs ys

hAppend :: HList ts1 -> HList ts2 -> HList (TAppend ts1 ts2)
hAppend HNil ys = ys
hAppend (x :+: xs) ys = x :+: hAppend xs ys

type family Map (f :: Type -> Type) (ts :: [Type]) :: [Type] where
  Map f '[] = '[]
  Map f (t ': ts) = f t ': Map f ts

-- hSequence :: forall (m :: Type -> Type) (ts :: [Type]) . Monad m => HList (Map m ts) -> m (HList ts)

class HSeq (ts :: [Type]) where
  hSequence :: Monad m => HList (Map m ts) -> m (HList ts)

instance HSeq '[] where
  hSequence HNil = return HNil

instance HSeq ts => HSeq (t ': ts) where
  hSequence (x :+: xs) = do
    xr <- x
    xsr <- hSequence xs
    return (xr :+: xsr)

data Nat = Z | S Nat

infixr 4 :::
data Vect :: Nat -> Type -> Type where
  VNil :: Vect 'Z a
  (:::) :: a -> Vect n a -> Vect ('S n) a

type family (:+) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :+ n = n
  ('S m) :+ n = 'S (m :+ n)

vAppend :: Vect m a -> Vect n a -> Vect (m :+ n) a
vAppend VNil ys = ys
vAppend (x:::xs) ys = x ::: vAppend xs ys



nat2Int :: Nat -> Int
nat2Int Z = 0
nat2Int (S n) = 1 + nat2Int n

instance Show Nat where
  show = ("n"++) . show . nat2Int

instance Num Nat where
  Z     + n = n
  (S m) + n = S (m + n)

  Z     - _     = Z
  m     - Z     = m
  (S m) - (S n) = m - n

  Z     * _ = Z
  (S m) * n = n + (m * n)

  fromInteger 0 = Z
  fromInteger n = S $ fromInteger (n - 1)

  abs x = x
  signum _ = 1

data SNat :: Nat -> Type where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

infixl 6 |+|
(|+|) :: SNat m -> SNat n -> SNat (m :+: n)
SZ   |+| n = n
SS m |+| n = SS (m |+| n)

infixl 7 |*|
(|*|) :: SNat m -> SNat n -> SNat (m :*: n)
SZ   |*| _ = SZ
SS m |*| n = n |+| (m |*| n)


type family (:+:) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :+: n = n
  ('S m) :+: n = 'S (m :+: n)

type family (:*:) (m :: Nat) (n :: Nat) :: Nat where
  'Z     :*: _ = 'Z
  ('S m) :*: n = n :+: (m :*: n)


data Proxy t = Proxy

class FromNat (nat :: Nat) where
  fromNat :: Proxy nat -> Nat

instance FromNat 'Z where
  fromNat _ = 0

instance FromNat n => FromNat ('S n) where
  fromNat _ = S $ fromNat (Proxy :: Proxy n)

class ToSNat (nat :: Nat) where
  toSNat :: Proxy nat -> SNat nat

instance ToSNat 'Z where
  toSNat Proxy = SZ

instance ToSNat n => ToSNat ('S n) where
  toSNat Proxy = SS (toSNat (Proxy :: Proxy n))

fromList :: SNat n -> [a] -> Vect n a
fromList SZ     _        = VNil
fromList (SS n) (x : xs) = x ::: fromList n xs
fromList _ _ = error "Index out of range"

data Fin :: Nat -> Type where
  FZ :: Fin ('S k)
  FS :: Fin k -> Fin ('S k)

infixl 9 !
(!) :: Vect n a -> Fin n -> a
(x ::: _)  ! FZ     = x
(_ ::: xs) ! (FS f) = xs ! f


data (:<:) :: Nat -> Nat -> Type where
  LZ :: 'Z :<: 'S n
  LS :: m :<: n -> 'S m :<: 'S n

twoLtfour :: 'S ('S 'Z) :<: 'S ('S ('S ('S 'Z)))
twoLtfour = LS (LS (LZ :: 'Z :<: 'S ('S 'Z)))


infixl 4 :~:
data (:~:) :: k -> k -> Type where
  Refl :: a :~: a

cong :: a :~: b -> f a :~: f b
cong Refl = Refl

sym :: a :~: b -> b :~: a
sym Refl = Refl

trans :: a :~: b -> b :~: c -> a :~: c
trans Refl Refl = Refl

class Assoc (a :: Nat) (b :: Nat) (c :: Nat) where
  assoc :: ((a :+: b) :+: c) :~: (a :+: (b :+: c))

instance Assoc 'Z b c where
  assoc = Refl

instance Assoc a b c => Assoc ('S a) b c where
  assoc = cong @_ @_ @'S (assoc @a @b @c)

class Idr (n :: Nat) where
  idr :: (n :+: 'Z) :~: n
  
instance Idr 'Z where
  idr = Refl

instance Idr n => Idr ('S n) where
  idr = cong @(n:+:'Z) @n @'S (idr @n)

class SuccR (a :: Nat) (b :: Nat) where
  succR :: (a :+: 'S b) :~: 'S (a :+: b)

instance SuccR 'Z b where
  succR = Refl

instance SuccR a b => SuccR ('S a) b where
  succR = cong (succR @a @b)

class Comm (a :: Nat) (b :: Nat) where
  comm :: (a :+: b) :~: (b :+: a)

instance Idr a => Comm a 'Z where
  comm = idr

instance (SuccR a b, Comm a b) => Comm a ('S b) where
  comm = let eq1 = succR @a @b 
             eq2 = cong (comm @a @b) 
         in trans eq1 eq2

#Haskell #编程 #计算机

类型体操指北 (Haskell)

http://konjacsource.github.io/2023/11/08/Haskell/

作者

KonjacSource

发布于

2023年11月8日

许可协议

海森堡方程上一篇

热力学笔记下一篇