Haskell:a -> a 类型函数的示例，除了标识

Question

我刚刚开始玩一点Haskell......我想写一个相同类型的身份函数。显然，不等同于它。那会是这样的，
myfunction :: a -> a
我想不出一个参数和返回类型相同并且几乎可以是任何东西的例子(这排除了使用 Haskell 的 Typeclasses 的可能性)。

Answer 1

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

f :: a -> a

当您说这与 id 不一样，这意味着您不能定义:

f x = x

但是，考虑 a 的情况。是类型 () :

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

在哪里 ~表示 (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与 () 同构.米田引理提供了我的证明缺失的严谨性。