Hask是否为范畴？如何理解undef1与undef2是不同值却为同一态射？

这是个很有意思的问题，触及了Haskell语义和Hask范畴定义的核心差异——咱们一步步拆解来看：

首先要明确：Hask范畴里的“态射”并不是直接对应Haskell中的函数值，而是函数值的等价类，等价关系是外延相等：两个函数f和g被视为同一个态射，当且仅当对所有可能的输入x，f x和g x在Haskell的语义下完全相等（即f x ≡ g x对所有x成立）。

回到你的例子：

• undef1 = undefined :: a -> b是一个“完全未定义”的函数值（属于Haskell里的bottom值）；
• undef2 = \_ -> undefined是一个已定义的lambda函数，只是它的返回值永远是bottom。

它们作为Haskell的值是不同的——比如seq undef1 ()会返回undefined（因为seq会尝试求值第一个参数，而undef1本身就是bottom），但seq undef2 ()返回()（因为undef2是一个合法的lambda值，seq不会深入求值它的内部逻辑）。但从外延行为来看，对任意输入x，undef1 x和undef2 x的结果都是undefined——没有任何输入能让它们的输出产生差异。

这种定义的本质是：Hask范畴抽象掉了Haskell函数的求值策略/严格性细节，只关注函数对输入的映射结果。这样做是为了让Hask满足范畴论的公理——比如你的例子里undef1 . id = undef2，从外延上看这个等式成立，所以它们是同一个态射，这符合范畴中态射复合的一致性要求。

验证的核心就是确认两个函数满足外延相等的条件，同时区分开内涵（值层面）和外延（态射层面）的差异：

1. 验证外延相等
   对任意类型为a的输入x：

   • undef1 x的结果是undefined（因为undef1本身就是类型为a->b的bottom，应用任何参数都会返回bottom）；
   • undef2 x是忽略x后返回undefined，结果同样是undefined。
     不存在任何x能让两者的输出不同，因此它们满足外延相等的条件，在Hask范畴中是同一个态射。

2. 区分值与态射的差异
   用seq测试可以看到它们作为值的不同：

   • 执行seq undef1 ()：seq要求第一个参数是“头部正规形式（WHNF）”，而undef1是bottom，无法达到WHNF，因此整个表达式返回undefined；
   • 执行seq undef2 ()：undef2是一个lambda，已经是WHNF，因此seq直接返回第二个参数()。
     但这种差异是内涵层面的，不影响函数的外延行为，因此在Hask范畴中不被视为不同的态射。

3. 验证复合后的等价性
   从等式推理来看，undef1 . id展开后是\x -> undef1 (id x)，而id x ≡ x，因此等价于\x -> undef1 x——这和undef2的外延行为完全一致，两者对所有x都返回undefined，进一步证明它们是同一个态射。

内容的提问来源于stack exchange，提问作者user8585703