“forall”如何影响函数签名？

Question

我使用“forall”量词声明了两个函数。其中第一个在签名之前有一个量词，其中包含所有泛型类型参数。第二个使用量词代替每个泛型类型参数的第一个用法。

\n

f :: forall a b c. a -> b -> c -> b -> a\nf a _ _ _ = a\n\ng :: forall a. a ->\n     forall b. b ->\n     forall c. c -> b -> a\ng a _ _ _ = a\n

\n

我期望这两个函数是相同的（区别仅在于描述的风格），但以下两个测试告诉我事实并非如此。

\n

w_f :: (forall a b c. a -> b -> c -> b -> a) -> Bool\nw_f _ = True\n\nw_g :: (forall a. a ->\n        forall b. b ->\n        forall c. c -> b -> a) -> Bool\nw_g _ = True\n

\n

> w_f g\n

\n

 error:  \n    \xe2\x80\xa2 Couldn\'t match type: forall b1. b1 -> forall c1. c1 -> b1 -> a  \n                     with: b -> c -> b -> a   \n      Expected: a -> b -> c -> b -> a  \n      Actual: a -> forall b. b -> forall c. c -> b -> a  \n    \xe2\x80\xa2 In the first argument of \xe2\x80\x98w_f\xe2\x80\x99, namely \xe2\x80\x98g\xe2\x80\x99  \n      In the expression: w_f g  \n      In an equation for \xe2\x80\x98it\xe2\x80\x99: it = w_f g  \n

\n

> w_g f\n

\n

 error:\n    \xe2\x80\xa2 Couldn\'t match type: b0 -> c0 -> b0 -> a\n                     with: forall b. b -> forall c. c -> b -> a\n      Expected: a -> forall b. b -> forall c. c -> b -> a   \n        Actual: a -> b0 -> c0 -> b0 -> a  \n    \xe2\x80\xa2 In the first argument of \xe2\x80\x98w_g\xe2\x80\x99, namely \xe2\x80\x98f\xe2\x80\x99\n      In the expression: w_g f\n      In an equation for \xe2\x80\x98it\xe2\x80\x99: it = w_g f\n

\n

我创建了此案例的图形表示来查看问题所在，但我做不到。

\n

\n

为什么它们不等价？为什么我们不能将所有量词从签名中移出，就像将公倍数从数学表达式中移出一样？有人可以提供类型不匹配的示例吗？

\n

Answer 1

Aforall指定某种类型的函数，就像->那样。

f :: forall (a :: Type). a -> a 
-- "f is a function from types to (functions from values of the type passed as argument to values of that same type)"
f {- @a -} (x :: a) = x
-- "f of a type a and a value (x :: a) is x"
-- syntax for type abstractions is not present in GHC (yet!) for historical reasons
-- but they do appear in the high-level IR (pass -ddump-simpl to GHC)

main = print (f @Integer 5)
-- f must be applied to a type and then a value
-- type abstraction (@a above) and application (@Integer here) can be left unwritten
-- then GHC will infer them

交换->(例如A -> B -> C到B -> A -> C)的实例

• 创建不同的类型，因此交换类型的值对于原始类型来说是不可接受的
• 不会有意义地改变类型；这两种类型是可以相互转换的，只是不是隐式的。

用您自己的话来说，“区别只是描述的风格”。然而，您仍然需要保持该风格的一致性（即参数顺序）。您肯定不会对以下内容感到困惑：

data A = A; data A' = A'; data B = B; data B' = B'; data C = C
f :: A -> B -> A' -> B' -> C
f A B A' B' = C
g :: A -> A' -> B -> B' -> C
g A A' B B' = C

w_f :: (A -> B -> A' -> B' -> C) -> Bool
w_f _ = True

w_g :: (A -> A' -> B -> B' -> C) -> Bool
w_g _ = True

main = do
  print (w_f f)
  -- print (w_f g) -- error...
  print (w_f (\x y -> g y x)) -- ...must shuffle arguments
  -- print (w_g f) -- error...
  print (w_g (\x y -> f y x)) -- ...must shuffle arguments
  print (w_g g)

比较：

-- replacing:
-- A  -> Type (named a)
-- B  -> Type (named b)
-- A' -> a
-- B' -> b
f :: forall (a :: Type) (b :: Type). a -> b -> C
f {- @_ @_ -} _ _ = C
g :: forall (a :: Type). a -> forall (b :: Type). b -> C
g {- @_ -} _ {- @_ -} _ = C
-- notice that f and g even have different equations

w_f :: (forall (a :: Type) (b :: Type). a -> b -> C) -> Bool
w_f _ = True

w_g :: (forall (a :: Type). a -> forall (b :: Type). b -> C) -> Bool
w_g _ = True

main = do
  print (w_f f)
  -- print (w_f g) -- error...
  print (w_f (\x y -> g x y)) -- ...must (invisibly) shuffle arguments
  -- print (w_g f) -- error...
  print (w_g (\x y -> f x y)) -- ...must (invisibly) shuffle arguments
  print (w_g g)

您的代码是上述代码的稍微复杂的版本。在这三种情况下，错误的根本原因都是相同的，而且非常简单。您定义了f和g并具有一定的参数顺序；你最好将它们与这些参数命令一起使用。

PS 评论指出有一个DeepSubsumption扩展可以生成w_f g和w_g f编译，并且从历史上看，这种行为是默认行为（因此您可能已经接受了顺序不重要的信念forall）。这不再是默认值的原因之一是，虽然有一个明显的从forall a b. a -> b -> Cto 的转换forall a. a -> forall b. b -> C，但这种转换会改变定义性。

{-# LANGUAGE DeepSubsumption #-}
convert :: (forall a b. a -> b -> C) -> (forall a. a -> forall b. b -> C)
convert f = f

main = do
  -- print (undefined `seq` ())      -- would die with an exception
  print (convert undefined `seq` ()) -- does NOT die with an exception
  -- so... convert undefined /= undefined...
  -- even though it looks like I defined convert f = f...
  -- gross

forall因此，当您更改函数的顺序时，GHC 已开始强制您明确说明。