14

参数化多态函数

考虑以下函数：

f :: a -> Int
f x = (1 :: Int)

我们可以说fis的类型a -> Int，f因此它是“多态”类型。

以下哪项是最准确的思考方式f？

  1. 实际上有一个 ftype a -> Int。但是，它可以用作 、f :: Int -> Int等f :: Double -> Int。

  2. 从字面上看，类型f是 NOT a -> Int。实际上，这只是一种简写方式，即存在一个类型为具体的函数族f（即，有 an f :: Int -> Int、anf :: Double -> Double等；此外，这些函数中的每一个都彼此不同）。

高等类型

同样，我们可以考虑以下类型声明：

data Maybe a = Just a | Nothing

并问两种观点哪个更正确：

  1. 没有单一类型Maybe；实际上，只有一个具体类型的族（Maybe Int、Maybe String等），仅此而已。

  2. 实际上只有一种类型Maybe。这种类型是更高种类的类型。当我们说它是“类型”时，我们的意思是字面意思（不是 (1) 的简写）。碰巧我们也可以编写Maybe Int,Maybe Double等来生成不同的类型（它们恰好是具体的）。但是，归根结底（即）：Maybe、Maybe Int和Maybe String表示三种不同的类型，其中两种是具体的，另一种是高级的。

问题摘要

在 Haskell 中，“高级类型”真的是类型吗？或者只是具体类型是“真正的类型”，当我们谈到“高级类型”时，我们只是表示一个具体类型的族。此外，参数化多态函数是表示单一类型的函数，还是仅表示具体类型的集合函数（仅此而已）？

4

2 回答 2

13

目前尚不完全清楚您要问什么，以及两种情况下 1 和 2 之间的实际区别是什么，但从基础数学的角度来看：

参数化多态函数

f实际上有类型f :: forall a.a->int

它是 Haskell 所基于的类型化 lambda 演算中函数的完全合法类型。它可以是这样的：

f = λa:Type.λx:a.(body for f)

你如何从中得到Double->Int？您将其应用于Double类型：

f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double)

Haskell 在后台执行这两种操作（类型抽象和类型应用程序），尽管可以使用GHC 扩展显式声明forall类型签名中的部分，并显式创建具有类型签名的实例：XExplicitForAllDouble->Intf

f_double :: Double -> Int
f_double = f

高等类型

考虑一个简单的类型：

data Example = IntVal Int | NoVal

（是的，它是Maybe Int）。

Maybe是一个类型构造函数，就像IntVal是一个数据构造函数。它完全一样，只是“高一级”，在适用于 的意义上Maybe，Type很像IntVal适用于Int。

在 lambda 演算中，Maybe具有类型：

Maybe : Type->Type

Haskell 不允许您从类型构造函数中获取类型，但允许您获取一种（这只是type 类型的花哨名称）：

:k Maybe
Maybe :: * -> *

所以不，Maybeis not a type：你不能有一个 type 的对象Maybe。Maybe是（几乎）从类型到类型IntVal的函数，就像是从值到值的函数。

我们将应用Maybe到的结果String称为 as Maybe String，就像我们将应用IntVal到的结果4称为 as 一样IntVal 4。

于 2016-05-22T01:33:48.043 回答
7

首先一个问题：语句“所有列表都有长度”是单个语句还是一系列语句“list1 有长度”，“list2 有长度”，...？

如果你给出fwith 显式的类型forall，你会得到f :: forall a. a -> Int. 首先，这不是“高级”。我们可以在 GHCI 中执行以下操作：

λ> :set -XRankNTypes
λ> :k (forall a. a -> Int)
(forall a. a -> Int) :: *

所以f有一种*。

现在，在 Haskell 中，我们可以使用~类型相等。我们可以设置以下内容来检查 GHCI 中的内容：

λ> :set -XImpredicativeTypes
λ> :set -XTypeFamilies
λ> :t undefined :: ((~) Int Int) => a
undefined :: ((~) Int Int) => a :: a

这表明 GHC 为这个例子找出了类型相等。类型不等式将给出以下错误：

λ> undefined :: ((~) (Int -> Int) (Int)) => a

<interactive>:22:1:
    Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
    In the expression: undefined :: ((~) (Int -> Int) (Int)) => a
    In an equation for ‘it’:
    it = undefined :: ((~) (Int -> Int) (Int)) => a

现在直接使用这种方法会阻止我们比较 的类型f，但我发现了一个可以满足我们目的的轻微变体：

λ> :t undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a
undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a :: Int

换句话说，如果f类型等价于g :: Int -> Int，则a必须是 Int。这类似于x = y，y = 0所以x = 0。x = 0在我们指定之前我们没有y = 0，直到那时我们才有x = y。

Maybe是不同的，因为它有以下种类：

λ> :k Maybe
Maybe :: * -> *

因为我们正在使用DataKinds，所以我们有:k (~) :: k -> k -> GHC.Prim.Constraint，所以我们可以执行以下操作：

λ> :t undefined :: (~) Maybe Maybe => Int
undefined :: (~) Maybe Maybe => Int :: Int

λ> :k Either ()
Either () :: * -> *

λ> :t undefined :: (~) Maybe (Either ()) => Int
Couldn't match expected type ‘Either ()’ with actual type ‘Maybe’

总而言之，f :: forall a. a -> Int就像“如果你给我任何东西，我会给你一个 Int”这样的陈述一样有意义。你能把这句话翻译成一堆“如果你给我一只狗……”，“如果你给我一分钱……”吗？是的，但它削弱了声明。最后，准确地确定“相同”的含义，然后您就会得到答案。

于 2016-05-22T00:58:03.810 回答