标签: hindley-milner

当元编程时,传递Haskell的类型系统信息可能是有用的(或必要的),这些信息是关于程序已知但在Hindley-Milner中不可推断的类型.是否有一个库(或语言扩展等)提供了执行此操作的工具 - 即Haskell中的编程类型注释？

考虑一种情况,即您正在使用异构列表(使用Data.Dynamic库或存在量化实现,比如说),并且您希望将列表过滤到沼泽标准,同质类型的Haskell列表.你可以写一个像这样的函数

import Data.Dynamic
import Data.Typeable

dynListToList :: (Typeable a) => [Dynamic] -> [a]
dynListToList = (map fromJust) . (filter isJust) . (map fromDynamic)

并使用手动类型注释调用它.例如,

foo :: [Int]
foo = dynListToList [ toDyn (1 :: Int)
                    , toDyn (2 :: Int)
                    , toDyn ("foo" :: String) ]

这foo是清单[1, 2] :: [Int]; 这很好,你回到了坚实的基础,Haskell的类型系统可以做到这一点.

现在想象你想要做同样的事情,但是(a)当你编写代码时,你不知道调用产生的列表类型是什么dynListToList,但是(b)你的程序确实包含只有(c)它不是类型系统可访问的形式.

例如,假设您从异类列表中随机选择了一个项目,并且希望按该类型过滤列表.使用提供的类型检查工具Data.Typeable,您的程序具有执行此操作所需的所有信息,但据我所知 - 这是问题的本质 - 没有办法将其传递给类型系统.这是一些伪Haskell,它显示了我的意思:

import Data.Dynamic
import Data.Typeable

randList :: (Typeable a) …

在C++中是否有Damas-Hindley-Milner样式推断的实现,最好使用现代C++技术？

Hindley-Milner是一种类型系统,是许多众所周知的函数式编程语言的类型系统的基础.Damas-Milner是一种在Hindley-Milner型系统中推断(推导？)类型的算法.

维基百科给出了算法的描述,据我所知,该算法相当于一个单词:"统一".这就是它的全部吗？如果是这样,那意味着有趣的部分是类型系统本身而不是类型推理系统.

如果Damas-Milner不仅仅是统一,我想要一个Damas-Milner的描述,其中包括一个简单的例子,理想情况下是一些代码.

此外,该算法通常被称为类型推断.它真的是一个推理系统吗？我认为这只是推断出类型.

相关问题:

• 什么是Hindley Miller？
• 键入对统一问题的推断

我正在研究一个用Java编写的基于数据流的简单系统(想象它就像一个LabView编辑器/运行时).用户可以在编辑器中将块连接在一起,我需要类型推断以确保数据流图是正确的,但是,大多数类型推断示例都是用数学符号,ML,Scala,Perl等编写的,我不会"说" ".

我看了一下辛德米尔纳算法,发现这个文件有一个很好的例子,我可以实现.它适用于一组T1 = T2之类的约束.但是,我的数据流图转换为T1> = T2,就像约束一样(或T2延伸T1,或协方差,或T1 <:T2,正如我在各篇文章中看到的那样).没有lambdas只是类型变量(在通用函数中使用T merge(T in1, T in2))和具体类型.

回顾一下HM算法:

Type = {TypeVariable, ConcreteType}
TypeRelation = {LeftType, RightType}
Substitution = {OldType, NewType}
TypeRelations = set of TypeRelation
Substitutions = set of Substitution

1) Initialize TypeRelations to the constraints, Initialize Substitutions to empty
2) Take a TypeRelation
3) If LeftType and RightType are both TypeVariables or are concrete 
      types with LeftType <: RightType Then do nothing
4) If only LeftType is a TypeVariable Then …

我无法理解维基百科上给出的HM系统的letrec定义,这里:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

对我来说,规则大致转换为以下算法:

1. 推断letrec定义部分中 所有内容的类型
   1. 为每个定义的标识符分配临时类型变量
   2. 使用临时类型递归处理所有定义
   3. 成对,将结果与原始临时变量统一起来
2. close(with forall)推断类型,将它们添加到基础(context)并用它推断表达式部分的类型

我遇到这样的程序有问题:

letrec
 p = (+)     --has type Uint -> Uint -> Uint
 x = (letrec
       test = p 5 5
     in test)
in x

我观察的行为如下:

• p获取临时类型的定义a
• x获取一些临时类型的定义,但现在超出了我们的范围
• in x,test获取临时类型的定义t
• pa从范围中获取临时类型,使用HM规则作为变量
• (f 5)得到由HM规则应用,造成类型是处理b(以及(统一a与结合Uint -> b)
• ((p 5) 5)由同一规则处理,导致更多的统一和类型c,a现在结果统一Uint -> Uint -> c
• 现在,测试关闭以输入 forall …

我需要一种(快速和脏的)方法来获得一个以字符串形式给出的Haskell表达式的表示.

我目前看到3个选项:

• 使用GHC API - 然而,文档很快就失去了我.
• 使用其他类型的推理工具 - 我曾被建议尝试haskell-type-exts,但它无法输入除了最简单的表达式之外的所有内容.我不知道任何其他这样的工具.
• 滚动我自己的HM推理员 - 除非绝对必要,否则我会避免这种情况

我甚至不需要一个完整的解决方案,因为可以输入一个合理的Haskell基本子集的库/工具就足够了.

那么实现这一目标的最简单方法是什么？

Haskell类型系统(*)的一个有趣特性是,有时你可以根据它的类型签名确定函数的确切功能(假设没有unsafe IO黑暗魔法被激活).

例如,具有类型签名的任何函数a -> a必须是标识函数,并且任何类型的函数(a,b) -> a都等效于fst.在某些情况下,您无法完全确定函数:类型中存在无数个不同的可能函数a -> Int,但它们都是常量 - 它们都忽略第一个参数.

我发现这个属性很吸引人,但我怀疑它只适用于"琐碎"的功能,如id和const.我对么？

此外,我在这里的推理仅基于直觉 - 例如,在a -> a我们中"不知道" a(与受约束的函数相反Num a => a -> a),因此除了不变地返回之外,"不能做任何事情".有没有正式的方法来处理这种扣除？

_{*我知道Haskell的类型系统是基于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绑定变量的类型检查期间.

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

如果我正确理解Haskell中的ST monad,则以runST巧妙的方式使用rank-2类型,以确保计算在转义monad时不引用任何其他线程.

我有一个带有Hindley-Milner类型系统的玩具语言,我的问题如下:是否可以扩展HM类型系统,使用ad-hoc规则键入runST应用程序,以便ST monad可以安全地逃避,而不会引入排名-2种类型？

更确切地说,runST将具有类型forall s a. ST s a -> a(即rank-1)并且输入规则将首先尝试以与在let-expression中概括类型的方式相同的方式来推广计算类型,但是如果s发现类型变量被绑定则引发类型错误.

上面只限制了接受的程序与香草HM相比,所以看起来很合理,但我不确定.这会有用吗？

下面是几个简单的函数：

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 …