parsing - 在 Haskell 中解析谓词

Question

我想解析一个谓词，例如:"3 > 2" 或 "MyVar = 0"。

理想情况下，我会使用一个小的 GADT 来表示谓词:

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Var :: String -> Expr Int
    Add :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool
    Mt  :: Eq a => Expr a -> Expr a -> Expr Bool

表达式 3 > 2 将解析为 Mt (I 3) (I 2)。

我试图用 Parsec 来解决这个问题。但是，模块 Text.Parsec.Expr只处理表达式，类型为 a -> a -> a。有什么建议吗？

Answer 1

直接解析成 GADT 实际上有点棘手。根据我的经验，通常最好先解析为无类型的 ADT(其中 a -> a -> a 类型很自然)，然后通过转换它来单独“类型检查”ADT进入所需的 GADT。主要缺点是您必须为非类型化和类型化抽象语法树定义两种并行类型。 (从技术上讲，您可以使用一些类型级别的技巧来解决这个问题，但对于小型语言来说，这是不值得的。)但是，最终的设计更易于使用，而且通常更灵活。

换句话说，我建议使用 Parsec 来解析为未类型化的 ADT:

data UExpr where
  UI :: Int -> UExpr
  UB :: Bool -> UExpr
  UVar :: String -> UExpr
  UAdd :: UExpr -> UExpr -> UExpr
  UEq :: UExpr -> UExpr -> UExpr
  UMt :: UExpr -> UExpr -> UExpr

然后写一个类型检查器:

tc :: UExpr -> Expr a

实际上，您无法像那样编写tc。相反，您需要将其分解为针对不同表达式类型的相互递归类型检查器:

tc_bool :: UExpr -> Expr Bool
tc_int :: UExpr -> Expr Int

您可能希望在提供有效变量列表的 Reader monad 中运行它们。 (类型检查通常涉及检查变量的类型。在您的情况下，您只有整数变量，但确保在类型检查阶段定义变量仍然有意义。)

如果您遇到困难，将有一个完整的解决方案...

剧透

.

.

.

正如我所说，我首先会为未类型化的 UExpr ADT 编写一个 Parsec 解析器。请注意，Text.Parsec.Expr 机制适用于 UExpr -> UExpr -> UExpr 运算符:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS -Wall -Wno-missing-signatures #-}

import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.String
import Text.Parsec.Language
import Control.Monad.Reader
import Control.Exception
import Data.Maybe (fromJust)
import qualified Text.Parsec.Token as P

lexer = P.makeTokenParser haskellDef { P.reservedNames = ["true","false"] }

identifier = P.identifier lexer
integer = P.integer lexer
parens = P.parens lexer
reserved = P.reserved lexer
reservedOp = P.reservedOp lexer
symbol = P.symbol lexer

data UExpr where
  UI :: Int -> UExpr
  UB :: Bool -> UExpr
  UVar :: String -> UExpr
  UAdd :: UExpr -> UExpr -> UExpr
  UEq :: UExpr -> UExpr -> UExpr
  UMt :: UExpr -> UExpr -> UExpr
  deriving (Show)

expr :: Parser UExpr
expr = buildExpressionParser
  [ [Infix (UAdd <$ reservedOp "+") AssocLeft]
  , [Infix (UEq <$ reservedOp "=") AssocNone, Infix (UMt <$ reservedOp ">") AssocNone]
  ] term

term :: Parser UExpr
term = parens expr
  <|> UI . fromIntegral <$> integer
  <|> UB True <$ reserved "true"
  <|> UB False <$ reserved "false"
  <|> UVar <$> identifier

test_parser :: IO ()
test_parser = do
  parseTest expr "3 > 2"
  parseTest expr "MyVar = 0"

然后，我会编写一个类型检查器，可能类似于以下内容。请注意，对于类型检查，我们只需要验证变量名是否存在；我们不需要他们的值(value)观。但是，我使用了一个 Ctx 类型来进行类型检查和评估。

-- variable context (i.e., variable name/value pairs)
type Ctx = [(String, Int)]

data Expr a where
  I   :: Int  -> Expr Int
  B   :: Bool -> Expr Bool
  Var :: String -> Expr Int
  Add :: Expr Int -> Expr Int -> Expr Int
  Eq  :: (Show (Expr a), Eq a) => Expr a -> Expr a -> Expr Bool
  Mt  :: (Show (Expr a), Ord a) => Expr a -> Expr a -> Expr Bool
deriving instance Show (Expr Bool)
deriving instance Show (Expr Int)

tc_bool :: UExpr -> Reader Ctx (Expr Bool)
tc_bool (UB b) = pure $ B b
tc_bool (UEq x y) = Eq <$> tc_int x <*> tc_int y
tc_bool (UMt x y) = Mt <$> tc_int x <*> tc_int y
tc_bool _ = error "type error: expecting a boolean expression"

tc_int :: UExpr -> Reader Ctx (Expr Int)
tc_int (UI n) = pure $ I n
tc_int (UVar sym)
  = do mval <- asks (lookup sym)
       case mval of Just _ -> pure $ Var sym
                    _      -> error "type error: undefined variables"
tc_int (UAdd x y) = Add <$> tc_int x <*> tc_int y
tc_int _ = error "type error: expecting an integer expression"

test_tc :: IO ()
test_tc = do
  print $ run_tc_bool (UMt (UI 3) (UI 2))
  print $ run_tc_bool (UEq (UVar "MyVar") (UI 0))
  -- now some type errors
  handle showError $ print $ run_tc_bool (UMt (UB False) (UI 2))
  handle showError $ print $ run_tc_bool (UAdd (UEq (UI 1) (UI 1)) (UI 1))

  where showError :: ErrorCall -> IO ()
        showError e = print e

        run_tc_bool e = runReader (tc_bool e) [("MyVar", 42)]

您可能会惊讶地发现，编写类型检查器的最自然方式实际上并不是“使用”GADT。它可以同样容易地使用 bool 和整数表达式的两种不同类型来编写。如果您真的尝试直接解析到 GADT 中，您会发现同样的事情。解析器代码需要非常清楚地分为 Parser (Expr Bool) 类型的 bool 表达式解析器和 Parser (Expr Int) 类型的整数表达式解析器，并且没有直接的方法来编写单个 Parser (Expr a)。

实际上，GADT 表示的优势只体现在评估阶段，您可以编写一个简单的、类型安全的评估器，不会触发“非穷举模式”警告，如下所示:

eval :: Expr a -> Reader Ctx a
eval (I n) = pure n
eval (B b) = pure b
eval (Var sym) = fromJust <$> asks (lookup sym)
eval (Add x y) = (+) <$> eval x <*> eval y
eval (Eq x y) = (==) <$> eval x <*> eval y
eval (Mt x y) = (>) <$> eval x <*> eval y

test_eval :: IO ()
test_eval = do
  print $ run_eval (Mt (I 3) (I 2))
  print $ run_eval (Eq (Var "MyVar") (I 0))

  where run_eval e = runReader (eval e) [("MyVar", 42)]