问题标签 [type-theory]

我正在尝试为图形编写一个类型类。基本上，类型类看起来像：

其中我n用来表示节点的类型。

然后我有如下Graph定义：

其中Array是从标准容器中采用的Data.Array，其结构是用将每个节点映射到其相邻节点的方式来表示一个有限图。

问题来了，当我尝试FiniteGraph创建Graph.

不幸的是，这不起作用，因为!运算符需要约束Ix n，但我找不到在哪里声明它。

我希望实例声明类似于：

但这需要ginclass Graph g有 kind*而不是* -> *，这样我就没有地方可以显示n依赖了g。

那么我能用它做什么呢？谢谢。

我正在重写 PHP 类型系统并致力于实现更纯粹的语言。我正在尽可能多地实现纯粹主义作为功能性和面向对象的语言，如方法链、作为对象的类型、消息传递、作为方法的条件和一些其他特性http://github.com/haskellcamargo /生。在这里，函数将是 Func类的实例，在我为它做一个转译器之后，因为 PHP 已经走到了现在。Func将不限于将一元函数作为参数，但会在调用时检查参数的数量是否与预期参数的数量完全匹配：

其中 add 将是一个我不需要控制它的元数的函数，因为它是一元的并且通过柯里化工作。但是当我使用接收多个参数的函数时，我的问题就出现了。让我们以一个在屏幕上输出名称的简单函数为例：

$say_name需要1 个唯一参数，但我如何断言它将接收n 个参数，即这个匿名函数的数量？

$say_name -> invoke("Test");可能有效，但$say_name -> invoke("Test", 1);也有效，因为我没有办法了解匿名函数的数量。

function () { return func_num_args(); }

这将返回传递给它的参数数量。我需要知道所需参数的数量x，例如：

function x(Int $i, Functor $j) { return a_magic_function_that_returns_it_all(); }

并输出我类似的东西array(2) { [0]=> Int [1]=> Functor }。有人可以帮我吗？

例如，给定类型A、B和C：A × B × C =( A × B )× C = A ×( B × C ) 是真的，还是元组总是“扁平化”？直觉会告诉我它是关联的，但另一方面这意味着元组的元组是不可能的。我发现在我能找到的任何资源中都没有提到类型产品运算符的属性 -维基百科页面描述了产品类型，但没有详细介绍运算符本身。

我发现逻辑和编程之间存在同构，称为Curry-Howard 对应关系，那么类别理论是否存在这样的等价关系，有助于理解 Functors 或 Monads 之类的东西？

我正在尝试编写一个谓词，“如果某个常数为真”（在这种情况下，如果 'sec=ok'）那么谓词将评估为 False，因为我已经在那个特定的结果中编写了一个表达式与谓词其他地方的另一个表达式相矛盾的暗示。(f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) 应该是矛盾的，因为 x 和 ci 都是普遍量化的并且具有相同的类型。

但是，Nitpick 产生了一个我无法理解的反例。我希望是否有人可以检查这个引理，看看是否可以证明矛盾。或者让我知道我哪里出错了。所以简要说明如下；

• f 和 g 是从任意类型 'a 到 'b 的两个偏函数。

• 'sec' 是一个常量，其值为 'ok' 和 'notok'

  /li>

我还看到了两个 Z 数学工具包之间关于函数应用的“细微”差异。我都试过了，但问题仍然存在。

可以在这里看到 Nitpick 错误 http://i58.tinypic.com/316te1t.png

注意：作为参考，请从 HOL-Z 中找到我当前使用的部分函数的定义。

函数式语言中的GADT是否等同于传统的OOP + 泛型，或者存在这样一种情况，即 GADT 很容易强制执行正确性约束，但使用 Java 或 C# 很难或不可能实现？

例如，这个“类型良好的解释器”Haskell 程序：

可以使用泛型和每个子类的适当实现在 Java 中等效地编写，但要冗长得多：

在尝试了几个小时的不同版本后，我放弃了。我只想对 HoTT-Book 中所述的等式传递性的证明进行类型检查。我是 Agda 的新手，所以它可能只是一个小缺陷，也可能是一个更大的缺陷......不知道。我在 Agda 中为 HoTT 查阅了不同的库，但我发现的那些（在我看来）有相当复杂的解决方案。

它基于以下路径归纳的实现。

谢谢你的帮助。

我简化了peirce、classic、excluded_middle、de_morgan_not_and_not和implicit_to_or互等价的证明过程，主要写git@github.com:B-Rich/sf.git如下。

我成功删除了一些intuition战术，除了最后两个。

我的问题是：

• 如何在不使用intuition策略的情况下证明 to_or_peirce 和 de_morgan_to_or？
• 战术有什么作用intuition？
• 有没有办法提取该策略可能产生的具体程序intuition？

我正在尝试为玩具语言编写自己的类型推断算法，但我遇到了障碍——我认为算法 W 只能用于过于通用的类型。

以下是表达式：

类型化规则很简单——我们继续使用类型变量进行抽象和应用。以下是所有可能的类型：

正如您可能已经猜到的那样，ELit : TMono，更具体地说，EConc :: TMono → TMono → TMono。

我的问题来自于进行实际的类型推断。当递归表达式结构时，看到 an 时的一般技术EAbs是生成一个新的类型变量来表示新绑定的变量，用(String : TVar fresh)判断替换我们上下文中出现的任何类型，然后继续向下表达式。

现在，当我点击 时EConc，我正在考虑采用相同的方法 - 将子表达式的自由表达式变量TMon替换为上下文，然后对子表达式进行类型推断，并将两个结果的最通用统一符作为主要替代返回。但是，当我使用类似 的表达式尝试此操作时EAbs "x" $ EConc ELit (EVar "x")，我得到了不正确的TFun (TVar "fresh") TMon.

在 Agda 中使用证明验证时，我意识到我对某些类型显式地使用了归纳原则，而在其他情况下则使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字：“在 Agda 中，依赖类型的模式匹配是该语言的一种原语，核心语言没有模式匹配所转换的归纳/递归原则。”

那么，由于 Agdas 模式匹配，Agda 中的类型理论归纳和递归原则（定义类型上的函数）是否完全多余？像这样的东西（隐含的路径归纳）只有教学价值。

http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pa​​ttern_matching