haskell - 包装/展开通用量化类型

Question

我导入了一个数据类型 X ，定义为

data X a = X a

在本地，我定义了一个通用量化的数据类型， Y

type Y = forall a. X a

现在我需要定义两个函数， toY 和 fromY 。对于 fromY ，这个定义工作正常:

fromY :: Y -> X a
fromY a = a

但是如果我对 toY 尝试同样的事情，我会得到一个错误

Couldn't match type 'a' with 'a0'
'a' is a rigid type variable bound by the type signature for 'toY :: X a -> y'
'a0' is a rigid type variable bound by the type signature for 'toY :: X a -> X a0'
Expected type: X a0
Actual type: X a

如果我理解正确， toY 的类型签名将扩展为 forall a. X a -> (forall a0. X a0) 因为 Y 被定义为同义词，而不是新类型，因此定义中的两个 a 不匹配。

但如果是这样，那为什么 fromY type-check 会成功呢？除了使用 unsafeCoerce 之外，还有什么办法可以解决这个问题？

Answer 1

评论:

这更像是一条评论，但我不能真正把它放在那里，因为它不可读；请原谅我一次。

除了 dfeuer 已经告诉你的，你可能会看到(当你使用他的回答时)toY 现在真的很容易做，但你可能很难定义 fromY——因为你基本上丢失了类型信息，所以这个 将不起作用 :

{-# LANGUAGE GADTs #-}
module ExTypes where

data X a = X a

data Y where
  Y :: X a -> Y

fromY :: Y -> X a
fromY (Y a) = a

因为这里你有两个不同的 a s——一个来自构造函数 Y 一个来自 X a——实际上，如果你剥离定义并尝试编译: fromY (Y a) = a 编译器会告诉你 a 类型转义:

Couldn't match expected type `t' with actual type `X a'
  because type variable `a' would escape its scope
This (rigid, skolem) type variable is bound by
  a pattern with constructor
    Y :: forall a. X a -> Y,
  in an equation for `fromY'

我认为你现在唯一剩下的就是这样的:

useY :: (forall a . X a -> b) -> Y -> b
useY f (Y x) = f x

但这可能证明不是太有用。

问题是你通常应该更多地限制 forall a (使用类型类)以获得任何有意义的行为 - 但当然我在这里无能为力。

这个 wiki article 可能对你感兴趣。