功能组成和所有类型 [英] Function composition and forall'ed types

问题描述

假设我们有一些这样的代码，这种类型的代码很好：

$ b

  { - ＃LANGUAGE RankNTypes＃ - } 
 
 data Foo a 
 
 type a a = forall m。 Monad m => Foo a  - > m（）
 type PA a = forall m。 Monad m => Foo a  - > m（）
键入PPFA a = forall m。 Monad m => Foo a  - > m（）
 
 _pfa :: PPFA a  - > PA a 
 _pfa = _pfa 
 
 _pa :: PA a  - > A a 
 _pa = _pa 
 
 _pp :: PPFA a  - > a a 
 _pp x = _pa $ _pfa x 
 
 main :: IO（）
 main = putStrLnyay
  

我们注意到 _pp x = _pa $ _pfa x 太冗长了，我们试着用 _pp = _pa。 _pfa 。突然间，代码不再检查，失败的错误消息类似于

 •无法匹配类型'Foo a0  - > ; m0（）'与'PA a'
预期类型：（Foo a0  - > m0（）） - > Foo a  - > m（）
实际类型：PA a  - > A a 
  

我想这是由于 m 定义类型别名为 forall 'd—的确，用一些确切类型替换 m 可以解决问题。但问题是：为什么 forall 在这种情况下会破坏事情？

试图找出原因的奖励点用通常的 _pfa = undefined _pfa 和 _pa 的虚拟递归定义c>导致GHC抱怨统一变量和意外多态：

 •无法实例化统一变量'a0'
涉及虚构的类型：PPFA a  - > Foo a  - > m（）
 GHC不支持imprandicative多态性
•在表达式中：undefined 
在'_pfa'的等式中：_pfa = undefined 
  
 
解决方案
 
  _pa :: PA a  - > a a 
  
编译器展开类型同义词，然后向上移动量词和约束，如下所示： / p> 
 
 
  _pa 
 :: forall a。 
（m1。Monad m1 => Foo a  - > m1（））
  - > （m2）Monad m2 => Foo a  - > m2（））
 
 _pa 
 :: forall m2 a。 （Monad m2）
 => （m1。Monad m1 => Foo a  - > m1（））
  - > Foo a  - > m2（）
  
所以 _pa 有一个等级-2多态类型，因为它有一个嵌套在函数箭头左侧的文件。同样适用于 _pfa 。他们期望多态函数作为参数。
 
 
 
要回答实际问题，我会先给你看一些奇怪的东西。这些都是类型检查： 
 
 
  _pp :: PPFA a  - > A a 
 _pp x = _pa $ _pfa x 
 
 _pp :: PPFA a  - > a a 
 _pp x = _pa（_pfa x）
  
然而，这并不是：  
 
 
  apply ::（a  - > b） - > a  - > b 
应用f x = f x 
 
 _pp :: PPFA a  - > A a 
 _pp x = apply _pa（_pfa x）
  
不直观，对吗？这是因为应用程序运算符（$）在编译器中是特殊的，允许使用多态类型实例化它的类型变量，以支持 runST $ do {...} 而不是 runST（do {...}）。
 
 
 
然而，构成（。）并不是特别的。所以当你在 _pa 和 _pfa 上调用（。） ，它首先实例化它们的类型。因此，您最终试图传递类型的非多态结果 _pfa （Foo a0  - > m0（）） - > Foo a  - >在函数 _pa 中提到了m（），但它需要一个类型为 P a的多态参数 
  undefined :: a 不会发生统一错误。 typecheck，因为它试图用多态类型实例化 a ，这是一个impandicative多态性的实例。这暗示了你应该做什么 - 隐藏不可预知性的标准方式是使用 newtype 包装：
  newtype A a = A {unA :: forall m。 Monad m => Foo a  - > m（）} 
 newtype PA a = PA {unPA :: forall m。 Monad m => Foo a  - > m（）} 
 newtype PPFA a = PPFA {unPPFA :: forall m。 Monad m => Foo a  - > m（）} 
  
现在这个定义编译时没有错误：
 
 
  _pp :: PPFA a  - > a 
 _pp = _pa。使用您需要明确包装和解包的代价来告诉GHC何时抽象和实例化：？？？？？？？？？？？？？？？？？？？？  
 
 
  _pa :: PA a  - > a a 
 _pa x = A（unPA x）
  
 
Let's say we have some code like this, which typechecks just fine:
{-# LANGUAGE RankNTypes #-}

data Foo a

type A a = forall m. Monad m => Foo a -> m ()
type PA a = forall m. Monad m => Foo a -> m ()
type PPFA a = forall m. Monad m => Foo a -> m ()

_pfa :: PPFA a -> PA a
_pfa = _pfa

_pa :: PA a -> A a
_pa = _pa

_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

main :: IO ()
main = putStrLn "yay"
We note that _pp x = _pa $ _pfa x is too verbose, and we try to replace it with _pp = _pa . _pfa. Suddenly the code doesn't typecheck anymore, failing with error messages similar to
• Couldn't match type ‘Foo a0 -> m0 ()’ with ‘PA a’
  Expected type: (Foo a0 -> m0 ()) -> Foo a -> m ()
    Actual type: PA a -> A a
I guess this is due to m in the definition of type aliases being forall'd — indeed, replacing m with some exact type fixes the issue. But the question is: why does forall break things in this case?

Bonus points for trying to figure out why replacing dummy recursive definitions of _pfa and _pa with usual _pfa = undefined results in GHC complaining about unification variables and impredicative polymorphism:
• Cannot instantiate unification variable ‘a0’
  with a type involving foralls: PPFA a -> Foo a -> m ()
    GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
  In an equation for ‘_pfa’: _pfa = undefined

解决方案
Just to be clear, when you write:
_pa :: PA a -> A a
The compiler expands the type synonyms and then moves the quantifiers and constraints upward, like so:
_pa
  :: forall a.
     (forall m1. Monad m1 => Foo a -> m1 ())
  -> (forall m2. Monad m2 => Foo a -> m2 ())

_pa
  :: forall m2 a. (Monad m2)
  => (forall m1. Monad m1 => Foo a -> m1 ())
  -> Foo a -> m2 ()
So _pa has a rank-2 polymorphic type, because it has a forall nested to the left of a function arrow. Same goes for _pfa. They expect polymorphic functions as arguments.

To answer the actual question, I’ll first show you something strange. These both typecheck:
_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

_pp :: PPFA a -> A a
_pp x = _pa (_pfa x)
This, however, does not:
apply :: (a -> b) -> a -> b
apply f x = f x

_pp :: PPFA a -> A a
_pp x = apply _pa (_pfa x)
Unintuitive, right? This is because the application operator ($) is special-cased in the compiler to allow instantiating its type variables with polymorphic types, in order to support runST $ do { … } rather than runST (do { … }).

Composition (.), however, is not special-cased. So when you call (.) on _pa and _pfa, it instantiates their types first. Thus you end up trying to pass the non-polymorphic result of _pfa, of the type (Foo a0 -> m0 ()) -> Foo a -> m () mentioned in your error message, to the function _pa, but it expects a polymorphic argument of type P a, so you get a unification error.

undefined :: a doesn’t typecheck because it tries to instantiate a with a polymorphic type, an instance of impredicative polymorphism. That’s a hint as to what you should do—the standard way of hiding impredicativity is with a newtype wrapper:
newtype A a = A { unA :: forall m. Monad m => Foo a -> m () }
newtype PA a = PA { unPA :: forall m. Monad m => Foo a -> m () }
newtype PPFA a = PPFA { unPPFA :: forall m. Monad m => Foo a -> m () }
Now this definition compiles without error:
_pp :: PPFA a -> A a
_pp = _pa . _pfa
With the cost that you need to explicitly wrap and unwrap to tell GHC when to abstract and instantiate:
_pa :: PA a -> A a
_pa x = A (unPA x)


                        
这篇关于功能组成和所有类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！