问题标签 [forall]

我开始了解如何forall在所谓的“存在类型”中使用关键字，如下所示：

然而，这只是如何forall使用的一个子集，我根本无法理解它在这样的事情中的使用：

或者解释为什么这些不同：

或者整个RankNTypes东西...

我更喜欢清晰、没有行话的英语，而不是学术环境中常见的语言。我尝试阅读的大多数解释（我可以通过搜索引擎找到的解释）都存在以下问题：

1. 它们是不完整的。他们解释了这个关键字使用的一部分（比如“存在类型”），这让我感到很高兴，直到我阅读了以完全不同的方式使用它的代码（比如runST,foo和bar以上）。
2. 它们充满了假设，这些假设是我在本周流行的离散数学、范畴论或抽象代数的任何分支中读到的最新消息。（如果我再也没有读到“请参阅论文以了解实施细节”的话，那就太早了。）
3. 它们的编写方式经常将甚至简单的概念变成曲折扭曲和支离破碎的语法和语义。

所以...

关于实际问题。任何人都可以用清晰、简单的英语完整地解释这个forall关键字（或者，如果它存在于某个地方，指出我错过的如此清晰的解释）而不认为我是一个沉浸在行话中的数学家吗？

编辑添加：

下面的高质量答案中有两个突出的答案，但不幸的是，我只能选择一个作为最佳答案。 诺曼的回答详细而有用，以一种显示一些理论基础的方式解释事物，forall同时向我展示了它的一些实际含义。 亚初的回答涵盖了其他人没有提到的领域（作用域类型变量），并用代码和 GHCi 会话说明了所有概念。如果可以选择最好的，我会的。不幸的是，我不能，并且在仔细查看了这两个答案之后，我认为由于说明性代码和附加的解释，yairchu 稍微优于 Norman 的。然而，这有点不公平，因为我确实需要两个答案来理解这一点，以至于forall当我在类型签名中看到它时不会让我有一种微弱的恐惧感。

好的，我还有另一个代码合同问题。我有一个看起来像这样的接口方法的合同（为清楚起见，省略了其他方法）：

我有使用如下界面的代码：

AddRequested需要一个非空输入参数（它实现了一个具有 Requires 合同的接口），因此在传递到AddRequested. 我是否正确使用了 ForAll 语法？如果是这样并且求解器根本不理解，是否有另一种方法可以帮助求解器识别合同，或者我是否只需要在调用 GetAllGroups() 时使用 Assume？

对不起我的英语不好。所以，这是我的问题，我正在尝试通过 PLINQ 更新 DataTable 这是我的代码

但有例外：“索引超出范围。必须为非负数且小于集合的大小。参数名称：索引”

请帮我

我得到了一个代表金属板表面温度点的二维矩阵。矩阵（板）的边缘保持恒定在 20 摄氏度，并且在一个预定义的点有一个 100 摄氏度的恒定热源。所有其他网格点最初设置为 50 摄氏度。

我的目标是获取所有内部网格点并通过对周围四个网格点（i+1、i-1、j+1、j-1）进行迭代平均来计算其稳态温度，直到我达到收敛（变化迭代之间小于 0.02 摄氏度）。

据我所知，我遍历网格点的顺序无关紧要。

对我来说，这听起来是调用 FortranFORALL结构并探索并行化乐趣的好时机。

如何确保代码确实被并行化了？

例如，我可以在我的单核 PowerBook G4 上编译它，我预计并行化不会提高速度。但是如果我在双核 AMD Opteron 上编译，我会假设 FORALL 结构可以被利用。

或者，有没有办法衡量程序的有效并行化？

更新

针对 MSB 的问题，这是 gfortran 版本 4.4.0。gfortran 是否支持自动多线程？

值得注意的是，FORALL 结构已经过时了，我想，然后是自动矢量化。

也许这对于一个单独的问题是最好的，但是自动矢量化是如何工作的？编译器是否能够检测到循环中只使用了纯函数或子例程？

我正在使用 C# 4.0 和代码合同，并且我有自己的自定义GameRoomCollection : IEnumerable<GameRoom>.

我想确保，任何实例GameRoomCollection都不会包含null值元素。不过，我似乎无法做到这一点。我没有制定一般规则，而是尝试做一个简单明了的例子。是的AllGameRooms一个实例GameRoomCollection。

谁能看到，为什么我没有证明，那gameRoom不是null？

编辑：

在迭代之前为对象添加引用也不起作用：

编辑2：

但是：如果我将游戏室集合类型转换为数组，它可以正常工作：

这是因为您无法为IEnumerable<T>接口的方法定义规则吗？

EDIT3：这个问题可以与这个问题有关吗？

我正在努力理解与existsHaskell 类型系统相关的关键字。据我所知，默认情况下Haskell中没有这样的关键字，但是：

• 在像这样的声明中有添加它们的扩展data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• 我看过一篇关于它们的论文，并且（如果我没记错的话）它指出exists关键字对于类型系统来说是不必要的，因为它可以被概括为forall

但我什至无法理解是什么exists意思。

当我说 时forall a . a -> Int，它意味着（在我的理解中，我猜是不正确的）“对于每个 (type) a，都有一个类型的函数a -> Int”：

当我说exists a . a -> Int时，它甚至意味着什么？“至少有一种类型a具有某种类型的功能a -> Int”？为什么要写这样的声明？目的是什么？语义？编译器行为？

请注意，它并不是一个可以编译的真实代码，只是我想象的一个例子，然后我听说了这些量词。

PS 我不是 Haskell 的新手（可能像二年级学生），但我缺乏这些东西的数学基础。

PL/SQL forall 循环是否以特定间隔自动提交，还是我需要在循环后提交？

甲骨文 10g 和 11g

我目前有一个执行批量收集的 pl/sql 脚本，然后运行 ​​3 个不同的 forall 循环来迭代集合。我目前在每个 forall 循环完成后提交，脚本中有一个提交语句。需要这个吗？它是否会减慢执行速度，尤其是当集合有几百万个条目时？

谢谢

例如，在memocombinators包的源代码中，没有明确提到 LANGUAGE pragma，并且在尝试导入它时出现错误，因为不包括支持显式 forall 语句的扩展。我怎么知道在这种情况下需要哪个扩展？

如下所示，在 Haskell 中，可以将具有异构类型的值存储在列表中，并对其具有特定的上下文边界：

如何在 Scala 中实现相同的目标，最好不使用子类型？

所以我必须编写不同的程序来帮助我解决农民-狼-山羊-卷心菜-肥料的难题。对于那些不知道的人，它涉及到一个农民必须带着所有其他物品从一条河流的北岸穿越到南岸。银行在 3 种情况下变得安全：农夫在场，或者狼没有和山羊在一起，或者，山羊没有和卷心菜一起留下。出于练习的目的，变量将是 [f,b,g,w,c]。

我坚持的程序（选择（银行，项目））涉及找到一个包含 1 或 2 个元素的列表（始终包括农民 - f），这可能是银行运输的一部分，而不会使其不安全。

如果确实选择([g,f,b], Items)，则 Items 的可能返回值可以是 [f]、[f,g]、[f,b]。但是，如果我们选择([g,f,c], Items)，则返回的唯一可能值是 [f,c] 或 [f,g]，因为山羊和卷心菜不能放在一起。

因此，谁能给我一个提示，如何获得项目的所有可能选项，但列表中不超过 2 个项目？