倒装数据类型

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的唯一参数将具有​​构造函数。因此，例如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和​​，以及三个显式参数，它们是产生一个类型的二元函数，然后是它的两个参数以相反的顺序。这个函数的参数是无约束的类型（如果他们喜欢，老人可以说“kind”），但它肯定会返回一个类型（严格意义上的“*中的东西”，而不是毫无用处地模糊地指出“任何旧的垃圾权::“），因为它肯定用作MkFlip声明中的一种类型。

的数据构造，MkFlip，需要隐含参数（的Flip完全参数）和一个明确的说法，f b a是一些数据。

发生什么事情是Hindley-Milner类型推理的一个级别。约束收集（例如，f b a必须居住*因为构造函数的参数必须居住f b a），但除此之外，最一般的类型被传递：a和b可以是任何东西，所以它们的类型可以概括为​​和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。 A Functor实例因此是合理的并且实际上可交付的，其功能作用于打包的a元素，对应于参数Flip K b，其变为第一自变量K，因此存储的元素的类型。

基于统一的类型推断仍然存在并且（相当）良好，正确的为::。