haskell - 将简单类型语言的无类型 AST 转换为 GADT

Question

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

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) ，但这当然行不通，因为
并非对所有人都有效 a s。我什至不知道会是什么类型，因为
我们不知道 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 需要它的语言的子集
consequent 和 alternative 是 Ints (但 TIf TTrue TFalse TTrue 实际上是
完全有效)，并且我们知道我们的表达式的目标类型
打字。

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

Answer 1

标准技术是定义存在类型:

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"