将简单类型语言的非类型 AST 转换为 GADT

我有一个代表简单语言 AST 的 ADT：

data UTerm = UTrue
      | UFalse
      | UIf UTerm UTerm UTerm
      | UZero
      | USucc UTerm
      | UIsZero UTerm

该数据结构可以表示不遵循类型的无效术语 语言规则，例如UIsZero UFalse，所以我想使用 GADT 强制类型正确：

{-# LANGUAGE GADTs #-}

data TTerm a where
  TTrue :: TTerm Bool
  TFalse :: TTerm Bool
  TIf :: TTerm Bool -> TTerm a -> TTerm a -> TTerm a
  TZero :: TTerm Int
  TSucc :: TTerm Int -> TTerm Int
  TIsZero :: TTerm Int -> TTerm Bool

我的问题是输入检查 UTerm 并将其转换为 TTerm。我的第一次 以为是UTerm -> Maybe (TTerm a)，但这当然行不通，因为 它并不对所有人都有效as。我什至不知道类型是什么，因为 我们不知道是否a将是 Int 或 Bool。然后我想我可以写一个 对每个可能值的不同类型检查函数a:

import Control.Applicative

typecheckbool :: UTerm -> Maybe (TTerm Bool)
typecheckbool UTrue = Just TTrue
typecheckbool UFalse = Just TFalse
typecheckbool (UIsZero a) = TIsZero <$> typecheckint a
typecheckbool _ = Nothing

typecheckint :: UTerm -> Maybe (TTerm Int)
typecheckint UZero = Just TZero
typecheckint (USucc a) = TSucc <$> typecheckint a
typecheckint (UIf a b c) = TIf <$> typecheckbool a <*> typecheckint b <*> typecheckint c
typecheckint UTrue = Nothing
typecheckint UFalse = Nothing
typecheckint (UIsZero _) = Nothing

这适用于某些情况，对于 TIf 需要其语言的子集 结果和替代是整数（但是TIf TTrue TFalse TTrue实际上是 完全有效），并且我们知道表达式的目标类型 打字。

从 UTerm 转换为 TTerm 的正确方法是什么？

标准技术是定义一个存在类型：

data ETerm_ where
    ETerm_ :: TTerm a -> ETerm

在这种情况下，您可能还需要一些术语级别的证据来证明您拥有哪种类型；例如

data Type a where
    TInt :: Type Int
    TBool :: Type Bool

那么真实的ETerm看起来像这样：

data ETerm where
    ETerm :: Type a -> TTerm a -> ETerm

类型检查的有趣案例是这样的

typeCheck (UIf ucond ut uf) = do
    ETerm TBool tcond <- typeCheck ucond
    ETerm tyt tt <- typeCheck ut
    ETerm tyf tf <- typeCheck uf
    case (tyt, tyf) of
        (TBool, TBool) -> return (ETerm TBool (TIf tcond tt tf))
        (TInt , TInt ) -> return (ETerm TInt  (TIf tcond tt tf))
        _ -> fail "branches have different types"