将DSL的无类型表示转换为类型化表示

Question

举个简单的语言吧

data E where
  ValE :: Typeable a => a -> E
  AppE :: E -> E -> E

然后可以将其转换为类型化表示:

data T a where
  ValT :: Typeable a => a -> T a
  AppT :: T (a -> b) -> T a -> T b
  deriving Typeable

我尝试过各种方法,例如:

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2)

这不起作用,我收到以下错误消息:

约束中的模糊类型变量'a':
'Typeable a'
源于使用`e2t'...
可能的修复:添加修复这些类型变量的类型签名

但是,如果我喜欢这样的话

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2 :: Maybe (T Int))

它汇编.

Answer 1

这是正确的。您可能没有意识到，但您正在尝试对您的语言进行类型推断。如果您想将表达式转换f x为类型化的 GADT，仅仅知道结果类型是不够的。我们可以使用f :: Bool -> Intwith x :: Bool、f :: (Int -> Int) -> Intwithx :: Int -> Int等。并且您的类型化表示声称知道这一点，特别是因为它需要Typeable其常量（如果您没有约束，您可能可以谎称知道它是什么类型Typeable） 。

e2t需要了解表达式的预期类型。您需要某种方法来确定应用程序的参数预期是什么类型。也许你可以通过说一些不同的话来避免需要这个，即：

e2t :: E -> Maybe (exists a. T a)

也就是说，您只是想看看是否E可以给定一个类型，但它不会告诉它应该是什么类型，而是告诉您。这是自下而上的推理，通常更容易。对此进行编码：

data AnyT where
    AnyT :: Typeable a => T a -> AnyT

嗯，玩了一段时间后，我意识到你在备份时遇到了完全相同的问题。我认为仅使用Data.Typeable. 您需要重新创建类似dynAppfrom 的东西Data.Dynamic，但是 for Ts 而不是常规的 Haskell 类型。即，您将必须对TypeReps 进行一些操作，然后在某个时刻插入“相信我” unsafeCoerce，一旦您知道它是安全的。但据我所知，你无法让编译器相信它是安全的。

TypeRep这在 Agda 中是可能的，因为编译器可以观察到 s上的等效操作。在学习该语言时，这可能是一个很好的练习。