5

给定一种简单的语言，说

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))

它编译。

4

1 回答 1

2

这是正确的。您可能没有意识到这一点，但您正在尝试对您的语言进行类型推断。如果要将表达式转换为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，但使用Ts 而不是常规的 Haskell 类型。即你必须对TypeReps 做一些操作，然后在unsafeCoerce你知道它是安全的时候插入一个“just trust me”。但据我所知，您无法说服编译器它是安全的。

这在 Agda 中是可能的，因为TypeReps 上的等价操作对于编译器是可观察的。学习该语言时，这可能是一个很好的练习。

于 2010-10-31T18:23:10.287 回答