"你不明白欣德利 - 米尔纳的哪一部分？"

Question

我发誓曾经有一件T恤出售,上面写着不朽的话:

---

什么部分

你不明白吗？

---

就我而言,答案就是......全部!

特别是,我经常在Haskell论文中看到这样的符号,但我不知道它的含义是什么.我不知道它应该是什么样的数学分支.

我当然认识到希腊字母的字母,以及诸如"∉"之类的符号(通常意味着某些东西不是一组的元素).

另一方面,我以前从未见过"⊢"(维基百科称它可能意味着"分区").我也不熟悉这里使用的vinculum.(通常它表示一个级分,但是这并不出现在这里是这种情况.)

如果有人至少可以告诉我从哪里开始想要理解这个符号海洋的含义,那将会有所帮助.

Answer 1

• 所述水平条是指"[见上] 意味着 [下文]".
• 如果有多个表达式在[见上],则考虑它们相与在一起; 所有[上述]必须为真以保证[下方].
• :手段有类型
• ?意思是在.(同样?意思是"不在".)
• ?通常用于指代环境或背景; 在这种情况下,它可以被认为是一组类型注释,将标识符与其类型配对.因此x : ? ? ?意味着环境?包括x具有类型的事实?.
• ?可以被证明是证明或决定的.? ? x : ?表示环境?确定x具有类型?.
• ,是一种在环境中包含特定附加假设的方法?.
  因此,?, x : ? ? e : ?'意味着环境?,与该附加的首要假设x有一个类型?,证明e已键入?'.

根据要求:运营商优先级,从最高到最低:

• 语言特定的缀和mixfix运营商,如? x . e,? ? . ?,和? ? ?',let x = e0 in e1和空白为功能应用.
• :
• ? 和 ?
• , (左结合)
• ?
• 分隔多个命题的空格(关联)
• 横杠

Answer 2

这种语法虽然看起来很复杂,但实际上相当简单.基本思想来自形式逻辑:整个表达是一种含义,上半部分是假设,下半部分是结果.也就是说,如果你知道顶部表达式是真的,你可以得出结论底部表达式也是真的.

符号

另外要记住的是,有些字母具有传统意义; 特别是,Γ代表你所处的"背景" - 即你所看到的其他类型的东西.所以类似的? ? ...意思是" ...当你知道每个表达式的类型时的表达式?.

该?符号实质上意味着你可以证明一些东西.所以? ? ...声明说"我可以...在上下文中证明?.这些陈述也称为类型判断.

要记住的另一件事是:在数学中,就像ML和Scala一样,x : ?意味着x有类型?.你可以像Haskell一样读它x :: ?.

每条规则的含义

所以,知道这一点,第一个表达式变得易于理解:如果我们知道x : ? ? ?(即在某些上下文中x有某种类型),那么我们就知道(即,in ,具有类型).所以真的,这并没有告诉你任何超级有趣的东西; 它只是告诉你如何使用你的上下文.??? ? x : ??x?

其他规则也很简单.例如,拿[App].此规则有两个条件:e?是从某种类型?到某种类型的函数?',e?是类型的值?.现在你知道你将通过应用获得什么类型e?来e?!希望这不是一个惊喜:).

下一个规则有一些新的语法.特别是,?, x : ?仅仅意味着由上下文构成?的判断和判断x : ?.因此,如果我们知道变量x具有类型?并且表达式e具有类型?',我们也知道获取x和返回的函数的类型e.这只是告诉我们如果我们弄清楚函数采用什么类型以及它返回什么类型该怎么做,所以它也不应该令人惊讶.

下一个只是告诉你如何处理let语句.如果你知道有些表达e?有型?,只要x有一个类型?,那么let它结合本地表达x到类型的值?将e?有一个类型?.真的,这只是告诉你一个let语句本质上允许你用一个新的绑定扩展上下文 - 这正是let它的作用!

该[Inst]规则涉及子类型.它表示如果你有一个类型的值,?'并且它是一个子类型?(?表示一个部分排序关系),那么该表达式也是类型?.

最终规则涉及泛化类型.快速搁置:自由变量是一个变量,它不是由某个表达式中的let语句或lambda引入的; 该表达式现在,取决于其context.The规则的自由变量的值是说,如果有一些变量?是不是 "免费"在您的上下文任何东西,那么它是安全地说,它的类型,你知道任何表情e : ?将具有该类型的任何值?.

如何使用规则

那么,既然您已了解符号,那么您对这些规则有何看法？好吧,您可以使用这些规则来确定各种值的类型.要做到这一点,请查看您的表达式(比如说f x y)并找到一个与您的陈述相符的结论(底部)的规则.让我们称之为你想要找到你的"目标".在这种情况下,您将查看以此结尾的规则e? e?.当你发现这一点时,你现在必须找到规则,证明这条规则的所有内容.这些东西通常对应于子表达式的类型,因此您实际上是对表达式的某些部分进行递归.您只需执行此操作,直到完成校对树,这样可以证明表达式的类型.

因此,所有这些规则都是精确地指定 - 并且在通常的数学上迂腐的细节:P-如何找出表达式的类型.

现在,如果您曾经使用Prolog,这应该听起来很熟悉 - 您实际上是像人类Prolog解释器一样计算证明树.Prolog被称为"逻辑编程"是有原因的!这也很重要,因为我介绍HM推理算法的第一种方法是在Prolog中实现它.这实际上非常简单,并且清楚地表明了这一点.你当然应该尝试一下.

注意:我可能在这个解释中犯了一些错误,并且如果有人指出它们会很喜欢它.我实际上会在几周内在课堂上报道,所以我会更自信:P.

Answer 3

如果有人能够至少告诉我从哪里开始想要理解这个符号海洋意味着什么

参见" 编程语言的实用基础 ",第2章和第3章,通过判断和推导来讨论逻辑风格.整本书现已在亚马逊上市.

第2章

归纳定义

归纳定义是编程语言研究中不可或缺的工具.在本章中,我们将开发归纳定义的基本框架,并举例说明它们的使用.归纳定义包括一组用于推导各种形式的判断或断言的规则.判断是关于指定排序的一个或多个句法对象的陈述.规则规定了判决有效性的必要和充分条件,从而充分确定其含义.

2.1判决

我们从判断的概念开始,或者关于句法对象的断言.我们将利用多种形式的判断,包括以下例子:

• n nat - n是一个自然数
• Ñ = N1 + N2 - Ñ是的总和N1和N2
• τ 型 - τ是一种类型
• e:τ - 表达式e具有类型τ
• ë ⇓ v -表达Ë具有值v

判断表明一个或多个句法对象具有彼此某种关系的属性或立场.财产或关系本身被称为判断形式,并且一个或多个对象在该关系中具有该属性或立场的判断被认为是该判断形式的实例.判断形式也称为谓词,构成实例的对象是其主语.我们写一个 Ĵ的判断断言Ĵ的持有一个.当强调判断的主题并不重要时,(文字在这里切断)

Answer 4

符号来自自然演绎.

⊢符号称为十字转门.

这6条规则非常简单.

Var 规则是相当简单的规则 - 它表示如果类型标识符的类型已存在于您的类型环境中,那么要推断类型,您只需从环境中获取它.

App规则说如果你有两个标识符e0并且e1可以推断它们的类型,那么你可以推断出应用程序的类型e0 e1.如果您知道e0 :: t0 -> t1并且e1 :: t0(相同的t0!),则规则如下所示,然后应用程序是良好类型的,类型是t1.

Abs并且Let是推断lambda抽象和let-in类型的规则.

Inst 规则说你可以用较不普遍的类型替换.

Answer 5

我如何理解Hindley-Milner规则？

Hindley-Milner是一组以后续微积分形式的规则(不是自然演绎),它表示你可以在没有明确的类型声明的情况下从程序的构造中推导出一个程序的(最一般的)类型.

符号和符号

首先,让我们解释符号

• 是一个标识符(非正式地,变量名称).
• : means是一种(非正式地,实例或"is-a").
• (sigma)是一个变量或函数的表达式.
• ε表示是元素
• (Gamma)是一个环境.
• ⊦(断言符号)表示断言(或证明,但在上下文中"断言"读取更好.)
• ⊦ : 因此读取断言,a
• 是类型的实际实例(元素) .
• (tau)是一种类型:基本的,可变的(),功能→'或产品×'
• →'是一种功能型 和'是类型.
• .手段 (lambda)是一个带参数的匿名函数, ,并返回一个表达式, .
• 让 =₀ 在 ₁指表达,₁,替代₀无论 出现.
• ⊑表示先前元素是后一元素的子类型(非正式 - 子类).
• 是一个类型变量.
• ∀ .是一个类型,∀(对所有)参数变量,,回来 表达
• ∉free ()表示不是外部上下文中定义的自由类型变量的元素.(绑定变量是可替代的.)

线上的一切都是前提,下面的一切都是结论(Per Martin-Löf)

接下来是对逻辑语句的英语解释,然后是松散的重述和解释.

变量

给定是(sigma)的一种类型,(Gamma)的元素,
conclude asserts是a.

换句话说,我们知道是类型因为是类型的.

这基本上是一个重言式.标识符名称是变量或函数.

功能应用

给定断言0是函数类型,断言1是
结束断言应用函数0到1是一个类型'

为了重述规则,我们知道函数应用程序返回类型'因为函数有类型→'并获得类型的参数.

这意味着如果我们知道一个函数返回一个类型,并将它应用于一个参数,那么结果将是我们知道它返回的类型的实例.

功能抽象

给定和类型断言是一种类型,'
conclude断言一个匿名函数,返回表达式,类型为→'.

同样,当我们看到一个接受并返回表达式的函数时,我们知道它是类型→'因为(a)声明它是'.

如果我们知道是类型,因此表达式是',那么返回表达式的函数是类型→'.

让变量声明

给定断言的类型,和 类型的断言,断言类型为1的
断言断言let= 0 in的类型

宽松地,在1(1)中受到0的约束,因为τ是a,并且断言1是a.

这意味着如果我们有一个表达式that是一个(是一个变量或一个函数),一个名字,也是一个和一个类型的表达式1,那么我们可以用substitute代替它在¹中出现的任何地方.

实例化

给定类型'和'的
断言是conclude断言的子类型

表达式是父类型,因为表达式是子类型',并且是父类型'.

如果实例的类型是另一种类型的子类型,那么它也是该超类型的实例 - 更通用的类型.

概括

给定断言是a 并且 不是自由变量的元素,
结束断言,为所有返回表达式的参数表达式键入

所以通常,为所有参数变量()返回键入,因为我们知道它是一个并且不是自由变量.

这意味着我们可以将程序概括为接受所有类型的参数,这些参数尚未绑定在包含范围内(非非本地变量).这些绑定变量是可替代的.

把它们放在一起

给定某些假设(例如没有自由/未定义的变量,已知环境),我们知道以下类型:

• 我们程序的原子元素(变量),
• 函数返回的值(Function Application),
• 功能构造(功能抽象),
• 让绑定(让变量声明),
• 父类型的实例(实例化),和
• 所有表达式(泛化).

结论

这些规则的组合使我们能够证明断言程序的最一般类型,而不需要类型注释.

Answer 6

有两种方法可以考虑e:σ.一个是"表达式e具有类型σ",另一个是"表达式e和类型σ的有序对".

查看Γ作为关于表达式类型的知识,实现为一组表达式和类型,e:σ.

旋转门⊢意味着从左侧的知识中,我们可以推断出右侧的内容.

因此可以读取第一个规则[Var]:
如果我们的知识Γ包含对e:σ,那么我们可以从Γ推导出e具有类型σ.

可以读取第二个规则[App]:
如果我们从Γ可以推断出e_0具有类型τ→τ',并且我们从Γ可以推断出e_1具有类型τ,那么我们从Γ可以推断出e_0 e_1具有输入τ'.

写Γ,e:σ而不是Γ∪{e:σ}是很常见的.

因此可以读出第三个规则[Abs]:
如果我们从Γ延伸到x:τ可以推导出e具有类型τ',那么我们从Γ可以推导出λx.e具有类型τ→τ'.

第四条规则[让]留作练习.:-)

可以读取第五个规则[Inst]:
如果我们从Γ可以推导出e具有类型σ',并且σ'是σ的子类型,那么我们从Γ可以推导出e具有类型σ.

可以读取第六个也是最后一个规则[Gen]:
如果我们从Γ可以推导出e具有类型σ,并且α在Γ中的任何类型中都不是自由类型变量,那么我们从Γ可以推导出e具有类型∀ασ.