是否可以确保两个GADT类型变量是相同的而没有依赖类型？

Question

我正在编写一个编译器,我正在为我的IR使用GADT,但是我的其他所有东西都使用标准数据类型.我在从旧数据类型转换为GADT期间遇到了麻烦.我试图用下面的小/简化语言重新创建这种情况.

首先,我有以下数据类型:

data OldLVal = VarOL Int -- The nth variable. Can be used to construct a Temp later.
             | LDeref OldLVal

data Exp = Var Int -- See above
         | IntT Int32
         | Deref Exp

data Statement = AssignStmt OldLVal Exp
               | ...

我想将这些转换为这种中间形式:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}

-- Note: this is a Phantom type
data Temp a = Temp Int

data Type = IntT
          | PtrT Type

data Command where
    Assign :: NewLVal a -> Pure a -> Command
    ...

data NewLVal :: Type -> * where
    VarNL :: Temp a -> NewLVal a
    DerefNL :: NewLVal ('PtrT ('Just a)) -> NewLVal a

data Pure :: Type -> * where
    ConstP :: Int32 -> Pure 'IntT
    ConstPtrP :: Int32 -> Pure ('PtrT a)
    VarP :: Temp a -> Pure a

此时,我只想编写从旧数据类型到新GADT的转换.现在,我有一些看起来像这样的东西.

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
   newLval <- convertLVal oldLval -- Either String (NewLVal a)
   pure <- convertPure exp -- Either String (Pure b)
   -- return $ Assign newLval pure -- Obvious failure. Can't ensure a ~ b.
   pure' <- matchType newLval pure -- Either String (Pure a)
   return $ Assign newLval pure'

-- Converts Pure b into Pure a. Should essentially be a noop, but simply 
-- proves that it is possible.
matchType :: NewLVal a -> Pure b -> Either String (Pure a)
matchType = undefined

我意识到我不能轻易写convert,所以我试图用这个想法来解决这个问题,这个想法matchType可以证明这两种类型确实是平等的.问题是:我怎么写matchType？如果我有完全依赖类型(或者我被告知),这会容易得多,但我可以在这里完成这段代码吗？

另一种方法是以某种方式提供newLval作为参数convertPure,但我认为本质上只是尝试使用依赖类型.

欢迎任何其他建议.

如果它有帮助,我也有一个可以转换Exp或OldLVal类型的函数:

class Typed a where
    typeOf :: a -> Type
instance Typed Exp where
    ...
instance Typed OldLVal where
    ...

编辑:

感谢下面的优秀答案,我已经能够完成这个模块的编写.

我最终使用了singletons下面提到的包.起初有点奇怪,但我发现在我开始理解我在做什么之后使用它是非常合理的.然而,我确实陷入了一个陷阱:类型convertLVal和convertPure需要存在的表达.

data WrappedPure = forall a. WrappedPure (Pure a, SType a)
data WrappedLVal = forall a. WrappedLVal (NewLVal a, SType a)

convertPure :: Exp -> Either String WrappedPure
convertLVal :: OldLVal -> Either String WrappedLVal

这意味着你必须打开那个存在主义convert,否则,下面的答案会告诉你如何.再次非常感谢.

Answer 1

您希望在运行时对某些类型级别的数据(即Type索引值的s)执行比较.但是当你运行代码并且值开始交互时,类型早已不复存在.它们以生成高效代码的名义被编译器擦除.因此,您需要手动重建已删除的类型级别数据,并使用一个值来提醒您忘记您正在查看的类型.你需要一份单件Type.

data SType t where
    SIntT :: SType IntT
    SPtrT :: SType t -> SType (PtrT t)

成员SType模样的成员Type-比较值的结构类似SPtrT (SPtrT SIntT)与的PtrT (PtrT IntT)-但是他们由(类型级)索引Types表示他们类似.对于每一个,t :: Type只有一个SType t(因此名称为单身),并且因为SType是GADT,在a上的模式匹配SType t告诉类型检查器关于t.单身人士跨越了严格执行的类型和价值之间的分离.

因此,在构建类型化树时,需要跟踪SType值的运行时间并在必要时进行比较.(这基本上等于编写部分验证的类型检查器.)有一个类Data.Type.Equality包含一个函数,它比较两个单例并告诉你它们的索引是否匹配.

instance TestEquality SType where
    -- testEquality :: SType t1 -> SType t2 -> Maybe (t1 :~: t2)
    testEquality SIntT SIntT = Just Refl
    testEquality (SPtrT t1) (SPtrT t2)
        | Just Refl <- testEquality t1 t2 = Just Refl
    testEquality _ _ = Nothing

在你的convert函数中应用它看起来大致如下:

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
    (newLval, newLValSType) <- convertLVal oldLval
    (pure, pureSType) <- convertPure exp
    case testEquality newLValSType pureSType of
        Just Refl -> return $ Assign newLval pure'
        Nothing -> Left "type mismatch"

实际上并没有很多依赖类型的程序,你不能伪装TypeInType和单身(有没有？),但是以"正常"和"单一"形式复制所有数据类型真的很麻烦.(该副本获取,即使你想传递的单身周围隐含更糟-看到Hasochism了解详细情况.)的singletons包可以产生许多样板给你的,但它并没有真正减轻因复制概念本身的痛苦.这就是为什么人们想要为Haskell添加真正的依赖类型的原因,但我们距离它还有好几年的时间.

新Type.Reflection模块包含一个重写的Typeable类.它TypeRep与GADT一样,可以作为一种"普遍的单身人士".但在我看来,使用它进行编程比使用单例编程更加尴尬.