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

Question

我正在用Haskell编写一种特定于域的语言，并且已经确定了一个带有两个AST的设计:一个初始的非类型化的表示语法的和一个代表所有内容的最终类型的。我正在写最后一个作为一个GADT，以获得更好的打字。

我认为它几乎可以工作，但是我在编写转换初始-> final的函数时遇到了困难(检查类型，再加上一些没有显示的内容，比如所有引用都对应于变量)。

下面是一个简化的示例：

{-# 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))类型的值，但是我还没有打开它们，检查类型是否对齐(两个a都应该是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的返回类型(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非常聪明，它知道任何a中的两个TypedExpr2都必须匹配，所以如果您试图在末尾使用错误的总体返回类型，它会捕获您。精彩的!

Answer 1

从技术上讲，它是可行的，但这很不方便:您必须“挖掘”，直到找到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"

我会寻找其他选择。当构造者数量较大时，上述方法会受到组合爆炸的影响。

Answer 2

我的建议是使用“普通”表示类型的宇宙(带有解释类型函数)，然后将存在类型的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 3

以下解决方案很容易回答您的确切问题：

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

然而，有相当多的迹象表明，设计迷宫在那里。

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

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

我不明白为什么UAdd构造函数超过了Untyped值，而不是Int，我也不明白是什么使您采用了这种多级AST策略。

我可以继续，但我会打破这里，只是建议你重新设计你的模式。