haskell - 构造函数内部和构造函数外部 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一个。

2. 没有。构造函数 BarProxy 具有 2 级多态类型 (forall a.Bar a => Proxy a) -> BarProxy。 这意味着只有在以下情况下参数 p 才可以传递给 BarProxy: p 的 all 类型 a 具有 Proxy 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 universal BarProxy 类型。 对于存在性参数，参数 p 的类型应为任一 Proxy FooA 或 Proxy FooB (通过 {a | a 是 Bar} = {FooA,FooB} 的实例进行存在量化)。 另一方面，对于通用类型，p 应该具有类型两者 Proxy FooA 和 Proxy FooB (在同一组上通用量化)。 让我们考虑下面的三个代理。

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

   Existential BarProxy 接受三者中的任何一个，而Universal One 仅接受proxyPoly。

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