问题标签 [free-theorem]

根据Typeclassopedia和这个链接，一个类型只能有一个Functor实例（链接中有一个证明）。但我的理解是，给定类型可能有多个可能的Monad实例，对吗？但是对于给定的Monad实例，有一个免费的Functor实例

由此，我得出结论，如果我偶然发现了一种可以Monad以不同方式定义多个实例的类型，那么上述fmap派生的函数必须对所有这些实例都相等，换句话说，如果我有两对函数：

对于相同类型的构造函数m，比，必然：

对于所有xs :: a和f :: a -> b。

这是真的？这是否作为一个定理成立？

阅读这个答案促使我尝试构建并证明多态容器函数的规范形式。结构很简单，但证明让我难过。下面是我尝试编写证明的简化版本。

简化版本证明，由于参数性，足够多态的函数不能仅根据参数的选择来改变它们的行为。假设我们有两个参数的函数，一个是固定类型，一个是参数：

我想证明的属性：

Agda 内部可以证明这样的陈述吗？

对于足够多态的类型，参数性可以唯一地确定函数本身（详情请参阅Wadler定理！）。例如，唯一具有类型的总函数forall t. t -> t是恒等函数id。

是否有可能在 Idris 中陈述和证明这一点？（如果它不能在 Idris 内部得到证明，那是真的吗？）

以下是我的尝试（我知道函数相等不是 Idris 中的原始概念，所以我断言任何泛型类型的函数t -> t总是返回与恒等函数返回的结果相同的结果）：

产生的洞是：

我如何推导出类型的自由定理：

Nat简直在哪里data Nat = Z | S Nat？

原则上，这可以通过 Haskell 的“自由定理”包来回答，但它太老了，无法在我可以合理安装的任何 GHC 版本下编译。

如何使用插件Paramcoq证明以下自由定理？

如果不可能，那么这个插件的目的是什么？

我正在尝试从我的作业中做这个问题：

给定任意foo :: [[a]] -> ([a], [a])，写下函数foo满足的一个定律，涉及map列表和对。

一些背景：我是一年级本科生，正在学习函数式编程课程。虽然这门课程是介绍性的，但讲师在教学大纲中提到了许多内容，其中包括自由定理。因此，在尝试阅读 Wadler 的论文后，我认为concat :: [[a]] -> [a]法律map f . concat = concat . map (map f)看起来与我的问题相关，因为我们必须具有foo xss = (concat xss, concat' xss)whereconcat和concat'are 类型的任何函数[[a]] -> [a]。然后foo满足bimap (map f, map g) . foo = \xss -> ((fst . foo . map (map f)) xss, (snd . foo . map (map g)) xss)。

这个“法律”似乎太长了，不正确，我也不确定我的逻辑。所以我想到了使用在线免费定理生成器，但我不明白是什么lift{(,)}意思：

我应该如何理解这个输出？我应该如何foo正确推导出函数的定律？

我正在查看typeclass的法律，Alt如下所示：

其中一项法律是这样的：

更详细地说，这是：

假设我们 uncurry<!>操作，即我们假设类是这样写的：

我们可以这样写一个组合器：

这表示type Pair a = (a, a)函子与给定函子的组合f。所以它本身就是函子的态射映射。

有问题的法律现在可以这样写（不改变其含义）：

请注意，就像在法律的原始陈述中一样，mapBoth f它只是适用fmap f于 的两个论点。alt

This is akin to demanding that alt is a natural transformation from the functor (f -, f -) to the functor f -.

However, isn't it actually impossible for a function of alt's type not to be a natural transformation? How would one write a "bad" implementation of alt that that typechecks, but would be rejected by the law?

考虑以下包装器：

我想反驳（作为围绕这个有趣帖子的练习）存在一个合法Functor F实例，它允许我们将Int -> Int类型函数应用于实际内容并〜忽略〜所有其他函数（即fmap nonIntInt = id）。

我相信这应该用一个自由定理来完成（我在这里fmap读到）： 对于给定的 ,和,这样: ,给定构造函数的自然映射在哪里。fghkg . f = k . h$map g . fmap f = fmap k . $map h$map

什么定义了自然地图？我是否正确地假设它是一个简单flip const的 for F？

据我所知：$map f是我们Ff在范畴论中所指的。因此，从分类的意义上说，我们只是想要下图中的一些东西来通勤：

然而，我不知道用什么代替???s （也就是说，我们应用什么函子来得到这样的图，我们如何表示这个几乎fmap-？）。

那么，一般来说，什么是自然地图F？的自由定理的正确图是什么fmap？

我要去哪里？

考虑：

很容易看出f . g是h . k。然而，不存在的fmap只会执行，而f不是k，给出不同的结果。如果我对自然性的直觉是正确的，那么这样的证明就会奏效。这就是我想要弄清楚的。

@leftaroundabout提出了一个更简单的证明：fmap show . fmap (+1)改变内容，不像fmap $ show . (+1). 这是一个很好的证明，但我仍然想将自由定理作为练习。