在Haskell中有可能有健忘的类型同义词吗？

Question

如果我有一个带有幻像参数的类型,我有时只会关心它,如下所示:

data Foo p a b = Bar a b

是否有任何黑客方式来编写一个类型的同义词Baz,这Baz a b是Foo p a b为了一些p我忘记的？

你做不到:

type Baz a b = Foo p a b

虽然你可以做(​​有适当的扩展):

type Baz a b = forall p.Foo p a b

它看起来不像我想要的那样,因为我无法将类型的值转换Foo P1 a b为类型Baz a b,并带有关于"刚性类型变量"的消息.

您是否需要另一层构造器来实现此效果,如下所示？你能简单解释一下原因吗？

data Baz' a b = forall p.Baz' (Foo p a b)

Answer 1

目前没有办法将此作为类型同义词.但是,如果您有GHC 7.10,则可以打开PartialTypeSignatures扩展名并写入Foo _ a b.使用-fno-warn-partial-type-signatures要求GHC不是要提醒你每次以这种方式离开孔.

Answer 2

使用类型同义词无法可靠地完成此操作.您需要存在类型或rank-n类型.

问题是Haskell允许类型同义词完全是可互替的.即,当您定义时type Baz a b = Foo p a b,在您拥有的每个上下文中Foo p a b,您将被允许使用Baz a b,反之亦然.例如,如果你有这种类型的函数:

f1 :: Foo Something a b -> Whatever Something b a

然后由于可替代性,它与此类型相同:

f1 :: Baz a b -> Whatever Something b a

就像这样:

f1 :: Foo p a b -> Whatever Something b a

...然后你可以专门研究这个:

f1 :: Foo SomethingElse a b -> Whatever Something b a

所以,你可以做什么？一种是定义存在的包装类型:

{-# LANGUAGE ExistentialTypes #-}

data Baz a b = forall p. Baz (Foo p a b)

做同样事情的另一种方式:

{-# LANGUAGE GADTs #-}

data Baz a b where
     Baz :: Foo p a b -> Baz a b

第二种方式:rank-n类型和continuation-passing风格:

{-# LANGUAGE RankNTypes #-}

-- To consume one of these, you pass a "callback" function to `runBaz`,
-- which is not allowed to restrict the type variable `p`.
newtype Baz a b = Baz { runBaz :: forall p r. (Foo p a b -> r) -> r }

makeBaz :: Foo p a -> Baz a b
makeBaz foo = Baz ($foo)

第三种方式,你已经尝试过(我被告知)不能很好地工作:输入同义词+ impredicative类型(forall在许多情况下,需要将同义词作为类型参数出现).