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,但是在看到这个之后,即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)],但这不是我想要的).

我也发现了这个问题,但不能真正使这是否是同样的问题或没有,因为我想应用功能不是id,但fst还是snd,实际上返回不同类型的功能(a -> b).

Answer 1

问题是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.

Answer 2

签名中的问题是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,其中种类实际上只是类型的类型,您可以定义类型级函数以及值级函数.但这是有代价的:所有功能都需要全部功能!这并不是一件坏事,但这意味着这些语言通常不是真正的图灵完备(这需要无限循环/递归的可能性;但这?与完整的结果评估有关).

¹事情已经改变,有点用的来临那种多态性等.

²这与例如C++不同,后者允许 - 尽管语法非常糟糕 - 通过模板进行鸭式类型级函数.这可能是一个非常好的功能,但其中一个后果是,当您尝试使用实例化模板时,您经常会得到完全不可读的错误消息(与真实问题的关系甚至比GHC最糟糕的"可能修复"暗示......)更少隐式域之外的类型参数.