Hask甚至是一个类别吗? [英] Is Hask even a category?

问题描述

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

考虑:

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

请注意，这些值不相同:

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

这可能是个问题，因为undef1 . id = undef2.为了使 Hask 成为一个类别，我们为所有x将f和g定义为相同的词素(如果f x = g x).因此，undef1和undef2是不同的值，但是在 Hask 中，相同的同态.

这是什么意思或如何检查: undef1和undef2是不同的值，但是同构吗?

解决方案

在Haskell中，我们的想法是，每个表达式都可以求值为特定的值"，我们可能有兴趣确定两个表达式是否具有相同"的值.

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

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将是不同的形态，因为我们已经证明它们在上面是不同的Haskell值.

但是，如果我们比较undef1 . id和undef2，我们会发现它们具有 same 值.就是说，没有表达可以证明它们之间存在差异.证明这有点困难，但请参阅下文.

无论如何，我们现在的 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 x的相等性还是等价性? Haskell 值 f x和g x?现在让我们忽略这个问题.

在此替代定义下，undef1和undef2 等同于射态，因为我们可以显示类型为()的所有可能值x的undef1 x = undef2 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或使用seq将其评估为WHNF.如果已知f和g等同于 Hask 语素，则对于所有x，我们都已经具有f x = g 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

我们已经为所有x建立了高于undef1 x = undef2 x的位置.从技术上讲，我们应该证明:

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

与所有x的Haskell值相等，从而为所有x确立(undef1 . id) x = undef2 x.两者都在上面定义了WHNF，这足以表明undef1 . id = undef2与Haskell值相等.

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

Consider:

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

Note that these are not the same value:

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

This might be a problem, because undef1 . id = undef2. In order to make Hask a category, we define two functions f and g as the same morphism if f x = g x for all x. Thus undef1 and undef2 are different values, but the same morphism in Hask.

What does it mean or how can I check, that: undef1 and undef2 are different values, but the same morphism?

解决方案

In Haskell, we have this idea that every expression can be evaluated to a particular "value", and we might be interested in determining if two expressions have the "same" value.

Informally, we know that some values (e.g., value 2 and 3 of type Integer) can be compared directly. Other values, like sqrt and id of type Double -> Double can be compared, as @pigworker notes, by constructing an expression that "witnesses" a difference in directly comparable values:

sqrt 4 = 2
id 4 = 4

Here, we can conclude that sqrt and id are different values. If there is no such witness, then the values are the same.

If we look at the monomorphic specializations of undef1 and undef2 to the type () -> () given by:

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

how can we tell if these are different values?

Well, we need to find an expression that witnesses a difference, and one is given above. The two expressions:

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

have different values, according to GHCi. We could also show this directly, using our understanding of Haskell semantics:

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 ()
= ()

So, what's the problem? Well, when considering Hask as a category where the objects are types and the morphisms are (monomorphic) functions, we implicitly need a concept of identity/equality for objects and morphisms.

Object identity/equality is easy: two objects (monomorphic Haskell types) are equal if and only if they are the same type. Morphism identity/equality is harder. Because morphisms in Hask are Haskell values (of monomorphic function types), it would be tempting to define equality of morphisms to be the same as equality of values, as above.

If we used this definition, then undef1 and undef2 would be different morphisms, because we have proved they are different Haskell values above.

However, if we compared undef1 . id and undef2, we would discover that they have the same value. That is, there is no expression that witnesses a difference between them. Proving this is a little tough, but see below.

Anyway, we now have a contradiction in our Hask category theory. Because id is the (polymorphic family of) identity morphisms in Hask, we must have:

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

so we simultaneously have undef1 /= undef2 because of the witness above, but undef1 = undef2 by the previous argument.

The only way to avoid this contradiction is to give up the idea of defining equality of morphisms in Hask as equality of the underlying Haskell values.

One alternative definition of equality of morphisms in Hask that has been offered is the weaker definition that two morphisms f and g are equal if and only if they satisfy f x = g x for all values x (including _|_). Note that there's still an ambiguity here. If f x and g x are themselves Haskell functions and so morphisms, does f x = g x mean equality of the morphisms f x and g x or equality of the Haskell values f x and g x? Let's ignore this problem for now.

Under this alternative definition, undef1 and undef2 are equal as morphisms, because we can show undef1 x = undef2 x for all possible values x of type () (namely () and _|_). That is, applied to (), they give:

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

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

and applied to _|_ they give:

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

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

Similarly, undef1 . id and undef2 can be shown to be equal as morphisms in Hask by this definition (in fact, they were equal as Haskell values which implies they're equal according to the weaker definition of equality of Hask morphisms), so there's no contradiction.

However, if you follow the link provided by @n.m., you can see that there's more work to do in terms of formalizing the meaning of equality of Haskell values and precisely giving an appropriate definition of equality of Hask morphisms before we'd really feel comfortable believing that there is a contradiction-free Hask category.

Proof that undef1 . id = undef2 as Haskell Values

For the reasons above, this proof is necessarily a little informal, but here's the idea.

If we are trying to witness a difference between functions f and g, the only way a witnessing expression can use these values is by applying them to a value x or by evaluating them to WHNF using seq. If f and g are known to be equal as Hask morphisms, then we already have f x = g x for all x, so no expression can witness a difference based on application. The only remaining thing to check is that when they are evaluated to WHNF they are either both defined (in which case, by the previous assumption, they will yield the same values when applied) or they are both undefined.

So, for undef1 . id and undef2, we just need to ensure that they are either both defined or both undefined when evaluated to WHNF. It's easy to see that they both, in fact, have defined WHNFs:

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

We already established above that undef1 x = undef2 x for all x. Technically, we ought to show that:

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

with equality as Haskell values for all x, which establishes that (undef1 . id) x = undef2 x for all x. Together with the fact that both have defined WHNFs above, this is enough to show that undef1 . id = undef2 with equality as Haskell values.

这篇关于Hask甚至是一个类别吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！