程序员经验分享-hwhale

设计简单静态类型语言的类型系统（在 Haskell 中）

2024-01-04

我一直在考虑为命令式静态类型语言编写一个解释器，以习惯函数式编程和 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代表返回类型。问题是我真的不知道如何强制类型仅是我打算支持的类型。它看起来更简洁，但我也不确定这是否“正确”。

最后，是否有任何资源以适合初学者的方式介绍该主题？我不想太深入这个主题，但我很想阅读……嗯，设计类型系统时的常见原则/注意事项。


根据评论，不要尝试将此作为您的第一个口译员。如果您还没有为非类型化 lambda 演算编写解释器或完成教程，例如48小时内给自己写一个计划 https://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours，先这样做。

无论如何，这是一种静态类型表达式语言的解释器的简单实现，具有布尔和数字类型、一些内置运算符（包括具有临时多态性的运算符）、变量和let x=... in ...变量绑定，但没有 lambda。它说明了设计类型化解释器的常见方法，但缺少足够的内容，因此不会破坏您的乐趣。

注意：我有意避免使用任何中级或高级 Haskell 功能（例如，类型ExprU and ExprT没有统一为单一的多态类型——不”生长的树 http://www.jucs.org/jucs_23_1/trees_that_grow/jucs_23_01_0042_0062_najd.pdf“对于我们来说！；我还没有使用 GADT利用 Haskell 类型系统 https://hackage.haskell.org/package/glambda输入目标语言； ETC。）。这些先进的技术可以产生更安全的代码——而且也非常棒，所以你将来肯定想看看它们——但它们并不是让基本类型解释器工作所必需的。

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

{-# OPTIONS_GHC -Wall #-}

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

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

您在问题中提到，您正在努力解决两种方法：一开始就按类型划分运算符，而不是以某种方式反映 Haskell 类型系统中的运算符类型。你对第一种方法的直觉是正确的——它的效果不会很好。第二种方法是可行的，但是您很快就会遇到一些非常先进的 Haskell 技术，而您可能还没有准备好。

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

-- 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

在具有一流函数的语言中，我们可能会将这些类型组合成一个 HaskellTyp它不仅可以表示 bool 和 nums 等“原始”类型，还可以表示函数类型，例如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

在我们的语言中，变量的类型也很简单。我们只允许使用变量after它们已经被定义（由LetU绑定 - 见下文），因此它们的类型在当前上下文中始终可用：

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

一元运算符的类型很简单。仅有的两个一元运算符是“negate”和“not”，并且两者仅适用于精确的一种参数类型并产生精确的一种结果类型。这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

因为哈斯克尔==运算符是多态的，我们可以添加一个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可以在没有运行时类型错误的情况下进行解释。也就是说，用这种简单的语言来说，fact程序类型检查比类型检查期间计算的类型更重要。在更复杂的语言中，类型注释可能更有用。

无论如何，就是这样。这是完整的代码和示例程序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
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

Haskell

functionalprogramming

interpreter

typesystems

设计简单静态类型语言的类型系统（在 Haskell 中） 的相关文章

  • 与 Functor 不同，Monad 可以改变形状？

    我一直很喜欢以下关于单子相对于函子的力量的直观解释 单子可以改变形状 函子不能 例如 length fmap f 1 2 3 总是等于3 然而 对于单子来说 length 1 2 3 gt gt g往往不等于3 例如 如果g定义为 g Nu

  • 这个实例有什么问题：ArrowApply Automaton？

    我希望 Automaton 有实例 ArrowApply 但 Control Arrow Transformer Automaton 没有 我认为下面的代码会表现良好 data Automaton b c Auto runAuto b gt

  • 如何测试自定义 StateT 的 Monad 实例？

    我正在学习 Monad Transformers 其中一个练习要求实现 Monad 实例StateT 我想使用以下方法测试我的实现是否符合 Monad 法则validity https github com NorfairKing vali

  • 来自数据类型的 Haskell 随机数

    我对 Haskell 还很陌生 我有一个数据类型 data Sentence Prop Int No Sentence And Sentence Or Sentence deriving Eq 我已经为它写了一个 Show 实例 然而 无论

  • Java泛型 - 实现像map这样的高阶函数

    我决定用 Java 编写一些常见的高阶函数 map filter reduce 等 这些函数通过泛型实现类型安全 但我在一个特定函数中遇到通配符匹配问题 为了完整起见 函子接口是这样的 The interface containing th

  • 为什么 GHC 在这里推断出单态类型，即使禁用了单态限制？

    这是由解析 f f pure 的类型 https stackoverflow com questions 55388119 resolving the type of f f pure 55388309 noredirect 1 comme

  • IntSummaryStatistics的summaryStatistics方法

    为什么空 IntStream 上的 summaryStatistics 方法返回整数的最大和最小值作为流中存在的最大和最小 int 值 IntStream intStream IntStream of IntSummaryStatistic

  • Cabal：使用源代码构建目录

    我有一个src目录 在这个目录中我有Main hs文件和Test目录 在里面Test我有的目录Test hs模块 我需要用 cabal 来编译它 在我的阴谋集团文件中 我有 Executable main hs or lhs file co

  • Haskell/Idris 中的开放类型级别证明

    在 Idris Haskell 中 可以通过注释类型并使用 GADT 构造函数 例如使用 Vect 来证明数据的属性 但这需要将属性硬编码到类型中 例如 Vect 必须是与 List 不同的类型 是否有可能拥有具有开放属性集的类型 例如同时

  • 需要澄清令人困惑的 Http4s 消息类型 `Response[F]` / `Request[F]`

    我很难理解为什么Request and Response参数化为F 类似的东西是猫效应数据类型资源 从文档中 https typelevel org cats effect docs std resource https typelevel

  • 当约束成立时，将没有约束的 GADT 转换为另一个有约束的 GADT

    我们能否将构造函数没有给定约束的 GADT 转换为具有上述约束的 GADT 我想这样做是因为我想要深度嵌入箭头并用 目前 似乎需要的表示做一些有趣的事情Typeable 一个理由 https stackoverflow com a 1223

  • monadicIO 的工作原理

    我有以下代码 fastShuffle a gt IO a fastShuffle a

  • 不理解 Monoid 定义中态射的表示法

    我试图理解什么Monoid是从范畴论的角度来看的 但我对用来描述它的符号有点困惑 这是维基百科 在范畴论中 幺半群范畴 C I 中的幺半群 或幺半群对象 M 是一个对象 M 和两个态射 M M M 称为乘法 I M 称为单位 我的困惑在于态

  • Haskell 有 takeUntil 函数吗？

    目前我正在使用 takeWhile x gt x 1 x 89 l 从列表中获取最多为 1 或 89 的元素 但是 结果不包括这些标记值 Haskell 是否有一个标准函数可以提供这种变化takeWhile结果中包含哨兵 到目前为止 我对胡

  • 带有参考的 Haskell 数据类型

    我正在实现 Ukkonen 的算法 该算法要求树的所有叶子都包含对同一整数的引用 并且我在 Haskell 中执行此操作是为了了解有关该语言的更多信息 但是 我很难编写出执行此操作的数据类型 Node has children indexe

  • 在不同上下文中使用的多态变量 haskell

    我有以下一段 Haskell 代码 foo Num a gt a gt a gt Either Integer Double gt Either Integer Double foo f x case x of Left i gt Left

  • Pandoc“无法找到已安装模块的模块...”

    我目前正在尝试使用 pandoc 作为 Haskell 模块 而不是程序 将 MediaWiki 文本转换为其他格式 我们假设这个程序 import Text Pandoc Readers MediaWiki main do print f

  • Haskell：去掉 liftM2 中的括号

    如何去掉标有的括号 而不引入新名称 如果能分成多行就更好了 liftM2 somefunc arg1 get arg2 somefunc arg3 get arg3 您可以使用以下方法删除最后一个 但另一个显然不能在不引入新名称的情况下被删

  • Haskell 中动态规划的高效表

    我已经编码了0 1背包问题 http en wikipedia org wiki Knapsack problem 0 1 knapsack problem在哈斯克尔 我对迄今为止所取得的懒惰和普遍性水平感到相当自豪 我首先提供用于创建和处

  • 命名和未命名类型

    问题 我最近开始阅读Golang规格手册 https golang org ref spec并陷入试图理解的困境有名和无名类型在相关部分 https golang org ref spec Types 我来自动态语言 这让我有点头疼 手册指

随机推荐

热门标签