多态递归的类型推断及可类型性研究：Hindley-Milner和交叉类型系统的讨论

理论计算机科学电子笔记136（2005）57-102www.elsevier.com/locate/entcs需要多态递归的杰杰Hallett1波士顿大学美国波士顿A. J. Kfoury2波士顿大学美国波士顿摘要为多态递归函数定义推断类型（缩写为多态递归）是流行类型化编程语言邮件列表上反复出现的主题。这是尽管事实上，类型推断多态递归使用的是非决定性的类型已被证明。本报告介绍了几个涉及多态递归的编程示例，并确定了它们在各种类型系统下的可类型性，包括Hindley-Milner系统，一个交叉型系统，以及这两个系统的扩展。这份报告的目的是表明，这些例子中的许多都是可类型化的，使用交集类型系统作为多态性的替代形式。通过实现这一点，我们希望奠定基础，为未来的研究成为一个可判定的交叉型推理算法。我们没有提供一个全面的调查类型系统适合多态递归，或没有类型注释插入到源语言。相反，我们关注的例子，类型可以推断没有类型注释，重点是系统的交叉类型。保留字：多态递归，交集类型，有限多态，示例1电子邮件：jhalllett@cs.bu.edu2 电子邮件地址：kfoury@cs.bu.edu1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.06.01458J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）571介绍背景和动机在多态递归的情况下，使用SML类型（SML中常见的“类型模式”）进行类型推断[10、11、4]。尝试解决这个限制包括用户的显式类型注释[8]和用户可调的迭代限制[17]。然而，这两种方法都需要程序员积极参与类型检查过程，从而破坏了自动类型推断和透明类型检查的目标。还有一种SML实现，它允许用户在标准类型系统（受限制到单态递归）和一个用多态递归扩充的类型系统，试图证明然而，需要多态递归的程序不断出现在诸如SML、Haskell和OCaml的编程语言的邮件列表上的讨论中。报告的贡献本文试图通过讨论几个在SML标准类型系统（也称为Hindley-Milner系统）下无法进行类型化的例子，为进一步研究隐式多态递归的可类型化性奠定基础。这些例子（大部分）是用SML语法编写的（其中一个例子是用Haskell语法编写的），并伴随着SML/NJ类型检查器发现的相应错误。一些示例也以Haskell语法显示，并带有相应的GHC错误消息，以比较SML/NJ和GHC编译器的错误报告。我们还讨论了使用Hindley-Milner系统无法典型化的例子，这些例子使用了具有交叉类型的多形态计算-也称为Milner-Mycroft系统-但可以使用交叉类型系统来典型化。这些示例支持使用交集类型作为表示多态性的交集类型的替代。此外，我们阐明了我们所谓的“无限宽度”的交叉类型的例子的需要。然而，我们不会以这种方式扩展我们的标准（有限宽度）交叉口类型系统，因为我们不知道标准系统的直接扩展，开发一个超出了本报告的范围。因此，我们求助于多态递归，对于这些示例，请按以下方式操作：，我们提供了一些无法识别的示例J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5759使用我们的交互式系统，但使用它的交互式系统。一个示例还给出了这种类型和 类型之间的高要求。 首先，我们提出了一个多态递归程序，它既不能用交集类型也不能用递归类型来类型化。报告的结构本文的结构如下。首先，我们定义我们要处理的类型，然后，我们提出我们在报告后面考虑的几个类型系统的规则，从Hindley-Milner系统开始，我们在这里表示HM;这在第2节中完成。在剩下的部分中，我们将介绍几个简单而自然的多态递归示例，以促进增强系统HM。我们开发的类型系统，允许多态递归使用唯一的交集类型（HM），唯一的交集类型（S），通用和交集类型（S）。使用这些系统，我们可以构建对于大多数例子来说都是有效的类型派生。下图总结了本报告中开发的示例在我们定义的四种类型系统中的可类型性。3图表的最后一栏，标题为3系统S被称为“S“，用于a b e t e r n a m a c k。60J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57例如HMH.M.SS小规模改建双CCCC麦考夫CCCC总计列表CCCC组合物CCCC埃塞尔山口CCCC困惑CCC矩阵转置CCC向量加法CCC收集CC酒吧CC结构列表C延迟上表在以下方面有点误导。该表表明，某些示例在我们的交叉点类型（S），但不是在我们的系统中的类型（HM）。尽管HM限制了类型表达式中的量化器只能出现在最外面的位置，但S对类型表达式中的量化器的有关此问题的进一步讨论，请参见第8相关工作关于多态递归程序的其他例子，特别是类似于Collect例子的嵌套递归数据类型，请参见Chris OkasakiSimon Peyton-Jones和Mark Shields撰写了一篇论文，描述了GHC通过显式用户定义类型注释推断任意高秩类型时所采用的方法[9]。今后工作在未来，我们计划探索一个可判定的（希望是可行的）类型推理和检查算法的交集类型的系统下，大多数，如果不是全部，在本报告中的例子可以类型化的可能性。我们还想研究是否引入膨胀变量，J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5761与系统I一起开发的技术，到我们的交叉型系统中将产生任何好处[14]。致谢乔·威尔斯是一个不断鼓励和技术建议的来源。我们还要感谢SimonPeyton-Jones提供的宝贵反馈，特别是关于更高级别的 分析类型的反馈。2类型和类型系统类型的语法由以下语法指定：τ∈Type：：= α|τ→τ|τ×τ|τ列表|τ∧τ|int|bool|......这是什么？σ∈Scheme：：= τ|α.σ注意，我们使用τ作为一个元变量，其范围在集合Type上，该集合包含简单类型与交集类型的组合，而σ作为一个元变量，其范围在集合Scheme上，该集合Scheme包含Type的所有成员，每个成员之前有零个或多个量化器。特别地，Type是阴谋我们在报告的其余部分中列出了四种不同的系统。基本类型系统HM类似于SML、Haskell和OCaml的类型系统，它允许let多态和单态递归。系统HM递归是系统HM的扩展，允许多态递归一般来说，只要量子化器在所有量子化器之外，类型构造函数。系统S允许交叉类型;S通过交叉类型提供我们开发的最后 一 个 系 统 叫 做 S.SystemmS将 所 有 类 型 的 intersection_t_y_p 和intersection_t_y_t我们现在概述阅读下表的惯例。我们假设存在一个函数type，从termconstants到types，使得type（c）是constantc的类型。我们在打字判断中使用上下文。SQL是术语变量和类型之间的绑定序列。然而，我们也允许将xm作为从项变量到类型的函数，这样xm（x）是绑定到变量x的类型。最后，我们使用从上下文到类型变量集合的函数FTV，使得FTV（）是在上下文中出现的自由类型变量首先，我们定义系统HM。62J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57系统HM打字规则：（所有类型都是无错误的类型（c）=σ电子邮件：info@bjc.com（-常数）（x）=σ（σ闭合）∆►x:σ(∀-Var)Δfnx=> M：τ→τJ（Abs）n，x：τM：τJ∆►M:τ→τJ∆►N:τ中国：τJ（应用程序）M：σ，x：σN：τ（τ-Let）在N端的x=M的三角形：τx1：τ1，.，xn：τ n<$N：τx1：τ1，.，xn：τ n<$M p：τp因此，让val rec x1= M1和.且xn=Mn在N端：τ（Rec）（1≤p≤n）质量标准：σ（Gen）∆►M:∀α.σ（α/∈FTV（ε））∆►M:∀α.σ(Inst)∆►M:σ[α:=τ]∆►M1:τ1∆►M2:τ2(×)时间（M1，M2）：τ1×τ2单位时间：τ1×τ2（Fst）最大值（M）：τ1平均值（M）：τ2平均值：τ1×τ2（Snd）∆►M1:bool∆►M2:τ∆►M3:τ(If)如果M1，则M2，否则M3：τ为了定义系统HM，我们简单地用规则（H-Rec）扩充HMJ.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5763系统HM键盘输入规则：（所有类型都是无键盘系统HM的所有类型化规则都是系统HM编译的类型化规则除以下内容外。x1：σ1，.，xn：σ n<$N：τx1：σ1，.，x n：σ n<$M p：σ p因此，让val rec x1= M1和.且xn=Mn在N端：τ（-Rec）（1≤p≤n）注意，我们允许规则（Rec-Rec）和（Rec）在系统HM中共存。这是可以接受的，因为（Rec）只是（Rec-Rec）的一个特例。系统S仅使用交叉点类型。64J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57SystemS打字规则：（所有类型都是无限制的类型（c）=τ∆►c:τ(∧-Const)(τclosed)（x）=τ∆►x:τ(∧-Var)n，x：τM：τJΔfnx=> M：τ→τJ（Abs）∆►M:τ→τJ∆►N:τ简体中文：τJ（App）∆►M:τJ∆,x:τJ►N:τN端上的x=M：τ（x-Let）x1：τ1，.，xn：τ n<$N：τx1：τ1，.，xn：τ n<$M p：τp因此，让val rec x1= M1和.且xn=Mn在N端：τ（-Rec）（1≤p≤n）∆►M1:τ1∆►M2:τ2(×)时间（M1，M2）：τ1×τ2单位时间：τ1×τ2最大值（M）：τ1（Fst）M：τ1×τ2平均值（M）：τ2（Snd）∆►M:τi i∈I∆►M:∧i∈Iτi（）（size（I）≥2），（size（I）is finite）电子邮件： INFO@JJS.COM∆►M:τJ(Sub)τ≤τ（S-Re）τ1≤τ2τ2≤τ3τ1≤τ3（S-反式）τ1≤τJτJ≤τ2τJ≤τ1τJ≤τ21 2（S-Fun）τJ→τJ ≤τ1 →τ21 2（S-配对）τJ×τJ ≤τ1 ×τ21 2 1 2J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5765我τi≤τJi∈I I<$J J（S-）i∈Jτi ≤ τi∈Iτi66J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57系统提示输入规则：系统S的所有类型化规则都是系统S编译的除以下内容外。类型（c）=σ电子邮件：info@bjc.com（-常数）（x）=σ（σ闭合）∆►x:σ(∀-Var)M：σ，x：σN：τ（τ-Let）在N端的x=M的三角形：τx1：σ1，.，xn：σ n<$N：τx1：σ1，.，x n：σ n<$M p：σ p因此，让val rec x1= M1和.且xn=Mn在N端：τ（-Rec）（1≤p≤n）质量标准：σ（Gen）∆►M:∀α.σ（α/∈FTV（ε））∆►M:∀α.σ(Inst)∆►M:σ[α:=τ]实践证明，这一制度是健全的。证据可在附录B中找到。最后，我们定义系统S。注意，系统S中的（E-Const）、（E-Var）、（E-Let）和（E-Rec）是系统S中的（E-Const）、（E-Var）、（E-Let）和（E-Rec）的特殊情况。3可在HM和S3.1双3.1.1双耦合下面是一个简单的示例，它揭示了SML中多态递归的不可类型性let val rec double = fn f => fn y => f（f y）和foo = fn v => double（fn x => x + 1）v和goo = fn w => double Math.sqrt win（foo 3，goo 16.0）endJ.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5767SML类型报告：错误：运算符和操作数操作数：int -> int在表达式中：double（fn x => x +1）double、foo和goo的定义是相互递归的。 因此，在foo和goo的定义中，对double的调用是递归调用。因此，Hindley-Milner类型化的推导被这些递归调用中的每一个都是在不同类型的参数上的实现这个例子在系统HM下是不可打字的。然而，我们可以使用HM_R或S来类型化它。使用HM_R，我们可以为这个例子编写一个类型化派生，其中分配的最终类型是：double：双α。（α→α）→α→αfoo：int →intgoo：real →real。使用S，我们也可以输入这个例子。如果给double指定了以下交集类型：（（int→int）→int→int）（（real→real）→real →real）那么在foo的主体中对double的调用将能够使用交集类型的第一个组件，而在goo的主体中对double的调用将能够使用第二个组件。我们暂时不讨论S中的类型推导，直到下一个更复杂的例子。3.1.2旁白：SML/NJ vs. GHC顺便说一句，我们将本报告中的一些示例翻译为Haskell语法，并将SML/NJ错误消息与GHC错误消息进行比较（GHC 使用算法M，而SML/NJ使用算法W-更多讨论请参见[3]）。我们选择只翻译那些会产生有趣和不同的错误消息的例子。下面的大多数例子，在翻译时，输出的错误信息与SML/NJ错误信息非常相似，但偶尔在编译器作为问题目标的程序位置上这个例子，当翻译时，没有什么不同。IntFunc：：Int -> Int68J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57intFunc x = x +1doubleFunc：： Double -> DoubledoubleFunc x = sqrt xmyPair = let（double，foo，goo）=（\f -> \y -> f（f y），\v -> double intFunc v，\w-> double doubleFuncw）in（foo 3，goo 16.0）GHC类型报告：Couldn’t match ‘Double’ against ‘Int’Expected type: Int -> IntInferred type: Double ->在'double'的第一个参数SML/NJ和GHC编译器都检测到相同的错误，但SML/NJ分配类型：double：（real→real）→real→real，而GHC分配类型：double：（int → int）→ int → int。虽然这种差异不是很大，但它确实显示了两个编译器之间的操作3.1.3双-非耦合在上面的双重例子中出现的问题可以通过我们称之为“解耦”的技术来缓解。也就是说，我们利用Hindley-Milner let多态性，从相互递归定义中删除double，并将其定义为外部let。let val double = fn f => fn y => f（f y）在let val rec foo = fn v => double（fn x => x + 1）v中和goo = fn w => double Math.sqrt win（foo 3，goo 16.0）end endSML类型报告：J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5769没有错误3.2麦考夫3.2.1Mycroft -耦合下面是Alan Mycroft [15]发现的多态递归的典型例子。let valrec myMap = fnf => fnl =>if（null l）thenlelse cons（f（hdl））（myMapf（tl l））和sqList = fnl =>myMap（fn（x：int）=> x* x）l和compList = fnl =>myMap notlin（sqList [2，4]，compList [true，false]）endSML类型报告：错误：操作符和操作数操作数：int -> int在表达式中：myMap（fn x：int => x* x）和前面一样，我们有三个相互递归的函数定义和两个带有不同类型参数的递归调用。 这个例子，虽然在HM系统中是不可类型化的，但是可以在多态递归系统中使用交集类型或交集类型来类型化。要证明这一点，任何一个系统都必须能够处理列表。为了简洁起见，我们将考虑hd、tl、cons和nil都是我们语言中的原始常量。有了这些常量，我们将能够处理列表类型的表达式。此外，我们注意到表达式[1，2]和[true，false]只是语法糖，cons 1（cons 2 nil）和cons true（cons false nil）。我们现在可以在HM中指定以下类型：myMap：α. 是的（α→β）→α列表→β列表sqList：int list→int listcompList：bool list→bool list。70J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57使用S，我们可以分配以下rank-1类型：myMap：（（int→int）→int list→int list）（（bool→bool）→bool list→bool list）sqList：int list→int listcompList：bool list→bool list。在这两个系统中，分配给Mycroft示例的最终类型intlist × bool list。关于S下的完整类型推导，请参见附录A。3.2.2Mycroft -未耦合如前所述，解耦合是可能的。这在下面以稍微不同的形式显示。let val recmyMap =fn f=>fnl=>if（null l）thenlelse cons（f（hdl））（myMapf（tl l）） val rec sqList = fnl =>myMap（fn x =>x* x）lcompList =fnl=> myMap notlin（sqList [2，4]，compList [true，false]）endSML类型报告：没有错误3.3总计列表下面的例子找到了列表中元素的总和，但也将多态身份函数应用于过程中的每个元素和子列表。这里的想法是，我们可能想要记录关于每个元素及其对应的子列表的一些信息（可能通过副作用）。let val rec id = fn x => x和sumList = fnl =>if（nulll）then 0else（id（hdl））+（sumList（id（tll） in sumList [1，2，3] endSML类型报告：J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5771错误：运算符和操作数操作数：id（tll）我们使用HM对象指定以下类型：id：α.α→αsumList：int list →int。使用S，我们指定以下类型：id：（int→int）int（int list→int list）sumList：int list →int。这个例子的最终类型是：int。这个例子可以用与前两个例子相同的方式来在这一点上，一个自然的问题是问为什么id需要定义为相互递归到sumList 。 为 了 避 免 这 样 的 问 题 ， 我 们 可 以 将 id 作 为 参 数 传 递 给sumList，然后通过演示需要将两个不同的函数传递给sumList来激发这一举动。我们在矩阵转置的例子中展示了这一点，所以这里没有展示。3.4同晶组成本例使用复合函数作为多态递归函数。两个组合函数的顺序被切换并应用于不同的参数。然后比较两种应用程序的结果let val删除列表= fn x => [x] val删除列表= fnl => hdlval rec comp = fnf => fn g =>f o g和appComp = fn v1 => fn v2 =>(comp removeList removeList v1）=hd（压缩列表removeList v2）在appComp 5 [5]结束SML类型报告：错误：运算符和操作数operand：72J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57公司简介我们使用HM对象指定以下类型：int list：int→int listremoveList：int list →intcomp：α。是的你好（β→η）→（α→β）→α→ηappComp：int → int list → bool。使用S，我们指定以下类型：int list：int→int listremoveList：int list →intcomp：（（int→int list）→（int list→int）→int list→int list）int（（int list→int）→（int→int list）→int→int）appComp：int → int list → bool。在这两个系统中，分配给这个例子的最终类型是：bool。这个例子也可以是非耦合的。3.5埃塞尔山口这个例子与前面的例子非常相似，是由Simon Peyton Jones [6，7]提出的，他说这是一个他“真的想写”的程序。作者正在编写一个编译器传递，它使用了两种数据类型和三个以延续传递风格编写的函数。它以Haskell语法表示。data Exp = Let Bind Expdata Bind = MkBind String ExpdoBinds（b：bs）= doBindAndScope b（\bGHC类型报告：Couldn’t match ‘[Bind]’ against ‘Exp’Expected type:推断类型：Exp在应用程序'doBinds bs'中在'（：b'的第二个参数中J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5773这个程序的问题在于doExp和doBindAndScope是相互递归定义的。这意味着对doBindAndScope的调用是一个递归调用，不能是多态的。但是，doBinds和doExp都使用不同类型的参数调用doBindAndScope作者接着描述了一种缓解此问题的方法，方法是将多态封装在数据类型结构中，并向参数添加构造函数 关于dobindandscope然而，他指出，这个补丁不仅“晦涩难懂”，而且“在运行时也这个例子可以由HM或S键入。在HM系统中，我们可以指定以下类型：doBinds：绑定列表→绑定列表doExp：Exp →ExpdoBindAndScope：α。Bind→（Bind → α）→ α。在系统S下，我们可以指定这些类型：doBinds：绑定列表→绑定列表doExp：Exp →ExpdoBindAndScope：（绑定→（绑定→绑定列表）→绑定列表）（Bind→（Bind→Exp）→Exp）。除了已经讨论过的减轻这个例子的方法之外，我们还可以用通常的方法把这个程序解耦。3.6困惑3.6.1困惑-未缓解下面的例子不是很直观，但有一定的用途。let val rec f= fnn => fnx => fny =>如果x > y或n = 0，则n否则，如果n >= 100那么如果n 200那么nelse f（n div 2）（x *y）y elseif x y则f（n*n）0.03 1.0（n*n）n = 0在f3 5 6结束74J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）57SML类型报告：错误：运算符和操作数操作数：表达式中的int（f（n * n））1错误：运算符和操作数操作数：表达式中的int（f 3）5这个例子要求f的第二个和第三个参数是int和real类型。这个例子使用了重载的操作符>和 *，它们是为这两种类型定义的请注意，如果我们给f适当的类型，那么这个例子在HM和S中都是良好类型的。在HM中，我们指定以下类型：f：α。int→ α → α → int。在S下，我们指定以下类型：f：（int → int → int）（int → real → real → int）.在这两个系统中，分配给示例的最终类型是：int。这个例子与前面所有的例子都不同前面的例子都使用了一个多态函数，它被定义为相互递归到另一个函数。多态函数，然后使用两次的argu- ments不同类型。这个例子的目的是说明，可以定义一个多态递归函数，它本身就是这样，而不需要外部多态函数的帮助。因此，该示例难以缓解。在下一节中，我们将看到其他多态递归函数，它们具有相同的属性，但如果没有HM的推广和S.3.6.2旁白：SML/NJ vs. GHC值得注意的是，当转换成Haskell语法时，这个例子可以由GHC编译器类型化这是因为GHC编译器J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）5775将此示例中的整数转换为double并分配以下类型：f：double → double → double → double3.6.3困惑-缓解我们可以通过重复来减轻这个例子考虑以下方案。let val rec f1= fn n=> fnx => fny =>如果x > y或n = 0，则n否则，如果n >= 100那么如果n 200那么nelse f1（n div 2）（x * y）yelseif x y则f2（n*n）0.03 1.0否则f1（n*n）1 1和f2 = fn n => fn x => fn y =>如果x > y或n = 0，则n否则，如果n >= 100那么如果n 200那么nelse f2（n div 2）（x * y）y elseif x y则f2（n*n）0.03 1.0f1（n*n）= 0在f1 3 5 6结束这个程序现在可以在HM下打印。 我们可以指定以下类型：f1：int→int→intf2：int → real → real → int。然而，以这种方式减轻示例与之前的所有尝试不同，因为我们必须复制整个程序。由于复制破坏了多态性的目的，因此不推荐这种改变76J.J. Hallett，A.J.Kfoury/Electronic Notes in Theoretical Computer Science 136（2005）574仅可在S中键入4.1矩阵转置4.1.1矩阵转置-未缓解这个例子展示了矩阵转置运算的简洁而优雅的公式let valmap 1 = mapval recmap2 = fnf => fnl =>if（null l）thennilelseif（null（hdl））thennilelsecons（fhd l）（map2f（f tll））inmap2 map1 [[1，2]，[3，4]]endSML类型报告：错误：运算符和操作数操作数：f tl与前面的示例不同，此示例不能通过使用hint- t类型的polymor-phicrecursion来键入。 这个问题是在试图将第一个参数映射到2，f时出现的。要看到这一点，我们只需要看看else分支，嵌套if表达式。注意，从cons（fhdl）（map2f（f tl））中，f的第一次出现的类型必须是以下形式：f：（α list → α）→ α list list → α list。然而，f的第二次出现需要以下形式：f：（αlist→αlist）→αlist list→αlist list。我们，我们有多晶型。 然而，由于新的严格条件仅限于类型的最外部分，因此映射2的严格类型是不可能的。