Flip数据类型的Functor类型变量

Question

我有以下类型定义:

newtype Flip f a b = 
  Flip (f b a) deriving (Eq, Show)

Flip数据构造函数是否有一个或三个参数？

Consinder实施后:

data K a b = K a

newtype Flip f a b = 
  Flip (f b a) deriving (Eq, Show)

instance Functor (Flip K a) where
  fmap f (Flip (K b)) = Flip (K (f b))  

是什么类型的(Flip K a)？

Answer 1

该Flip数据构造函数有一个参数.那个论点有类型f b a.

因此,这意味着它f本身是一个带有类型的高阶类型参数f :: * -> * -> *.更严格的newtype声明是:

newtype Flip (f :: * -> * -> *) a b = Flip (f b a)

因此,您可以实例化一个Flip Either Int Bool,因为Either是一个需要两个额外类型参数的类型,然后构造一个Flip (Right 1) :: Flip Either Int Bool.

是什么类型的(Flip K a)？

Flip K a不是完全应用的类型.在伪代码中,它具有类型b -> Flip K a b.一旦b解决了(Functor使用更高阶类型),我们知道唯一的参数Flip将有一个K b构造函数.所以例如Flip (K 1)是一种Flip K a Int类型.

Answer 2

未来就是现在,当你(使用ghc 8和)打开一两个旗帜时

Prelude> :set -XPolyKinds -XFlexibleInstances

让我们宣布

Prelude> newtype Flip f a b = MkFlip (f b a)

然后询问

Prelude> :kind Flip
Flip :: (k1 -> k -> *) -> k -> k1 -> *

Prelude> :type MkFlip
MkFlip
  :: forall k k1 (b :: k) (f :: k -> k1 -> *) (a :: k1).
     f b a -> Flip f a b

该类型的构造Flip有两个隐式参数,感k和k1,以及三个明确的参数,是在相反的顺序制造的类型,则它的两个自变量的二元函数.这个函数的参数是无约束的类型(老人们可以说"善意",如果他们喜欢),但它肯定会返回一种类型(严格意义上的"东西*",而不是无用的模糊的"任何旧垃圾" ::")的权利,因为它肯定被用作声明中的一种类型MkFlip.

该数据构造,MkFlip,采用5个隐参数(恰好参数Flip)和一个明确的说法,是在一些数据f b a.

发生了什么是Hindley-Milner类型推断一级.收集约束(例如,f b a必须居住,*因为构造函数参数必须居住f b a)但是否则传递最普遍的类型:a并且b可以是任何东西,因此它们的类型被概括为k1和k.

让我们用常量类型构造函数玩同一个游戏:

Prelude> newtype K a b = MkK a

Prelude> :kind K
K :: * -> k -> *

Prelude> :type MkK
MkK :: forall k (b :: k) a. a -> K a b

我们看到了这一点,a :: *但b可以是任何旧的垃圾(就此而言k :: *,就像现在一样* :: *).显然,a实际上是用作事物的类型,但b根本不使用,因此不受约束.

然后我们可以宣布

Prelude> instance Functor (Flip K b) where fmap f (MkFlip (MkK a)) = MkFlip (MkK (f a))

并问

Prelude> :info Flip
...
instance [safe] forall k (b :: k). Functor (Flip K b)

这告诉我们,未使用的b仍然可以是任何旧的垃圾.因为我们有

K    ::   * -> k -> *
Flip :: (k1 -> k -> *) -> k -> k1 -> *

我们可以统一k1 = *并得到

Flip K :: k -> * -> *

所以

Flip K b :: * -> *

对于任何旧的b.Functor因此,一个实例是合理的,并且实际上是可交付的,其中函数作用于打包a元素,对应于其参数Flip K b成为第一个参数K,因此存储元素的类型.

基于统一的类型推断是有效的,并且(相当)很好,正确::.