23

我刚刚开始玩一点Haskell......我想写一个相同类型的身份函数。显然，不等同于它。那会是这样的，

myfunction :: a -> a

我想不出一个参数和返回类型相同并且几乎可以是任何东西的例子（这排除了使用 Haskell 的 Typeclasses 的可能性）。

4

5 回答 5

28

undefined如果不使用另一位提到的评论者，这是不可能的。让我们通过反例来证明它。假设有这样一个函数：

f :: a -> a

当您说这与 不同时id，这意味着您无法定义：

f x = x

但是，考虑atype的情况()：

f () = ...

唯一可能f返回的结果是()，但这将是与 相同的实现id，因此是矛盾的。

更复杂和严格的答案是表明类型a -> a必须同构于(). 当我们说两种类型a并且b是同构的时，这意味着我们可以定义两个函数：

fw :: a -> b
bw :: b -> a

...这样：

fw . bw = id
bw . fw = id

当第一种类型是a -> a，第二种类型是时，我们可以很容易地做到这一点()：

fw :: (forall a . a -> a) -> ()
fw f = f ()

bw :: () -> (forall a . a -> a)
bw () x = x

那么我们可以证明：

fw . bw
= \() -> fw (bw ())
= \() -> fw (\x -> x)
= \() -> (\x -> x) ()
= \() -> ()
= id

bw . fw
= \f -> bw (fw f)
-- For this to type-check, the type of (fw f) must be ()
-- Therefore, f must be `id`
= \f -> id
= \f -> f
= id

当您证明两种类型是同构的时，您知道的一件事是，如果一种类型包含有限数量的元素，那么另一种也必须如此。由于该类型()只包含一个值：

data () = ()

这意味着该类型(forall a . a -> a)也必须只包含一个值，而这恰好是id.

编辑：有些人评论说同构的证明不够严格，所以我将调用米田引理，当翻译成 Haskell 时，它对任何函子说f：

(forall b . (a -> b) -> f b) ~ f a

Where~意味着它(forall b . (a -> b) -> f b)与f a. 如果您选择Identity函子，这将简化为：

(forall b . (a -> b) -> b) ~ a

...如果您选择a = ()，这将进一步简化为：

(forall b . (() -> b) -> b) ~ ()

你可以很容易地证明它() -> b同构于b：

fw :: (() -> b) -> b
fw f = f ()

bw :: b -> (() -> b)
bw b = \() -> b

fw . bw
= \b -> fw (bw b)
= \b -> fw (\() -> b)
= \b -> (\() -> b) ()
= \b -> b
= id

bw . fw
= \f -> bw (fw f)
= \f -> bw (f ())
= \f -> \() -> f ()
= \f -> f
= id

所以我们可以使用它来最终将米田同构特化为：

(forall b . b -> b) ~ ()

这表示任何类型forall b . b -> b的函数都与(). 米田引理提供了我的证明缺失的严谨性。

于 2012-09-01T19:53:05.553 回答
12

让我制定一个详细说明 dbaupp 评论的答案。任何类型的函数a -> a也会产生一个类型的函数() -> ()，所以我先看看这个子问题。

Haskell 类型和函数的通常语义将类型表示为指向链完整的偏序，并将函数表示为连续函数。类型()由两个元素集{⊥,()} 表示，顺序为⊥⊏()。在普通集合论中，从这个集合到自身有 2^2=4 个函数，但其​​中只有三个是连续的：

  • f1: ⊥ ↦ ⊥, () ↦ ⊥,
  • f2: ⊥ ↦ ⊥, () ↦ (), 和
  • f3: ⊥ ↦ (), () ↦ ()。

所以在我们的语义模型中， type 有三种不同的功能() -> ()。但是其中哪些可以在 Haskell 中实现呢？他们都是！

  • f1 _ = undefined（或f1 x = f1 x）
  • f2 x = x（或f2 = id）
  • f3 _ = ()（或f3 = const ()）

查看这些定义，您可以看到f1并且f2也可以用于定义 type 的函数a -> a。由于他们已经在做不同的事情()，所以他们是不同的。所以我们至少有两个不同的 type 函数a -> a。

在上面的语义模型中，还有很多 type 的函数a -> a，但是这些函数在 Haskell 中是无法表达的（这与参数化和 Wadler 的Free 定理有关）。正确证明f1并且f2是唯一这样的函数似乎并不容易，因为它取决于 Haskell 语言不允许的内容（例如，参数类型没有模式匹配）。

于 2012-09-01T21:05:44.207 回答
9

除非您愿意使用 undefined 或 bottom（非终止表达式），否则实际上没有其他函数可以满足该类型。

这是 Haskell 类型系统的一大优势。可以强烈限制可以通过编译器传递给显然正确的函数。举一个极端的例子，见djinn——它接受一个类型，并生成与该类型匹配的可能函数。即使是真实的、复杂的例子，这个列表通常也很短。

于 2012-09-01T19:52:52.503 回答
8

这里的关键是要了解我们对 . 什么都不知道a，尤其是我们无法生成一个新的或将其转换为不同的东西。因此，我们别无选择返回它（或底部值）。一旦我们有了更多关于a（例如上下文绑定）的信息，我们就可以用它做更多有趣的事情：

f :: Monoid a => a -> a
f _ = mempty

或者

f :: Monoid a => a -> a
f x = x `mappend` x `mappend` x

或者，如果您有类似 in 的选择f :: (a, a) -> a，您有两种可能的实现（再次忽略底部值），但f :: (a, b) -> a您又回到了一个实现，这与 for 相同fst：虽然f使用一对相同的类型调用是有效的，例如f ("x", "y")，您可以确定它的f行为类似于fst，因为在实现中f您无法测试两种参数类型是否相同。同样，只有一个非底层版本的f :: (a -> b) -> a -> b.

多态性限制了自由度，因为你对你的论点一无所知，在某些情况下，它归结为一个非底层版本。

于 2012-09-02T13:08:09.610 回答
2

正如其他人所提到的，不存在这样的其他总功能。（如果我们不将自己限制在总功能上，那么我们可以通过 . 来居住任何类型undefined。）

我将尝试基于 λ 演算给出一个理论解释：

为简单起见，让我们将自己限制在 λ 项（我们可以将任何 Haskell 表达式翻译成它）。对于 λ 项，如果不是应用程序（也可以为零），M我们称它为头。请注意，如果是正常形式，则不能是 λ-抽象，除非.AM ≡ A N1 ... NkAkMAk = 0

所以让M :: a -> a成为范式的 λ-项。由于我们在上下文中没有变量，M因此不能是变量，也不能是应用程序。如果是，它的头部就必须是一个变量。所以M一定是λ-抽象，一定是M ≡ λ(x:a).N。

现在N必须是类型的a，正式的{x:a}⊢N:a。如果N是 λ-抽象，则其类型为σ -> τ，这是不可能的。如果N是一个函数应用程序，那么它的 head 必须是一个变量，而我们在上下文中唯一的一个是x. 但是因为x:a，我们不能应用于x任何东西，x P所以不能对任何 P 进行录音。所以唯一的可能性是N ≡ x。所以，M一定是λ(x:a).x。

（如果可能，请更正我的英语。特别是，我不确定如何使用虚拟语气权利）。

于 2012-09-02T16:54:09.523 回答