在 Haskell 中，如何将无类型的 AST 解析为基于 GADT 的类型？

Question

我正在用 Haskell 编写一种特定领域的语言，并且已经确定 具有两个 AST 的设计：一个初始的无类型表示语法和 代表一切的最终类型。我把最后一个写成 GADT 以获得更好的类型检查。

我认为它几乎在工作，但我在编写一个函数时遇到了问题 转换初始 -> 最终（检查类型，以及其他一些未显示的内容， 就像所有引用都对应一个变量）。

这是一个简化的例子：

{-# LANGUAGE GADTs, StandaloneDeriving #-}

module Main where

-- untyped initial AST

data Untyped
  = UNum Int
  | UStr String
  | UAdd Untyped Untyped
  deriving (Show, Eq)

-- typed final AST

data Typed a where
  TNum :: Int    -> Typed Int
  TStr :: String -> Typed String
  TAdd :: Typed Int -> Typed Int -> Typed Int

deriving instance Eq   (Typed a)
deriving instance Show (Typed a)

-- wrapper that allows working with a `Typed a` for any `a`
data TypedExpr where
  TypedExpr :: Typed a -> TypedExpr

这是我对check 函数的尝试。基本情况很简单：

check :: Untyped -> Either String TypedExpr
check (UNum n) = Right $ TypedExpr $ TNum n
check (UStr s) = Right $ TypedExpr $ TStr s
-- check (Uadd e1 e2) = ???

但是如何添加Add？它可以递归地评估子表达式 Either String (TypedExpr (Typed a)) 类型的值，但我没有设法 打开包装，检查类型是否对齐（@9​​87654332@s 都应该是 Ints），然后 之后重新包装。我计划用大模式匹配来做这一切，但是 GHC 不同意：

My brain just exploded
  I can't handle pattern bindings for existential or GADT data constructors.
  Instead, use a case-expression, or do-notation, to unpack the constructor.

here已经解释过了，但我没看懂解释。它似乎 我不想要模式匹配。

更新：我一定是在不知不觉中搞砸了其他事情。模式匹配有效，如 Nikita 所示。

所以我摆弄着试图强迫事情进入 正确的形状，但还没有得到任何实质性的东西。如果这些是 只是Either String SomeValue 我想使用应用程序，对吗？是吗 可以向它们添加另一个级别的展开+类型检查吗？我怀疑this answer 接近我想要的，因为问题非常相似，但我还是不明白。 This 也可能是相关的。

更新：That first answer 毕竟正是我想要的。但是直到 chi 在没有额外的 Type 类型的情况下编写下面的中间版本时，我才知道如何。这是一个有效的解决方案。诀窍是用一个新类型标记TypedExprs，该类型仅表示Typed a 的return 类型（a）：

data Returns a where
  RNum :: Returns Int
  RStr :: Returns String

-- extend TypedExpr to include the return type
data TypedExpr2 where
  TypedExpr2 :: Returns a -> Typed a -> TypedExpr2

这样check 不必知道每个子表达式是否是原始的 TNum 或返回 TNum 的函数（如 Add）：

check :: Untyped -> Either String TypedExpr2
check (UNum n) = Right $ TypedExpr2 RNum (TNum n)
check (UStr s) = Right $ TypedExpr2 RStr (TStr s)
check (UAdd u1 u2) = do
  -- typecheck subexpressions, then unwrap by pattern matching
  TypedExpr2 r1 t1 <- check u1
  TypedExpr2 r2 t2 <- check u2
  -- check the tags to find out their return types
  case (r1, r2) of
    -- if correct, create an overall expression tagged with its return type
    (RNum, RNum) -> return $ TypedExpr2 RNum $ TAdd t1 t2
    _ -> Left "type error"

GHC 足够聪明，知道任何TypedExpr2 中的两个as 必须匹配， 因此，如果您尝试在 结尾。太棒了！

Answer 1

我的建议是使用类型域的“简单”表示（使用解释类型函数），然后将存在类型的 Singleton 物化存储在 TypedExpr 中，即类似于

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies #-}

data Type = TInt | TString

type family InterpT (a :: Type) where
  InterpT TInt = Int
  InterpT TString = String

-- plus the usual singletons stuff
-- ...

-- and finally
data Typed (a :: Type) where ...

data TypedExpr where
  TypedExpr :: Sing a -> Typed a -> TypedExpr

这样，你可以做类似的事情

check (UAdd e1 e2) = do
  TypedExpr t1 e1' <- check e1
  TypedExpr t2 e2' <- check e2
  case testEquality t1 t2 of
    Just Refl -> ... use e1' and e2' here, you know they have the same Type
    Nothing -> Left ...

找到一个完整的例子here。

Answer 2

您的确切问题可以通过以下解决方案轻松回答：

check (UAdd (UNum a) (UNum b)) = Right $ TypedExpr $ TAdd (TNum a) (TNum b)

但是那里有很多设计迷宫的迹象。

您是否意识到，一旦将某些内容放入TypedExpr，您就会丢失有关a 类型的所有信息？这会使您的 check 函数变得毫无意义。

我了解您这样做是因为这是您统一 GADT 类型的唯一方法，否则您无法实现 check 函数。但实际上它只是证明了您的建模错误并且 GADT 可能不适合您的用例。

我不明白为什么 UAdd 构造函数超过 Untyped 值，而不是 Int，我不明白是什么让你采用这种多阶段 AST 策略。

我可以继续，但我会在这里中断并建议您重新设计模型。

Answer 3

在技术上它是可行的，但它很不方便：你必须“挖掘”直到找到 GADT 构造函数。

check :: Untyped -> Either String TypedExpr
check (UNum n) = return $ TypedExpr $ TNum n
check (UStr s) = return $ TypedExpr $ TStr s
check (UAdd t1 t2) = do
    t1 <- check t1
    t2 <- check t2
    case (t1, t2) of
      (TypedExpr (TNum x)     , TypedExpr (TNum y))
         -> return $ TypedExpr $ TAdd (TNum x    ) (TNum y)
      (TypedExpr (TAdd x1 x2) , TypedExpr (TNum y))
         -> return $ TypedExpr $ TAdd (TAdd x1 x2) (TNum y)
      (TypedExpr (TNum x)     , TypedExpr (TAdd y1 y2))
         -> return $ TypedExpr $ TAdd (TNum x    ) (TAdd y1 y2)
      (TypedExpr (TAdd x1 x2) , TypedExpr (TAdd y1 y2))
         -> return $ TypedExpr $ TAdd (TAdd x1 x2) (TAdd y1 y2)
      _ -> Left "type error"

我会寻找替代品。当构造函数的数量很大时，上述方法会出现组合爆炸。