将简单类型语言的无类型AST转换为GADT [英] Converting an untyped AST for a simple typed language into a GADT

问题描述

  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 
 TIsero :: TTerm Int  - > TTerm Bool 
  

我的问题是键入检查UTerm并将其转换为TTerm。我的第一个
认为是 UTerm - >也许（TTerm a），但这当然不起作用，因为
对所有 a s都是无效的。我甚至不知道类型是什么，因为
我们不知道 a 是Int或Bool。然后我想我可以为 a 的每个可能值写一个
的不同类型检查函数：

  import Control.Applicative 
 
 typecheckbool :: UTerm  - >也许（TTerm布尔）
 typecheckbool UTrue =只是TTrue 
 typecheckbool UFalse =只是TFalse 
 typecheckbool（UIsZero a）= TIsZero< $> typecheckint a 
 typecheckbool _ = Nothing 
 
 typecheckint :: UTerm  - >可能（TTerm Int）
 typecheckint UZero =只是TZero 
 typecheckint（USucc a）= TSucc< $>类型
 typecheckint（UIf a b c）= TIf< $> typecheckbool a< *> typecheckint b * typecheckint c 
 typecheckint UTrue = Nothing 
 typecheckint UFalse = Nothing 
 typecheckint（UIsZero _）= Nothing 
  

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

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

解决方案

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

  data ETerm_ where 
 ETerm_ :: TTerm a  - > ETerm 
  

在这种情况下，您可能还需要一些术语级证据，例如

 数据类型a其中
 TInt ::类型Int 
 TBool ::类型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） - >返回（ETerm TBool（TIf tcond tt tf））
（TInt，TInt） - >返回（ETerm TInt（TIf tcond tt tf））
 _  - >失败分支有不同的类型
  

I have an ADT representing the AST for a simple language:

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

This data structure can represent invalid terms that don't follow the type rules of the language, like UIsZero UFalse, so I'd like to use a GADT that enforces well-typedness:

{-# 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

My problem is to type check a UTerm and convert it into a TTerm. My first thought was UTerm -> Maybe (TTerm a), but this of course doesn't work because it's not valid for all as. I don't even know what the type would be, because we don't know if a is going to be Int or Bool. Then I thought I could write a different type checking function for each of the possible values of 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

This works for some cases, for a subset of the language where TIf requires its consequent and alternative are Ints (But TIf TTrue TFalse TTrue is actually totally valid), and where we know the target type of the expression we're typing.

What's the right way to convert from a UTerm to a TTerm?

解决方案

The standard technique is to define an existential type:

data ETerm_ where
    ETerm_ :: TTerm a -> ETerm

In this case, you may also want some term-level evidence of which type you have; e.g.

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

then the real ETerm would look like this:

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

The interesting case of type checking is then something like

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"

这篇关于将简单类型语言的无类型AST转换为GADT的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！