标签: hindley-milner

我想使用该unification-fd软件包为Hindley-Milner类型系统实现一个简单的类型检查器.这需要表示多态("forall")类型.

表示这些类型的最佳方式是什么？提供的变量unification-fd,即在UVar东西,是统一的(元)变量,而不是在对象语言的变量.我考虑过的一些可能性:

1. 将类型变量的构造函数添加到表示类型的基本仿函数:

   data TyF tcon tv a
       = TCon tcon [a]
       | TVar tv
   

   Run Code Online (Sandbox Code Playgroud)

   与zipMatch 只有统一平等TVar秒.类型实例化始终UTerm (TVar a)用a 替换每个freeVar.

2. (Ab)将UVars用于类型变量,并freeVar在实例化时用s 替换它们.需要跟踪普遍性与存在性,UVar以了解要替换哪些.

3. 退出TVar,在类型检查期间TyF单独使用单一UTerm (TyF tcon) IntVar类型,UTerm (TyF tcon) tv从外部可见的多态类型,以及UTerm (TyF tcon) (Either tv IntVar)在中间,let绑定变量的类型检查期间.

哪个最好？还有其他一些我没有想过的方法吗？

下面是几个简单的函数：

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

所有的f1，f2以及f3能够接受()为输入。另一方面，当然f4不能接受()；f4 ()是类型错误。

是否有可能TYPE-理论上刻画了什么f1，f2以及f3有什么共同点？具体而言，是有可能定义一个acceptsUnit函数，以使得acceptsUnit f1，acceptsUnit f2和acceptsUnit f3是公类型的，但acceptsUnit f4是一种类型的错误-和不具有其他的效果？

下面完成了部分工作，但将其输入单态化（在 Haskell …

有人可以在下面的F#程序中解释一步一步的类型推断:

let rec sumList lst =
    match lst with
    | [] -> 0
    | hd :: tl -> hd + sumList tl

我特别希望逐步了解Hindley Milner的统一过程是如何运作的.

根据'什么是Hindley Milner',它说:

Hindley-Milner是System F的限制,它允许更多类型但需要程序员注释.

我的问题是,什么是系统F中可用的类型的例子,在Hindley Milner(类型推断)中不可用？

(假设系统F类型的推断已被证明是不可判定的)

我试图在Haskell中编写关系问题的代码,当时我必须发现以类型安全的方式执行此操作远非显而易见.比如谦虚

select 1,a,b, from T

已经提出了一些问题:

• 这个功能的类型是什么？
• 什么是投影的类型1,a,b？一般来说投影的类型是什么？
• 什么是结果类型,我如何表达结果类型和投影之间的关系？
• 接受任何有效投影的这种函数的类型是什么？
• 如何在编译时检测无效的投影？
• 如何在表格或投影中添加列？

我相信即使是Oracle的PL/SQL语言也没有这么做.虽然invald投影主要在编译时检测到,但是大量的类型错误仅在运行时显示.大多数其他绑定到RDBMS(例如Java的jdbc和perl的DBI)使用字符串中包含的SQL,因此完全放弃了类型安全性.

进一步的研究表明,有一些Haskell库(HList,乙烯基和TRex),它们提供类型安全的可扩展记录等等.但是这些库都需要Haskell扩展,如DataKinds,FlexibleContexts等等.此外,这些库不易使用,并且有一种诡计的气味,至少对于像我这样的未初始化的观察者来说.

这表明,类型安全的关系操作不能很好地适应功能范例,至少不像在Haskell中实现的那样.

我的问题如下:

• 以类型安全的方式对关系操作建模这种困难的根本原因是什么.Hindley-Milner在哪里落空？或者问题是否源于已键入的lambda演算？
• 是否有范式,关系操作是一等公民？如果是这样,是否有真实的实施？

在Haskell中,我们可以编写以下数据类型:

data Fix f = Fix { unFix :: f (Fix f) }

类型变量f具有种类* -> *(即它是未知类型的构造函数).因此,Fix有那种(* -> *) -> *.我想知道Fix在Hindley Milner类型系统中是否是一个有效的类型构造函数.

从我在维基百科上看到的内容来看,它似乎Fix不是Hindley Milner类型系统中的有效类型构造函数,因为HM中的所有类型变量必须是具体的(即必须具有类型*).确实如此吗？如果HM中的类型变量并不总是具体,那么HM会变得不可判断吗？

runST是一个Haskell函数,它通过类型静态地约束资源的可用生命周期.为此,它使用rank-2多态性.标准ML的简单类型系统仅提供秩-1多态性.

标准ML是否仍然可以使用类型将资源的生命周期约束到类似的最终结果？

此页面和此页面演示了一些重构代码的方法,只需要更简单的类型.如果我理解正确,核心是将表达式包装起来,以便它被上下文中可能的观察所取代,这些观察是有限的.这种技术一般吗？可以将它,或相关编码,具有一些可使用像(显然在签名不相同)runST,以防止从被包裹的表达逸出值的类型被观察？如果是这样,怎么样？

我想象的场景是这样的:

magicRunSTLikeThing (fn resource =>
    (* do things with resource *)
    (* return a value that most definitely doesn't contain resource *)
)

...其中magic...提供了用户提供的代码无法以任何方式共享的资源.显然,这样一个简单的界面具有单个库函数是不可能的,但也许有各种层次的包装和手工内联和提取......？

我已经看到了这一点,但如果我理解正确(...很可能不是),那实际上并不会阻止对资源的所有引用进行共享,只能确保对它的一个引用必须"关闭".

基本上我想在SML中实现安全类型的显式(非推断的MLKit样式)区域.

我公开了一个带有两个参数的函数,一个是最小边界,另一个是最大边界.如何使用类型确保例如最小边界不大于最大边界？

我想避免创建一个智能构造函数并返回一个Maybe,因为它会使整个使用更麻烦.

谢谢

根据Haskell 2010语言报告,其类型检查器基于Hindley-Milner.所以考虑f这种类型的功能,

f :: forall a. [a] -> Int

例如,它可以是长度函数.根据Hindley-Milner的说法,f []键入检查Int.我们可以通过实例的类型证明这一点f来[Int] -> Int,和类型[]来[Int],然后得出结论,应用([Int] -> Int) [Int]的类型的Int.

在这个证明中,我选择实例化类型forall a. [a] -> Int并forall a. [a]替换Int为a.我可以替代Bool,证明也可以.在Hindley-Milner中,我们可以将多态类型应用于另一个,而不指定我们使用的实例,这不奇怪吗？

更具体地说,Haskell中的什么阻止我a在实现中使用类型f？我可以想象这f是一个等于18任何的函数[Bool],并且等于所有其他类型列表上的通常长度函数.在这种情况下,会f []是18或0？Haskell报告称"内核未正式指定",因此很难说.

在显式类型注释的情况下,Haskell检查推断类型是否至少与其签名一样多态,或者换句话说,推断类型是否是显式类型的子类型.因此,以下功能是错误的:

foo :: a -> b
foo x = x

bar :: (a -> b) -> a -> c
bar f x = f x

然而,在我的场景中,我只有一个函数签名,需要验证它是否被潜在的实现"居住" - 希望这个解释完全有意义!

由于parametricity财产我认为两者foo并bar没有不存在的实现,因此,两者都应该被拒绝.但我不知道如何以编程方式结束.

目标是整理所有或至少一部分无效类型签名,如上所述.我很感激每一个提示.