haskell - 什么时候永远不是全部

在下面的程序中，test₁将不编译，但test₂将编译。原因似乎是因为forall s.中的withModulus₁。似乎由于s，每次调用withModulus₁的forall s.都是不同的类型。为什么会这样？

{-# LANGUAGE
    GADTs
  , KindSignatures
  , RankNTypes
  , TupleSections
  , ViewPatterns #-}

module Main where

import Data.Reflection

newtype Modulus :: * -> * -> * where
  Modulus :: a -> Modulus s a
  deriving (Eq, Show)

newtype M :: * -> * -> * where
  M :: a -> M s a
  deriving (Eq, Show)

add :: Integral a => Modulus s a -> M s a -> M s a -> M s a
add (Modulus m) (M a) (M b) = M (mod (a + b) m)

mul :: Integral a => Modulus s a -> M s a -> M s a -> M s a
mul (Modulus m) (M a) (M b) = M (mod (a * b) m)

unM :: M s a -> a
unM (M a) = a

withModulus₁ :: a -> (forall s. Modulus s a -> w) -> w
withModulus₁ m k = k (Modulus m)

withModulus₂ :: a -> (Modulus s a -> w) -> w
withModulus₂ m k = k (Modulus m)

test₁ = withModulus₁ 89 (\m ->
          withModulus₁ 7 (\m' ->
            let
              a = M 131
              b = M 127
            in
              unM $ add m' (mul m a a) (mul m b b)))

test₂ = withModulus₂ 89 (\m ->
          withModulus₂ 7 (\m' ->
            let
              a = M 131
              b = M 127
            in
              unM $ add m' (mul m a a) (mul m b b)))

这是错误消息:

Modulus.hs:41:29: error:
    • Couldn't match type ‘s’ with ‘s1’
      ‘s’ is a rigid type variable bound by
        a type expected by the context:
          forall s. Modulus s Integer -> Integer
        at app/Modulus.hs:(35,9)-(41,52)
      ‘s1’ is a rigid type variable bound by
        a type expected by the context:
          forall s1. Modulus s1 Integer -> Integer
        at app/Modulus.hs:(36,11)-(41,51)
      Expected type: M s1 Integer
        Actual type: M s Integer
    • In the second argument of ‘add’, namely ‘(mul m a a)’
      In the second argument of ‘($)’, namely
        ‘add m' (mul m a a) (mul m b b)’
      In the expression: unM $ add m' (mul m a a) (mul m b b)
    • Relevant bindings include
        m' :: Modulus s1 Integer (bound at app/Modulus.hs:36:28)
        m :: Modulus s Integer (bound at app/Modulus.hs:35:27)
   |
41 |               unM $ add m' (mul m a a) (mul m b b)))
   |                             ^^^^^^^^^

最佳答案

简而言之，一个功能

foo :: forall s . T s -> U s

让其调用者选择s类型。实际上，它适用于所有类型s。通过对比，

bar :: (forall s . T s) -> U

要求其调用者提供参数x :: forall s. T s，即适用于所有s类型的多态值。这意味着bar将选择s的类型。

例如，

foo :: forall a. a -> [a]
foo x = [x,x,x]

很明显。代替，

bar :: (forall a. a->a) -> Bool
bar x = x 12 > length (x "hello")

更微妙。在这里，bar首先使用x选择a ~ Int作为x 12，然后再次使用x选择a ~ String作为x "hello"。

另一个例子:

bar2 :: Int -> (forall a. a->a) -> Bool
bar2 n x | n > 10    = x 12 > 5
         | otherwise = length (x "hello") > 7

在此，a根据Int选择为String或n > 10。

你自己的类型

withModulus₁ :: a -> (forall s. Modulus s a -> w) -> w

声明必须允许withModulus₁选择s为其所需的任何类型。当称这个为

withModulus₁ arg (\m -> ...)

m的类型为Modulus s0 a，其中调用者选择a，而s本身选择withModulus₁。要求...必须与withModulus₁可能采取的任何选择兼容。

如果我们嵌套通话怎么办？

withModulus₁ arg (\m1 -> ...
   withModulus₁ arg (\m2 -> ...)
   ...
     )

现在，像以前一样m1 :: Modulus s0 a。进一步的m2 :: Modulus s1 a，其中s1由对withModulus₁的最内部调用选择。

这里的关键点是没有保证s0被选择为与s1相同。每个通话都可能做出不同的选择:例如，参见bar2上面确实如此。

因此，编译器不能假定s0和s1相等。因此，如果我们调用需要它们相等的函数，例如add，则会出现类型错误，因为这将限制两次s调用对withModulus₁的选择自由。

关于haskell - 什么时候永远不是全部，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47106058/

S0

haskell - 什么时候永远不是全部