RankNTypes：应用相同的功能，不同类型的

Question

的对我试图定义此功能重新组合对三个列表：

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 


main = do 
    let x = mapAndZip3 (fst) [(1,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5,"cake"),(4,"pudding")] 
    print x -- was expecting [(1,"chips",5), (2,"rice",4)] 

起初我并没有包括RankNTypes或forall，但随后在录入this后，即liftTup的定义，我认为它应该够了。

但显然，它不是，因为我还得到一个错误：

mapAndZip3.hs:8:25: 
Couldn't match type `x' with `(f0 x, b0)' 
    `x' is a rigid type variable bound by 
     a type expected by the context: x -> f0 x at mapAndZip3.hs:8:13 
Expected type: x -> f0 x 
    Actual type: (f0 x, b0) -> f0 x 
In the first argument of `mapAndZip3', namely `(fst)' 

我明明有forall关键字的了解有限，但是从我的理解是应该在这种情况下，允许为f接受任何类型。我不明白的是：一旦在给定的背景下使用过一次，定义是否会在剩下的环境中“固定”？因为如果我用Ints替换“芯片”和“米”，编译器仍然抱怨，所以我想我错了（当然，如果我删除了类型注释mapAndZip3在后一种情况下，因为签名被简化为mapAndZip3 :: (a -> t) -> [a] -> [a] -> [a] -> [(t, t, t)]，所有东西都可以使用，但这不是我想要的）。

我也发现了这个question，却无法真正使这是否是同样的问题或没有，因为我尝试应用功能不id，但fst或snd，实际上返回不同类型(a -> b)功能。

Answer 1

签名中的问题是f。让我们扩展了一点：

mapAndZip3 :: forall (a :: *) (b :: *) (c :: *) (f :: *->*) 
      => (forall x. x -> f x) -> [a] -> [b] -> [c] 
           -> [(f a, f b, f c)] 

f这里应该是“任何类型级功能”，在您的实例这将是type f (a,b) = a。但是Haskell不允许你抽象类型级函数，只能通过类型的构造函数，比如Maybe或IO。所以mapAndZip3 Just实际上是可能的，但fst不会构造，但解构元组类型。

类型函数甚至不存在于Haskell98中，它们只能在TypeFamilies之后才可能存在。问题基本上是Haskell的同类语言是无类型的，但是类型级别函数需要是总函数。但是，您无法真正定义所有类型为的定义为的任何非平凡函数（即非id或类型构造函数）。类型级别fst当然不是总数，它只适用于元组类型。

因此，为了使用这些功能，您需要明确地以其他方式指定其上下文。随着TypeFamilies它可以工作是这样的：

class TypeFunctionDomain d where 
    type TypeFunction d :: * 

instance TypeFunctionDomain (a,b) where 
    type TypeFunction (a,b) = a 

mapAndZip3 :: (forall x. TypeFunctionDomain x => x -> TypeFunction x) 
      -> [a] -> [b] -> [c] 
        -> [(TypeFunction a, TypeFunction b, TypeFunction c)] 

然而，这是不是真的是你想要什么：它是不可能在同一范围内也TypeFunctionDomain实例造成相应于snd定义，这意味着mapAndZip3有效止跌根本不是多态的，但只能用于单一功能。

这些问题只能在依赖性类型语言中妥善解决如Agda，在那里种真的只是种类型，您可以定义类型层次的功能一样好值级别的功能。但是，这是作为一个价格：所有功能需要是总功能！这并不是一件坏事，但它意味着这些语言通常并不是真正的图灵完备的（这将需要无限循环/递归的可能性;然而⟂关于完整的结果评估）。

---

事情已经改变，有点与kind polymorphism etc.来临。

这不同于例如， C++，它允许 - 尽管语法非常糟糕 - duck-typed类型级别的函数，通过模板。这可能是一个相当不错的功能，但其中一个后果就是您经常会得到完全无法读取的错误消息（与GHC最糟糕的“可能修复”提示相比，与真实问题的关系更小）隐式域之外的类型参数。

Answer 2

的问题是，fst不具有所需的类型

(forall x. x -> f x) 

类型的fst是

fst :: (a, b) -> a 

和a是形式f (a,b)的不。 f有一个变量，必须用类型构造函数实例化，如[],Maybe，Either Bool。 f不能代表像Λ (a,b) -> a这样的“类型函数”，它必须是一个类型构造函数。

它的工作原理，如果我们提供它所需类型的函数（抱歉，愚蠢的例子）：

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 

fst0 x = (True,x) 

main = do 
    let x = mapAndZip3 (fst0) [(1 :: Int,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5 :: Int,"cake"),(4,"pudding")] 
    print x 

因为在这里fst0有型a -> ((,) Bool) a，它的形式x -> f x。