时间戳

首页 > 解决方案 > 单位情况下如何理解米田的基数？

haskell - 单位情况下如何理解米田的基数？

问题描述

请注意，这不是严格意义上的haskell问题，但这就是我一直在玩这个的地方，也是我看到米田引理表达得最干净的地方......

所以，根据 yoneda 引理，我们知道

forall x . (a -> x) -> f x ~= f a

但我想知道的是，当类型 x 的基数低于 a 时，它如何工作？例如，unit...采用 f=Identity, a=Integer, x=Unit 我们得到类似

(Integer -> ()) -> Indentity () ~= Identity Int

哪个似乎没有意义？

我一直以 a=Bool 和 x=Int 的形式想到 yoneda

(Bool -> Integer) -> Identity Integer ~= Identity Bool

从某种意义上说，Identity Integer“似乎”比 Identity Bool 大，但鉴于它必须由 Bool->Integer 构建，我们知道实际上只有两个选项......但我觉得翻转它表明所说的理解不太正确。

我将不胜感激任何帮助理解这一点！

标签： haskell

解决方案

你无法修复x ~ ()。为了保持恒等式，该函数必须适用于 的每一个选择x，而不仅仅是一个特定的选择。这就是为什么forall在那个参数上有一个。因此，让我们重铸您的示例，保留参数超过x. 我给你一个以下类型的函数

(Integer -> x) -> Identity x

承诺它适用于x您选择的任何产品。我可能实现这个函数的唯一方法是Integer我手里已经有了一个，然后调用你给我的函数，产生一个x. 因此，我的函数相当于一个Identity Integer.

同样我们可以采取a ~ Bool, f ~ [], 屈服

(Bool -> x) -> [x]

我可以实现这一点的唯一方法是，如果我有一个[Bool]躺着，并用我的每个Bools 调用你的函数。

由于必须是多态的，它没有特定的基数，因此不会出现x小于或大于的问题。a

推荐阅读