构造函数内部和构造函数外部的 forall 量词之间的区别

Question

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}

import Data.Proxy

data Foo = FooA | FooB

class Bar (a :: k) where
    bar :: Proxy a -> Int

instance Bar FooA where
    bar _ = 1

instance Bar FooB where
    bar _ = 2

foo1 :: forall (a :: Foo). Proxy a -> (Bar a => Proxy a)
foo1 p = p

data BarProxy = BarProxy (forall a. Bar a => Proxy a)

foo2 :: forall (a :: Foo). Proxy a -> BarProxy
foo2 p = BarProxy (foo1 p)

main = print "Hello World"

在这段代码中：

1. 没有foo1，给定任何Proxy a，其中a 是一种Foo，返回一个Proxy a 使得a 有一个Bar 的实例？
2. BarProxy 构造函数不接受任何Proxy a，其中a 有Bar 的实例？与data BarProxy = forall a. BarProxy (Bar a => Proxy a) 有何不同？
3. 为什么foo2 p = BarProxy (foo1 p) 失败并出现以下错误？

Test6.hs:27:20: error:
    • Couldn't match type ‘a1’ with ‘a’
      ‘a1’ is a rigid type variable bound by
        a type expected by the context:
          forall (a1 :: Foo). Bar a1 => Proxy a1
        at Test6.hs:27:10-26
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo2 :: forall (a :: Foo). Proxy a -> BarProxy
        at Test6.hs:26:1-46
      Expected type: Proxy a1
        Actual type: Proxy a
    • In the first argument of ‘BarProxy’, namely ‘(foo1 p)’
      In the expression: BarProxy (foo1 p)
      In an equation for ‘foo2’: foo2 p = BarProxy (foo1 p)
    • Relevant bindings include
        p :: Proxy a (bound at Test6.hs:27:6)
        foo2 :: Proxy a -> BarProxy (bound at Test6.hs:27:1)
   |
27 | foo2 p = BarProxy (foo1 p)
   |                    ^^^^^^

Answer 1

1. 没有。我的理解是foo1 的签名与forall (a :: Foo). Bar a => Proxy a -> Proxy a 相同（虽然我找不到任何文件）。 在 ghci 中，:t foo1 给出foo1 :: Bar a => Proxy a -> Proxy a。 给定任何Proxy a，其中a 是一种Foo 和Bar 的一个实例，它返回Proxy a。

2. 没有。构造函数BarProxy 具有等级2 多态类型(forall a. Bar a => Proxy a) -> BarProxy。 这意味着参数 p 可以传递给 BarProxy 仅当 p 的类型为Proxy a，all 类型为a，它是Bar 的一个实例。 如果你想要一个存在量化的，你可以写

   data BarProxy = forall a. Bar a => BarProxy (Proxy a)
   

   或

   data BarProxy where
     BarProxy :: forall a. Bar a => Proxy a -> BarProxy
   

   启用-XGADTs。

   让我们打电话 BarProxy 类型为 forall a. Bar a => Proxy a -> BarProxy 存在 BarProxy 和 类型为(forall a. Bar a => Proxy a) -> BarProxy 通用 BarProxy。 对于存在论，参数p 应该具有类型either Proxy FooA 或 Proxy FooB（存在于{a | a is an instance of Bar} = {FooA,FooB} 上量化）。 另一方面，对于通用的，p 应该具有类型 both Proxy FooA 和 Proxy FooB（在同一集合上普遍量化）。 让我们考虑下面的三个代理。

   proxyFooA :: Proxy FooA
   proxyFooA = Proxy
   
   proxyFooB :: Proxy FooB
   proxyFooB = Proxy
   
   proxyPoly :: forall a. Proxy a
   proxyPoly = Proxy
   

   Existential BarProxy 接受这三个中的任何一个，而通用一个只接受 proxyPoly。

3. foo2 p = BarProxy (foo1 p) 编译为存在的BarProxy。