包装/展开通用量化类型

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定义中的两个s不匹配.

但如果是这种情况,为什么fromY类型检查成功呢？除了使用之外,还有什么解决这个问题的方法unsafeCoerce吗？

Answer 1

你声称要定义一个存在类型,但你没有.

type Y = forall a. X a

定义了一种普遍量化的类型.对于一些有型Y,就必须有类型X a为每一个 a.要创建一个存在量化的类型,你总是需要使用data,我发现GADT语法比传统的存在语法更容易理解.

data Y where
  Y :: forall a . X a -> Y

在forall那里实际上是可选的,但我想澄清的事情.

我现在太困了以解决你的其他问题,但是如果没有其他人的话,明天我会再试一次.

Answer 2

备注:

这更像是一个评论,但我无法真正把它放在那里,因为它本来是不可读的; 请原谅我一次.

除了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

在这里你有两个不同的as - 一个来自构造函数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文章可能会对您有所了解.