コンストラクター内とコンストラクター外のforall数量詞の違い

debugcn 投稿 Dev

happycoder97

{-# 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"

このコードでは：

しないfoo1、任意のProxy a場所a種類のものであるがFoo、返すProxy aようaにインスタンスを持っているのBar？
ていないBarProxyコンストラクタ任意の受け入れProxy a、どこaのインスタンスを持っているのBar？それはどう違うのdata BarProxy = forall a. BarProxy (Bar a => Proxy a)ですか？
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)
   |                    ^^^^^^

細山

いいえ。私の理解では、の署名は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。
いいえ。コンストラクターにBarProxyはランク2のポリモーフィック型があり(forall a. Bar a => Proxy a) -> BarProxyます。引数はこの手段pに渡すことができるBarProxy場合にのみ、pタイプがあるProxy aため、すべてのタイプaのインスタンスですBar。存在記号が必要な場合は、次のように記述できます。
```
data BarProxy = forall a. Bar a => BarProxy (Proxy a)
```
または
```
data BarProxy where
  BarProxy :: forall a. Bar a => Proxy a -> BarProxy
```
-XGADTs有効。

実存型とユニバーサルBarProxy型を呼びましょう。存在記号の場合、引数の型はまたは（存在記号で）のいずれかである必要があります。一方、全称記号の場合は、と（同じセットで全称記号）の両方を入力する必要があります。以下の3つのプロキシについて考えてみましょう。forall a. Bar a => Proxy a -> BarProxy BarProxy(forall a. Bar a => Proxy a) -> BarProxy BarProxyp Proxy FooA Proxy FooB{a | a is an instance of 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
```
ExistentialBarProxyは3つのうちのいずれかを受け入れますが、Universal1はのみを受け入れますproxyPoly。
foo2 p = BarProxy (foo1 p)実存のためにコンパイルしBarProxyます。