Hask甚至是一个类别？

Question

https://wiki.haskell.org/Hask:

考虑:

undef1 = undefined :: a -> b
undef2 = \_ -> undefined

请注意,这些值不相同:

seq undef1 () = undefined
seq undef2 () = ()

这可能是一个问题,因为undef1 . id = undef2.为了使Hask成为一个类别,我们定义了两个函数,f并且g如果f x = g x适用的话,我们定义相同的态射x.因此undef1并且undef2是不同的值,但在Hask中是相同的态射.

它是什么意思,或者我如何检查: undef1它undef2是不同的值,但是相同的态射？

Answer 1

在Haskell中,我们有这样的想法,即每个表达式都可以被评估为特定的"值",并且我们可能对确定两个表达式是否具有"相同"值感兴趣.

非正式地,我们知道可以直接比较某些值(例如,值2和3类型Integer).正如@pigworker所指出的那样,可以通过构造一个"见证"直接可比较值的差异的表达式来比较其他值,如类型sqrt和id类型.Double -> Double

sqrt 4 = 2
id 4 = 4

在这里,我们可以得出结论,sqrt并且id是不同的价值观.如果没有这样的证人,那么价值是相同的.

如果我们看一下的单态专业化undef1和undef2该类型() -> ()计算公式如下:

undef1, undef2 :: () -> ()
undef1 = undefined
undef2 = \_ -> undefined

我们如何判断这些是不同的价值？

好吧,我们需要找到一个见证差异的表达式,上面给出了一个表达式.两个表达式:

> seq undef1 ()
*** Exception: Prelude.undefined
> seq undef2 ()
()
>

根据GHCi,有不同的价值观.我们也可以使用我们对Haskell语义的理解直接显示:

seq undef1 ()
-- use defn of undef1
= seq undefined ()
-- seq semantics:  WHNF of undefined is _|_, so value is _|_
= _|_

seq undef2 ()
-- use defn of undef2
= seq (\_ -> undefined) ()
-- seq semantics: (\_ -> undefined) is already in WHNF and is not _|_,
--   so value is second arg ()
= ()

所以有什么问题？好吧,当把Hask看作一个对象是类型而且态射是(单态)函数的类别时,我们隐含地需要一个对象和态射的同一性/相等性的概念.

对象标识/相等很容易:当且仅当它们是相同类型时,两个对象(单态Haskell类型)是相等的.态射身份/平等更难.因为Hask中的态射是Haskell值(单态函数类型),所以很容易将态射的等式定义为与值的相等,如上所述.

如果我们用这个定义,然后undef1和undef2将不同的态射,因为我们已经证明他们是超然的不同哈斯克尔值.

但是,如果我们比较undef1 . id和undef2,我们会发现,它们具有相同的价值.也就是说,没有任何表达能见证它们之间的差异.证明这有点难,但见下文.

无论如何,我们现在在Hask类别理论中存在矛盾.因为id是Hask中的(多态族)身份态射,我们必须:

undef1 
= undef1 . id                            -- because `id` is identity
= undef2                                 -- same value

所以我们同时undef1 /= undef2因为上面的见证,而是undef1 = undef2通过前面的论证.

避免这种矛盾的唯一方法是放弃在Hask中定义态射的相等性作为底层Haskell值的相等性的想法.

在态射的平等的一个替代定义Hask已经提供是较弱定义两个态射f和g是相等的,当且仅当它们满足f x = g x对于所有的值x(包括_|_).请注意,这里仍然存在歧义.如果f x和g x是自己的Haskell函数等态射,不f x = g x意味着平等态射 f x和g xHaskell的或平等的价值观 f x和g x？我们现在暂时忽略这个问题.

根据这一备选方案的定义,undef1并且undef2 是平等的态射,因为我们可以显示undef1 x = undef2 x所有可能的值x类型()(即()和_|_).也就是说,适用于(),他们给出:

undef1 ()
-- defn of undef1
= undefined ()
-- application of an undefined function
= _|_

undef2 ()
-- defn of undef2
= (\_ -> undefined) ()
-- application of a lambda
= undefined
-- semantics of undefined
= _|_

并适用于_|_他们给:

undef1 _|_
-- defn of undef1
= undefined _|_
-- application of an undefined function
= _|_

undef2 _|_
-- defn of undef2
= (\_ -> undefined) _|_
-- application of a lambda
= undefined
-- semantics of undefined
= _|_

类似地,undef1 . id并且undef2可以通过这个定义显示出与Hask中的态射相等(事实上​​,它们等于Haskell值,这意味着它们根据Hask态射等式的较弱定义而相等),因此没有矛盾.

但是,如果你按照@nm提供的链接,你可以看到在形式化Haskell值相等的含义方面还有更多的工作要做,并且在我们真正感到舒服之前精确地给出Hask态射相等的适当定义.相信有是无矛盾,Hask类别.

undef1 . id = undef2作为Haskell值的证明

由于上述原因,这个证据必然是非正式的,但这是一个想法.

如果我们试图见证功能之间的差异f和g,一个见证表达式可以的唯一途径使用这些值是通过将他们的值x或者通过评估其使用到WHNF seq.如果f并且g已知它们与Hask态射相等,那么我们已经拥有f x = g x了所有x,所以没有表达可以看到基于应用程序的差异.唯一要检查的是,当它们被评估为WHNF时,它们要么被定义(在这种情况下,通过先前的假设,它们将在应用时产生相同的值),或者它们都是未定义的.

所以,对于undef1 . id和undef2,我们只需要确保它们在被评估为WHNF时既可以定义,也可以两者都未定义.事实上,很容易看出它们都定义了WHNF:

undef1 . id 
-- defn of composition
= \x -> undef1 (id x)
-- this is a lambda, so it is in WHNF and is defined

undef2
-- defn of undef2
= \_ -> undefined
-- this is a lambda, so it is in WHNF and is defined

我们已经undef1 x = undef2 x为所有人建立了以上x.从技术上讲,我们应该表明:

(undef1 . id) x
-- defn of composition
= (\x -> undef1 (id x)) x
-- lambda application
= undef1 (id x)
-- defn of id
= undef1 x

与所有人的Haskell值相等x,这(undef1 . id) x = undef2 x为所有人建立了这一点x.再加上两者都定义了上面的WHNF这一事实,这足以证明undef1 . id = undef2Haskell值相等.