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

Question

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

myfunction :: a -> a

我无法想出一个示例,其中参数和返回类型是相同的,几乎可以是任何东西(这排除了使用Haskell的类型类的可能性).

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.

编辑:有些人评论说同构的证明不够严谨,所以我会调用Yoneda引理,当翻译成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

因此我们可以使用它来最终将Yoneda同构专门化为:

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

其中说任何类型的函数forall b . b -> b都是同构的().Yoneda引理提供了我的证据缺失的严谨性.

Answer 2

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

Haskell类型和函数的通常语义将类型表示为指向链完整的部分顺序,并且用作连续函数.该类型()由两个元素集{⊥,()}表示,顺序为⊥⊏().在普通集理论中,从这个集合中有2 ^ 2 = 4个函数,但只有三个是连续的:

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

所以在我们的语义模型中,有三种不同的类型函数() -> ().但是哪些可以在Haskell中实现？他们都是!

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

查看这些定义,您可以看到它f1,f2也可以用于定义类型的函数a -> a.由于他们已经做了不同的事情(),他们是不同的.所以我们至少有两种不同的类型函数a -> a.

在上面的语义模型中,还有更多类型的函数a -> a,但这些函数在Haskell中是不可表达的(这与参数化和Wadler的免费定理有关).一个适当的证明,f1并且f2是唯一这样的函数似乎并不容易,因为它取决于Haskell语言不允许的内容(例如,参数的类型没有模式匹配).

Answer 3

除非您愿意使用undefined或bottom(非终止表达式),否则实际上没有其他函数满足该类型.

这是Haskell类型系统的一大优势.可以强制限制可以通过编译器传递到显然正确的函数的可能函数.对于一个极端的例子,请参阅djinn - 它需要一个类型,并生成与该类型匹配的可能函数.即使对于真实,复杂的例子,列表通常也很短.

Answer 4

这里的关键是要了解,我们知道什么有关a,尤其是我们没有办法生成一个新的,或将其转换成不同的东西.因此,我们没有选择返回它(或最低值).一旦我们获得了更多关于a(例如上下文绑定)的信息,我们就可以用它做更多有趣的事情:

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

要么

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

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

多态性限制了自由度,因为你对参数一无所知,在某些情况下,它归结为一个非底部版本.