haskell - 设计一种简单的静态类型化语言的类型系统(在Haskell中)

Question

我一直在想为一种命令式，静态类型的语言编写解释器以习惯于函数式编程和Haskell的想法，但是我从未真正想到过清晰的语法，这常常导致不满意的代码和迫切的需求。重写一切，所以我来这里寻求帮助。我应该如何设计一个相对简单但可扩展的类型系统？

我想支持基本的原语，例如数值类型，布尔值，字符等（在我掌握基本知识之前，不要涉足数组或记录结构）及其相关的基本操作。我最大的问题是我不完全知道应如何实现类型和运算符之间的关系。

我对Haskell的了解不多，但是定义一堆重复的求和类型的简单解决方案如

data ArithmeticOperator =
    Plus
    | Min
    | Mul 
    | Div

data LogicalOperator =
    And
    | Or
    | Not

对我而言，这似乎并不雄辩，因为这种类型划分将进一步传播到基于这些类型（如表达式）的结构中，并且在评估表达式时必须对每个运算符进行模式匹配似乎非常繁琐且不易扩展。

因此，我想到了为操作员定义一个灵活的类型，例如

data Operator a b =
    UnaryOperator (a -> b)
    | BinaryOperator (a -> a -> b)

其中a代表参数类型，b代表返回类型。问题是我真的不知道如何将类型强制为仅打算支持的类型。它看起来更简洁，但我不确定这是否“正确”。

最后，是否有任何资源可以以初学者友好的方式介绍此主题？我不想在这个主题上过分深入，但是我很想读..那么，在设计类型系统时，常见的原则/注意事项。

Answer 1

根据评论，请勿尝试作为第一个口译员。如果您尚未为未类型化的lambda演算编写解释器，或者未完成诸如Write Yourself a Scheme in 48 Hours之类的教程，请首先进行操作。

无论如何，这是一个静态解释器的简单实现，该解释器具有布尔和数字类型，一些内置运算符（包括具有多态性的一个），变量和let x=... in ...变量绑定，但没有lambda。它说明了一种设计类型化解释器的常用方法，但由于缺少足够的信息，不会破坏您的乐趣。

注意：我有意避免使用任何中级或高级Haskell功能（例如，ExprU和ExprT类型未统一为单个多态类型-对我们而言没有“ trees that grow” ！；我没有在键入目标语言时将GADT用作leverage the Haskell type system；等等。这些先进的技术可以带来更安全的代码-并且也非常出色，因此您将来肯定希望对其进行研究-但对于使基本类型的解释器正常工作而言，它们并不是必需的。

编写解释器时，最好打开-Wall －它会提醒您忘记处理哪些模式（即表达式类型）：

{-# OPTIONS_GHC -Wall #-}

另外，为了保持理智，我们需要使用一些monad：

import Control.Monad
import Control.Monad.Reader
import Control.Monad.Except

您在问题中提到，您在努力采用两种方法：一开始就按类型划分运算符，而某种程度上反映Haskell类型系统中的运算符类型。您对第一种方法的直觉已经到位-效果不是很好。第二种方法是可行的，但是您将很快遇到一些尚未准备好的非常先进的Haskell技术。

相反，对于我们的静态类型语言，让我们开始定义一个完全无类型的抽象表达式语法。请注意，这是一种完全不了解类型的解析器可能生成的抽象语法：

-- Untyped expressions
data ExprU
  = FalseU | TrueU           -- boolean literals
  | NumU Double              -- numeric literal
  | VarU String              -- variable
  | UnU UnOp ExprU           -- unary operator
  | BinU BinOp ExprU ExprU   -- binary operator
  | LetU String ExprU ExprU  -- let x = expr1 in expr2
data UnOp = NegOp | NotOp
  deriving (Show)
data BinOp = PlusOp | MulOp | AndOp | OrOp | EqualsOp
  deriving (Show)

注意，我们可以为此直接编写一个解释器。但是，解释器将不得不处理类型错误的表达式，例如：

BinU PlusOp FalseU (NumU 1)   -- False + 1

这会破坏定义静态类型语言的全部目的。

关键的见解是，我们可以采用这种非类型化的语言，并且在解释它之前，先对它进行类型检查！使用Haskell类型系统对目标语言进行类型检查有很多很酷的技术，但是只定义一个单独的数据类型来表示表达式类型要容易得多：

-- Simple expression types
data Typ
  = BoolT
  | NumT
  deriving (Show, Eq)

对于我们的操作员，也可以方便地给他们“类型”：

-- Types of operators
data BinTyp = BinTyp Typ Typ Typ   -- binary ops: two arg types plus result type
data UnTyp  = UnTyp Typ Typ        -- unary ops: arg type plus result type

在具有一流功能的语言中，我们可能会将这些类型组合为单个Haskell Typ，它不仅可以表示布尔值和num之类的“原始”类型，还可以表示诸如Bool -> Bool -> Bool之类的函数类型。但是，对于这种简单的语言，我们将“表达式类型”和“运算符类型”分开。

我们如何处理这些类型？好吧，我们采用我们的无类型表达式ExprU，并通过向每个表达式添加类型注释来对它们进行类型检查：

-- Typed expressions
data ExprT
  = BoolLit Bool
  | NumLit Double
  | VarT Typ String
  | UnT Typ UnOp ExprT
  | BinT Typ BinOp ExprT ExprT
  | LetT Typ String ExprT ExprT

在这里，每个构造函数（文字常量除外）都有一个Typ字段，该字段给出了关联表达式的类型。 （实际上，即使多余，我们也可以在文字上添加一个Typ字段。）使用帮助函数从ExprT中提取类型会很有帮助：

exprTyp :: ExprT -> Typ
exprTyp (BoolLit _) = BoolT
exprTyp (NumLit _) = NumT
exprTyp (VarT t _) = t
exprTyp (UnT t _ _) = t
exprTyp (BinT t _ _ _) = t
exprTyp (LetT t _ _ _) = t

类型检查将在monad中进行，该monad跟踪变量的类型（这是我们无法通过检查表达式立即找出的一件事）：

type TypContext = [(String, Typ)]   -- context of variable types
type TC = ExceptT Error (Reader TypContext)

现在，我们仅可以将字符串用于类型错误：

type Error = String

我们的类型检查器非常容易编写。我采用一个无类型的表达式ExprU，并添加适当的类型注释以构成ExprT：

tc :: ExprU -> TC ExprT

创建文字的“类型化版本”很容易：

tc (FalseU) = pure $ BoolLit False
tc (TrueU) = pure $ BoolLit True
tc (NumU x) = pure $ NumLit x

用我们的语言，变量的类型也很容易。我们仅允许在定义变量后使用它们（通过LetU绑定-参见下文），因此它们的类型在当前上下文中始终可用：

tc (VarU var) = do
  mt <- asks (lookup var)
  case mt of
    Just t -> pure $ VarT t var
    Nothing -> throwError $ "undefined variable " ++ var

一元运算符的类型很容易。一元运算符只有两个，即“取反”和“非”，它们都仅精确地应用于一种参数类型，并且只产生一种结果类型。 unTyp子句中的where函数告诉我们一元运算符具有什么UnTyp：

tc (UnU op e) = do
  let UnTyp targ tresult = unTyp op
  e' <- tc e
  let t = exprTyp e'
  when (t /= targ) $ throwError $ "op " ++ show op ++ 
    " expected arg of type " ++ show targ ++ ", got " ++ show t
  pure $ UnT tresult op e'
  where
    unTyp NegOp = UnTyp NumT NumT
    unTyp NotOp = UnTyp BoolT BoolT

对于二进制运算符，EqualsOp有点复杂。我们想要实现一些特殊的多态性，以便可以将其应用于布尔值和数字，尽管我们要求类型必须匹配（因此不允许False == 1）。因此，我们将检查参数的类型并确保它们匹配。但是，无论参数是什么类型，BinU EqualsOp _ _表达式的类型将始终为布尔值，因此键入的版本将始终为BinT BootT EqualsOp _ _：

tc (BinU EqualsOp e1 e2) = do
  e1' <- tc e1
  e2' <- tc e2
  let t1 = exprTyp e1'
      t2 = exprTyp e2'
  when (t1 /= t2) $ throwError $ "op EqualOp needs to compare equal types"
  pure $ BinT BoolT EqualsOp e1' e2'

其他二元运算符是单型运算符，因此我们对它们的处理与上面的（单型）一元运算符相同：

tc (BinU op e1 e2) = do
  let BinTyp targ1 targ2 tresult = binTyp op
  e1' <- tc e1
  e2' <- tc e2
  let t1 = exprTyp e1'
      t2 = exprTyp e2'
  when (t1 /= targ1) $ throwError $ "op " ++ show op ++
    " expected left arg of type " ++ show targ1 ++ ", got " ++ show t1
  when (t2 /= targ2) $ throwError $ "op " ++ show op ++
    " expected right arg of type " ++ show targ2 ++ ", got " ++ show t2
  pure $ BinT tresult op e1' e2'
  where
    binTyp PlusOp = BinTyp NumT NumT NumT
    binTyp MulOp = BinTyp NumT NumT NumT
    binTyp AndOp = BinTyp BoolT BoolT BoolT
    binTyp OrOp = BinTyp BoolT BoolT BoolT
    binTyp EqualsOp = error "internal error"

您可能希望对LetU表达式进行类型检查很复杂，但这非常简单。对于let x=exp1 in exp2，我们只需计算exp1的类型，然后在计算x的类型时将exp2的类型添加到类型上下文中：

tc (LetU var e1 e2) = do
  e1' <- tc e1
  let t1 = exprTyp e1'
  e2' <- local ((var,t1):) $ tc e2
  let t2 = exprTyp e2'
  pure $ LetT t2 var e1' e2'

这就是类型检查器的全部内容。

运行类型检查器以创建具有声音类型的ExprT之后，我们将对其进行评估。我们将表达式的值表示为：

-- Values
data Value
  = BoolV Bool
  | NumV Double
  deriving (Show)

评估将在monad中进行，其上下文将变量分配值：

type ValContext = [(String, Value)]   -- context of variable values
type E = Reader ValContext

请注意，我们在这里不需要ExceptT变压器。事实证明，类型检查程序无法使用我们的语言生成运行时错误。

评估员/口译员：

eval :: ExprT -> E Value

以明显的方式评估文字：

eval (BoolLit b) = pure $ BoolV b
eval (NumLit x) = pure $ NumV x

在当前上下文中查找变量值：

eval (VarT _ var) = do
  mt <- asks (lookup var)
  case mt of
    Just v -> pure $ v
    Nothing -> internalerror

请注意，类型检查器已经确保仅在定义变量后才使用它们，因此失败的查找“不会发生”。我们使用函数internalerror（在下面定义）来使编译器满意地处理了所有情况，从而避免出现警告，但是除非解释器中存在错误，否则将不会调用internalerror。

一元运算符的解释如下：

eval (UnT _ op e) = run op <$> eval e
  where run NegOp (NumV x) = NumV (-x)
        run NotOp (BoolV b) = BoolV (not b)
        run _ _ = internalerror

同样，由于类型检查器的原因，我们不能将NegOp应用于布尔值或NotOp应用于数字，因此此处的遗漏情况（例如run NegOp (BoolV b)）不会发生。不幸的是，这意味着我们失去了打开-Wall的某些好处-如果我们忘记处理新的运算符，它将在运行时抛出internalerror。 <插入悲伤表情符号>

二进制运算符的解释类似：

eval (BinT _ op e1 e2) = run op <$> eval e1 <*> eval e2
  where run EqualsOp (BoolV v1) (BoolV v2) = BoolV $ v1 == v2
        run EqualsOp (NumV v1) (NumV v2) = BoolV $ v1 == v2
        run PlusOp (NumV v1) (NumV v2) = NumV $ v1 + v2
        run MulOp (NumV v1) (NumV v2) = NumV $ v1 * v2
        run AndOp (BoolV v1) (BoolV v2) = BoolV $ v1 && v2
        run OrOp (BoolV v1) (BoolV v2) = BoolV $ v1 || v2
        run _ _ _ = internalerror

因为Haskell ==运算符是多态的，所以我们可以将Eq实例添加到Value类型，并用以下两种情况替换前两种情况：

  where run EqualsOp v1 v2 = BoolV $ v1 == v2

但是我想说明一个事实，即EqualsOp (BoolV v1) (NumV v2)永远不会在类型检查程序中发生。

最后，我们这样处理LetT：

eval (LetT _ var e1 e2) = do
  v1 <- eval e1
  local ((var,v1):) $ eval e2

那是我们的评估员/口译员。

有意思的事情。在我们对eval的定义中，我们实际上从未引用tc添加的类型注释！因此，我们实际上可以编写eval来解释原始的无类型ExprU，因为完成tc的事实足以确保可以解释ExprU而不会出现运行时类型错误。也就是说，用这种简单的语言，程序类型检查的事实比类型检查期间计算的类型重要得多。在更复杂的语言中，类型注释可能更有用。

无论如何，就是这样。这是完整的代码以及目标语言的示例程序expr1：

{-# OPTIONS_GHC -Wall #-}

import Control.Monad
import Control.Monad.Reader
import Control.Monad.Except

-- Untyped expressions
data ExprU
  = FalseU | TrueU           -- boolean literals
  | NumU Double              -- numeric literal
  | VarU String              -- variable
  | UnU UnOp ExprU           -- unary operator
  | BinU BinOp ExprU ExprU   -- binary operator
  | LetU String ExprU ExprU  -- let x = expr1 in expr2
data UnOp = NegOp | NotOp
  deriving (Show)
data BinOp = PlusOp | MulOp | AndOp | OrOp | EqualsOp
  deriving (Show)

-- Simple expression types
data Typ
  = BoolT
  | NumT
  deriving (Show, Eq)

-- Types of operators
data BinTyp = BinTyp Typ Typ Typ
data UnTyp  = UnTyp Typ Typ

-- Typed expressions
data ExprT
  = BoolLit Bool
  | NumLit Double
  | VarT Typ String
  | UnT Typ UnOp ExprT
  | BinT Typ BinOp ExprT ExprT
  | LetT Typ String ExprT ExprT

exprTyp :: ExprT -> Typ
exprTyp (BoolLit _) = BoolT
exprTyp (NumLit _) = NumT
exprTyp (VarT t _) = t
exprTyp (UnT t _ _) = t
exprTyp (BinT t _ _ _) = t
exprTyp (LetT t _ _ _) = t

-- Type check an expression
type Error = String
type TypContext = [(String, Typ)]   -- context of variable types
type TC = ExceptT Error (Reader TypContext)
runTC :: TC a -> a
runTC act = case runReader (runExceptT act) [] of
  Left err -> error err
  Right a -> a

tc :: ExprU -> TC ExprT
tc (FalseU) = pure $ BoolLit False
tc (TrueU) = pure $ BoolLit True
tc (NumU x) = pure $ NumLit x
tc (VarU var) = do
  mt <- asks (lookup var)
  case mt of
    Just t -> pure $ VarT t var
    Nothing -> throwError $ "undefined variable " ++ var
tc (UnU op e) = do
  let UnTyp targ tresult = unTyp op
  e' <- tc e
  let t = exprTyp e'
  when (t /= targ) $ throwError $ "op " ++ show op ++
    " expected arg of type " ++ show targ ++ ", got " ++ show t
  pure $ UnT tresult op e'
  where
    unTyp NegOp = UnTyp NumT NumT
    unTyp NotOp = UnTyp BoolT BoolT
tc (BinU EqualsOp e1 e2) = do
  e1' <- tc e1
  e2' <- tc e2
  let t1 = exprTyp e1'
      t2 = exprTyp e2'
  when (t1 /= t2) $ throwError $ "op EqualOp needs to compare equal types"
  pure $ BinT BoolT EqualsOp e1' e2'
tc (BinU op e1 e2) = do
  let BinTyp targ1 targ2 tresult = binTyp op
  e1' <- tc e1
  e2' <- tc e2
  let t1 = exprTyp e1'
      t2 = exprTyp e2'
  when (t1 /= targ1) $ throwError $ "op " ++ show op ++
    " expected left arg of type " ++ show targ1 ++ ", got " ++ show t1
  when (t2 /= targ2) $ throwError $ "op " ++ show op ++
    " expected right arg of type " ++ show targ2 ++ ", got " ++ show t2
  pure $ BinT tresult op e1' e2'
  where
    binTyp PlusOp = BinTyp NumT NumT NumT
    binTyp MulOp = BinTyp NumT NumT NumT
    binTyp AndOp = BinTyp BoolT BoolT BoolT
    binTyp OrOp = BinTyp BoolT BoolT BoolT
    binTyp EqualsOp = error "internal error"
tc (LetU var e1 e2) = do
  e1' <- tc e1
  let t1 = exprTyp e1'
  e2' <- local ((var,t1):) $ tc e2
  let t2 = exprTyp e2'
  pure $ LetT t2 var e1' e2'

-- Evaluate a typed expression
internalerror :: a
internalerror = error "can't happen, internal error in type checker"

-- Values
data Value
  = BoolV Bool
  | NumV Double
  deriving (Show)

type ValContext = [(String, Value)]   -- context of variable values
type E = Reader ValContext
runE :: E a -> a
runE act = runReader act []

eval :: ExprT -> E Value
eval (BoolLit b) = pure $ BoolV b
eval (NumLit x) = pure $ NumV x
eval (VarT _ var) = do
  mt <- asks (lookup var)
  case mt of
    Just v -> pure $ v
    Nothing -> internalerror
eval (UnT _ op e) = run op <$> eval e
  where run NegOp (NumV x) = NumV (-x)
        run NotOp (BoolV b) = BoolV (not b)
        run _ _ = internalerror
eval (BinT _ op e1 e2) = run op <$> eval e1 <*> eval e2
  where run EqualsOp (BoolV v1) (BoolV v2) = BoolV $ v1 == v2
        run EqualsOp (NumV v1) (NumV v2) = BoolV $ v1 == v2
        run PlusOp (NumV v1) (NumV v2) = NumV $ v1 + v2
        run MulOp (NumV v1) (NumV v2) = NumV $ v1 * v2
        run AndOp (BoolV v1) (BoolV v2) = BoolV $ v1 && v2
        run OrOp (BoolV v1) (BoolV v2) = BoolV $ v1 || v2
        run _ _ _ = internalerror
eval (LetT _ var e1 e2) = do
  v1 <- eval e1
  local ((var,v1):) $ eval e2

expr1 :: ExprU
expr1 = LetU "x" (BinU PlusOp (NumU 2) (NumU 3)) (LetU "y" (BinU MulOp (VarU "x") (NumU 5)) (BinU EqualsOp (VarU "y") (NumU 25)))

val1 :: Value
val1 = let e1' = runTC (tc expr1) in runE (eval e1')

main :: IO ()
main = do
  print $ val1