实现一个 Hindley-Milner 类型系统

随着对函数式语言的兴趣日渐浓厚，我对设计一门编程语言的冲动也越来越强烈。这个过程非常的艰难，需要大量的基础知识作为铺垫，其中非常重要的部分——类型系统尤为复杂。我从一些博文中了解到了Hindley-Milner类型系统、Algorithm W 和 Algorithm J等等知识，并试图整理出来一条脉络以供日后使用。

在这篇博客中，我将会通过一个例子展示Hindley-Milner类型系统，并通过Haskell完成实现。

Language

在这里，给出我们将要设计的语言的样子，它包括基础的变量，lambda表达式，基础类型，let 绑定，if表达式，二元操作符等等。目前它被设计的足够精简。

{- Expressions -}
abc                -- Variable
if a then b else c -- If-expression
\x -> y : a -> b   -- Abstraction
f x                -- Application
let a = b in c     -- Let-binding
123456789 : Int    -- Integer
True, False : Bool -- Boolean
x + y              -- Integer addition
x - y              -- Integer subtraction

如果写着

，这代表

是

类型

Syntax Representation

定义一些数据结构来表示我们设计的语言（启用 PatternSynoyms 拓展）。

首先给出一个类型别名用来表示符号名

{-# Language PatternSynonyms #-}
type Name = String

然后定义一个Expr 结构用来表示在 Language 中提到的表达式

data Expr
	= EVar Name
	| EIf Expr Expr Expr
	| EAbs Name Expr
	| EApp Expr Expr
	| ELet Name Expr Expr
	| EInt Integer
	| EBool Bool
	| EBin Oper Expr Expr
	deriving Show

然后定义一个结构用来表示操作符

data Oper = Add | Sub deriving Show

接下来就是用于表示 “类型” 的结构，TCon是具体类型，例如Int，Bool或者List Char等等。TVar是类型变量，是具体类型的占位符

newtype TVar = TV Name deriving (Eq, Show)
data Type
	= TCon Name [Type]
	| TVar TVar
	deriving (Eq, Show)

同时我们定义一些内置类型，在这里用到了PatternSynoyms提供的能力。

pattern TInt = TCon "Int" []
pattern TBool = TCon "Bool" []
pattern a :-> b = TCon "->" [a, b]

The Type System

在完成前置准备后，我们就可以来了解Hindley-Milner 类型系统了。

从根本上说，类型推断就是沿着抽象语法树逐级下降，为每个表达式分配新的类型变量，并根据可用信息生成一组约束(Constraint)的过程。之后，对这组约束条件进行求解（就像求解方程组一样），就会产生一个替换。这种替换将把每个生成的类型变量映射到推断出的主类型。解决约束的过程称为统一(Unification)。(主类型或多或少是表达式的最一般类型，即表达式的任何其他可能类型都是主类型的实例）。

Hindley-Milner 类型系统是由一系列推理规则定义的：

如果你之前没有接触过推理规则，它对你来说可能看起来像是外星语言。实际上，它们非常简单；在这种符号中，水平线上方的是假设，下方的是结论。

代表上下文信息，而代表断言或者证明，通常表示多态类型、代表单态类型。

每条上述规则描述了我们如何处理我们语言的一部分。前四个是：变量、函数应用、函数抽象和let绑定。之后我们将讨论最后两个：泛化和实例化。

让我们尝试解析第一个规则。假设是 x 在的上下文中属于类型。由此得出的结论 () 是：在中，可以断言 x 是类型。这条规则听起来可能有点傻，但它很重要，因为它向我们展示了如何使用上下文。（上下文也可以称为类型环境。）

第二个规则可能看起来更复杂，但其实同样简单。在中，如果有一个函数将类型的值映射到类型的值，并且有一个表达式属于类型，那么在中，应用到上会产生一个类型的结果。

在第三个规则中，假设是一个上下文，再加上一个变量，它断言。结论是，一个接收并计算的函数将会是类型 - 将类型的值映射到类型的值。

第四个规则向我们展示了如何处理let绑定。如果在中某个表达式，并且在中加上一个同类型的变量，断言有一个表达式，那么我们可以得出结论，绑定并计算会给我们一个类型的表达式。

现在，推理规则有了意义，你很可能想知道：如何利用这些信息进行类型推断？实际上相当简单。你所要做的就是逆向工作通过类型规则。给定一个表达式和一个与表达式匹配的结论（来自规则），你可以为未知类型的子表达式分配新的（未使用的）类型变量，并使用假设中的判断来对这些类型变量开发约束。如果这听起来不太明白，再想一想。一旦我们开始实现，这些应该会更有意义。

接下来是泛化和实例化的规则；但我们首先必须弄清楚多态和单态是什么。

Polymorphism and Monomorphism

多态性通常是指允许函数接受不同类型的输入。我们将要关注的多态类型被称为参数多态性。这只是泛型的一个高级名称。它与特设多态性（也称为重载）的不同之处在于，参数多态性函数必须以相同的方式处理每种类型的输入。参数多态性函数的一个简单例子是恒等函数。

类型变量是全称量化的。我们将用Type Schemes来表示这些多态类型（polytypes）。一般来说，如果一个类型包含类型变量，那么它就是一个 polytype。这个事实允许我们将包含类型变量的类型泛化为一个Scheme。为了展示我们为什么需要这样做，让我们考虑单态性。

单态性是多态性的对立面 - 一个单态函数只接受特定类型的输入。即使类型包含类型变量，类型推断也会使其在函数后续使用后归结为一个特定类型。例如：

let id = (\x -> x) in (id True)

当推断 id 的类型时，它被推断为 id : a -> a。然而，在 let 绑定的主体中，我们将其应用于一个布尔值。由于我们没有明确指出 id 应该是多态的，因此 id 的最终推断类型将变为 id : Bool -> Bool。而Scheme解决了这个问题，并推断出 id : \forall a. a -> a。

Generalization and Instantiation

泛化和实例化是 Hindley-Milner 类型系统中最重要的两个概念。泛化处理将单态（monomorphism）转换为多态类型（polytype），方法是关闭中所有自由类型变量的出现。关闭只是指移除任何自由变量，在数学中，自由变量是指在当前“范围”内未定义的变量。我们通过量化这些自由变量来移除它们的出现。

泛化的规则是：

给定，它断言，以及许多不在中作为自由类型变量的类型变量，我们可以得出结论，在中可以断言。换句话说，由于包含类型变量，我们可以用所有在上下文中未使用的类型变量对其进行全称量化。这可能会导致使用不出现在中的类型变量进行量化，但这并不会造成差异。

实例化有点像泛化的逆过程；你取一个类型方案并用单态的新鲜类型变量替换所有量化的类型变量。每当我们需要使用类型方案时就会这样做。

如果在中可以断言，并且是的一个实例化，则我们可以得出结论，在中也可以断言同样是类型的。

当我们说“是…的一个实例化”时，非正式地，我们的意思是在某种程度上类似于。通过例子更容易解释这一点。

Substitution

你可能已经对什么是替换有了一个概念。

基本上，它是从符号到其他符号的映射。应用一个替换意味着“一致地”将一个符号替换为在替换中映射到的内容。应用替换的例子：

替换出现在方括号内（例如）。多个替换由逗号分隔。也常见到符号用于表示替换。我们将以 Data.Map 的形式表示替换，其中类型变量作为键，类型作为值。

Free Type Variables

我们还将使用函数 tvs 来检索类型中所有自由类型变量的集合。它将使用 Data.Set 实现。定义如下：

Unification

统一（Unification）是我们构建替换的过程。我们不需要正式了解什么是统一。我们的算法只需要做的是取一个约束，比如等式约束，并尝试统一两个术语。

例如，如果两个术语之一是一个类型变量，例如，那么产生的替换可以简单地是或。

我们将使用记号来表示和可以通过替换进行统一，这意味着。有了这个，统一规则如下：

我们检查是否出现在的自由类型变量中，用于 Var Left 和 Var Right 规则，是因为否则它会尝试构造一个无限类型。

例如，尝试统一。你得到的替换是。如果我们尝试应用这个替换，我们会得到以下结果：

为了避免这种无限循环，我们执行一个称为“出现检查”的操作，这就是写成的内容。

Inference Implementation

最终，把所有的解释放在一边，我们可以开始实现类型系统。这是所有内容希望能够合理结合并且有意义的地方。我们将要实现的特定算法被称为算法 W。这个算法与算法 J 的不同之处在于我们首先构建一组约束，然后执行统一和替换。在算法 J 中，你会在生成约束的同时进行统一和替换。

首先，让我们回顾一下我们将用于类型推断的 monad 转换器栈。主要的 monad 转换器将是 RWST，它等同于 ReaderT、WriterT、StateT`` 栈。它将转换的 monad 将是Except String`，你可以根据需要添加自定义错误类型。

Reader monad 的环境将是类型上下文，一个从 Names 到 Schemes 的 Data.Map。Scheme 将是我们表示类型方案（polytypes）的方式。它将仅仅是一个类型变量的 Data.Set，以及这些类型变量关闭的类型。

Writer 将添加到等式约束列表中，我们将以另一种数据类型表示这些约束。我们还将定义一个帮助此过程的函数 constrain。

State monad 将保持生成的新鲜类型变量的计数（Int），以便我们知道下次返回哪个新鲜类型变量。函数 fresh 将处理生成新的类型变量。

最后一件事，启用 LambdaCase 语言扩展。它将使我们能够编写稍微清晰的代码。到目前为止，我们有：

{-# Language PatternSynonyms #-}
{-# Language LambdaCase #-}

{- ... Imports from before ... -}

import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad.RWS
import Control.Monad.Except

{- ... Code from before ... -}

data Scheme = Forall [Set.Set TVar] Type
data Constraint = Constraint Type Type
type Context = Map.Map Name Scheme
type Count = Int
type Constraints = [Constraint]

type Infer a = RWST Context Constraints Count (Except String) a

constrain :: Type -> Type -> Infer ()
constrain = tell . (:[]) . Constraint

fresh :: Infer Type
fresh = do
	count <- get
	put (count + 1)
	return . TVar . TV $ show count

我们还定义一个名为 Substitutable 的类型类，它将定义 apply 函数用于应用替换，以及 tvs 函数用于查询自由类型变量。如上所述，我们将替换简单地表示为从类型变量到类型的 Data.Map。tvs 函数将给我们一个类型变量的 Data.Set，就像我们上面定义的那样。同时定义一个名为 compose 的函数，以便更容易地组合替换。

type Subst = Map.Map TVar Type

compose :: Subst -> Subst -> Subst
compose a b = Map.map (apply a) (b `Map.union` a)

class Substitutable a where
	apply :: Subst -> a -> a
	tvs :: a -> Set.Set TVar

然后，我们可以使一些数据类型成为 Substitutable 的实例。我们已经讨论过查询类型变量的规则，而 apply 的实现大多是直接的，所以不会详细讨论实现。

instance Substitutable Type where
	tvs (TVar tv) = Set.singleton tv
	tvs (TCon _ ts) = foldr (Set.union . tvs) Set.empty ts
	apply s t@(TVar tv) = Map.findWithDefault t tv s
	apply s (TCon c ts) = TCon c $ map (apply s) ts

instance Substitutable Scheme where
	tvs (Forall vs t) = tvs t `Set.difference` vs
	apply s (Forall vs t) = Forall vs $ apply (foldr Map.delete s vs) t
	
instance Substitutable Constraint where
	tvs (Constraint t1 t2) = tvs t1 `Set.union` tvs t2
	apply s (Constraint t1 t2) = Constraint (apply s t1) (apply s t2)
	
instance Substitutable a => Substitutable [a] where
	tvs l = foldr (Set.union . tvs) Set.empty l
	apply s = map (apply s)

接下来，我们必须实现泛化（generalization）和实例化（instantiation）。这两个过程已经在第一部分中讨论过。generalize 函数将接收一个上下文和一个类型，并返回一个类型方案。instantiate 函数将接收一个类型方案，并在为其封闭的所有类型变量填入新鲜类型变量后返回一个类型。我们通过简单地应用一个替换来填充。

generalize :: Context -> Type -> Scheme
generalize ctx t = Forall (tvs t `Set.difference` tvs (Map.elems ctx)) t

instantiate :: Scheme -> Infer Type
instantiate (Forall vs t) = do
	let vars = Set.toList vs
	ftvs <- traverse (const fresh) vars
	let subst = Map.fromList (zip vars ftvs)
	return $ apply subst t

现在我们可以开始主要的表达式推断函数。它的类型将是 Expr -> Infer Type。这个函数所做的只是逆向通过我们之前讨论过的推断规则（如果需要，请回顾第一部分）。对于 if 表达式的推断解释已经在注释中说明，尽管它应该是相当明显的。

infer :: Expr -> Infer Type
infer = \case
	EInt _ -> TInt -- Integer literal
	EBool _ -> TBool -- Boolean literal
	EVar v -> do
		ctx <- ask -- Retrieve context from Reader
		case Map.lookup v ctx of
			Just t -> instantiate t -- Instantiate type scheme for use
			Nothing -> throwError $ "Undefined variable " ++ v -- Variable not defined
	EIf c a b -> do
		ct <- infer c -- Infer type of condition expression
		at <- infer a -- Infer type of main branch
		bt <- infer b -- Infer type of else branch
		constrain ct TBool -- Condition expression should be a Bool
		constrain at bt -- Branches should be of same type
		return at -- Return type of any branch
	EAbs p e -> do
		pt <- fresh -- Generate fresh type variable for param
		let ps = Forall Set.empty pt
		et <- local (Map.insert p ps) (infer e) -- Infer function definition with param defined
		return $ pt :-> et -- Function has type pt -> et
	EApp f a -> do
		ft <- infer f -- Infer type of expression being called
		at <- infer a -- Infer type of argument
		rt <- fresh -- Fresh type variable for result type
		constrain ft (at :-> rt)
		return rt
	EBin o a b -> do
		let ot = -- Operators are functions
			case o of
				Add -> TInt :-> (TInt :-> TInt)
				Sub -> TInt :-> (TInt :-> TInt)
				-- NOTE: ADD MORE OPERATORS!!
		at <- infer a -- Infer left operand
		bt <- infer b -- Infer right operand
		t <- fresh -- Result type
		constrain ot (at :-> (bt :-> t))
		return t
	ELet v e b -> do
		et <- infer e -- Infer variable type
		ctx <- ask
		let es = generalize ctx et -- Generalize variable type
		bt <- local (Map.insert v es) (infer b) -- Infer body with variable defined
		return bt

这就是主要类型推断函数的全部内容。请多阅读几遍以确保理解它。现在我们剩下要实现的就是统一（unification）过程。这将或多或少直接将上面的定义翻译成代码。我们还应该为整个解决过程使用不同的 monad，即 Except monad。将定义一个名为 bind 的辅助函数，用于代码重用。它将执行出现检查。

type Solve a = Except String a

unify :: Type -> Type -> Solve Subst
unify a b | a == b = return Map.empty -- Same
unify (TVar v) t = bind v t -- Var Left
unify t (TVar v) = bind v t -- Var Right
unify a@(TCon n1 ts1) b@(TCon n2 ts2) -- Arrow (->) / other TCons
	| a /= b = throwError $ "Type mismatch " ++ show a ++ " and " ++ show b
	| otherwise = unifyMany ts1 ts2
	where
		unifyMany [] [] = return Map.empty
		unifyMany (t1 : ts1) (t2 : ts2) = do
			s1 <- unify t1 t2
			s2 <- unifyMany (apply s1 ts1) (apply s1 ts2)
			return (s2 `compose` s1)

bind :: TVar -> Type -> Solve Subst
bind v t
	| v `Set.member` tvs t = throwError $ "Infinite type " ++ show v ++ " ~ " ++ show t -- Occurs check
	| otherwise = return $ Map.singleton v t

最后，我们应该定义一个函数，它接收一系列约束并通过统一（unify）过程构建出最终的替换。定义一个运行 solve 的辅助函数也会很有用。

solve :: Subst -> [Constraint] -> Solve Subst
solve s [] = return s
solve s ((Constraint t1 t2) : cs) = do
	s1 <- unify t1 t2
	solve (s1 `compose` s) (apply s1 cs)

runSolve :: [Constraint] -> Either TypeError Subst
runSolve = runExcept . solve Map.empty

< 白鸽

多谢你 >