标签: hindley-milner

PyPy 是否在编译时进行静态类型检查以在编译时捕获类型错误？如果没有，HM 类型推断之类的东西是否有助于在编译时捕获这些错误？

我有两个用于控制循环的函数,continue并且break:

type Control a = (a -> a) -> a -> a

continue :: Control a
continue = id

break :: Control a
break = const id

然后,我想简化Control类型同义词.因此,我写道:

type Endo a = a -> a

type Control a = Endo (Endo a)

continue :: Control a
continue = id

break :: Control a
break = const id

但是,当我试图进一步简化它时,我收到一个错误:

GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
Prelude> type Endo a = a -> a
Prelude> …

我有一个参数化类型,递归地使用自己但具有专门的类型参数,当我实现泛型运算符时,由于处理专用子树的情况,该运算符的类型绑定得太紧.第一个代码示例显示了问题,第二个示例显示了我不想使用的解决方法,因为实际代码有更多的情况,因此以这种方式复制代码是一种维护危险.

这是一个显示问题的最小测试用例:

module Op1 = struct
  type 'a t = A | B  (* 'a is unused but it and the _ below satisfy a sig *)

  let map _ x = match x with
    | A -> A
    | B -> B
end

module type SIG = sig
  type ('a, 'b) t =
    | Leaf  of 'a * 'b
    (* Here a generic ('a, 'b) t contains a specialized ('a, 'a Op1.t) t. *)
    | Inner of 'a * …

所以我只最近遇到一个玩具容量的阿卡之外,我不禁注意到它和OTP尽管Scala的静态类型的一般优先股动态类型.我开始挖掘一下,并且遇到了这篇描述HM型系统而非erlang进程间通信的Wadler论文.也就是说,SO的这个问题的答案是指Wadler和Marlow未能提供他们对过程类型通信的草图.作为参考,我对这样的代码感到非常失望:

def receive = {
    case "test" => log.info("received test")
    case _ => log.info("received unknown message")
  }

我知道在实践中,透析器可以提供真实类型系统的大量好处,但为什么创建静态验证的演员系统这么困难呢？当我们使用类型系统时,我们是倾向于编写Future或Observable/ Iteratee库,或者是Channel编程的IO而不是演员系统,还是Wadler和Marlow错过了技术难度？

考虑以下程序(在Haskell中,但可以是任何HM推断语言):

x = []
y = x!!0

使用HM(或运行编译器),我们推断:

x :: forall t. [t]
y :: forall a. a

我理解这是如何发生的,通过通常的泛化/实例化规则,但我不确定是否有可能有这样的东西forall a. a.

一个问题是:由于我们在这里有一个越界访问,人们可以排除该程序作为一个有效的例子.相反,我们可以说我们推断的通用类型是程序中出错的标志吗？如果是的话,我们是否可以使用这个"事实"故意在其他情况下无效检查无效程序？

下一个程序甚至可以获得更奇怪的类型:

c = []
d = (c!!0) + (1 :: Int)

推断类型:

c :: forall t. [t]
d :: Int

......虽然d是从中抽出来的c!

我们可以在没有排除有效程序的情况下增强HM在这里做得更好吗？

编辑:我怀疑ed这是使用部分函数的工件(!!0在这种情况下).但请看:

c = []
d = case c of [] -> 0; (x:_) -> x + (1 :: Int)

现在没有使用部分功能.然而,c :: forall t. [t] …

GHC说我的功能过于笼统,不能作为论据传递.

这是一个重现错误的简化版本:

data Action m a = SomeAction (m a)


runAction :: Action m a -> m a
runAction (SomeAction ma) =  ma

-- Errors in here
actionFile :: (Action IO a -> IO a) -> String -> IO ()
actionFile actionFunc fileName = do
    actionFunc $ SomeAction $ readFile fileName
    actionFunc $ SomeAction $ putStrLn fileName


main :: IO ()
main =
    actionFile runAction "Some Name.txt"

这就是错误所说的:

 • Couldn't match type ‘a’ with ‘()’
      ‘a’ is a rigid type …

我正在尝试在Haskell中执行函数组合,我不确定哪个运算符是正确的运算符.

文档包含这两种类型的签名:

(.) :: (b -> c) -> (a -> b) -> a -> c 
(<<<) :: Category cat => cat b c -> cat a b -> cat a c 

显然,这两个选项之间的区别在于是否存在Category cat,但是这个注释表示什么,以及我应该如何使用这些信息来选择一个运算符而不是另一个？

在比较其他两个运算符时,我还注意到上述两个签名的第三个变体:

(>>) :: forall a b. m a -> m b -> m b 
(>>>) :: Category cat => cat a b -> cat b c -> cat a c

forall注释意味着什么- >>用于第三种情况？

抽象语法树中存在哪些类型信息？如何使用 AST 进行类型推断？我不明白当没有节点指示具体类型时，如何在给定 AST 的情况下导出类型输入和输出。类型是仅从树结构推断出来的吗？例如有一堆IfStatement(Statement)，所以它可能会返回一个 bool ？例如，javalang python 模块使用以下 AST 节点：

CompilationUnit(Node)
Import(Node)
Documented(Node)
Declaration(Node)
Type(Node)
TypeArgument(Node)
TypeParameter(Node)
Annotation(Node)
ElementValuePair(Node)
ElementArrayValue(Node)
ArrayInitializer(Node)
VariableDeclarator(Node)
InferredFormalParameter(Node)
Statement(Node)
SwitchStatementCase(Node)
ForControl(Node)
EnhancedForControl(Node)
Expression(Node)
EnumBody(Node)
VariableDeclaration(Declaration)
FormalParameter(Declaration)
TryResource(Declaration)
CatchClauseParameter(Declaration)
AnnotationMethod(Declaration)
BasicType(Type)
ReferenceType(Type)
TypeDeclaration(Declaration, Documented)
PackageDeclaration(Declaration, Documented)
ConstructorDeclaration(Declaration, Documented)
EnumConstantDeclaration(Declaration, Documented)
ClassDeclaration(TypeDeclaration)
EnumDeclaration(TypeDeclaration)
InterfaceDeclaration(TypeDeclaration)
AnnotationDeclaration(TypeDeclaration)
Member(Documented)
MethodDeclaration(Member, Declaration)
FieldDeclaration(Member, Declaration)
ConstantDeclaration(FieldDeclaration)
LocalVariableDeclaration(VariableDeclaration)
IfStatement(Statement)
WhileStatement(Statement)
DoStatement(Statement)
ForStatement(Statement)
AssertStatement(Statement)
BreakStatement(Statement)
ContinueStatement(Statement)
ReturnStatement(Statement)
ThrowStatement(Statement)
SynchronizedStatement(Statement)
TryStatement(Statement)
SwitchStatement(Statement)
BlockStatement(Statement)
StatementExpression(Statement)
CatchClause(Statement)
Assignment(Expression)
TernaryExpression(Expression)
BinaryOperation(Expression)
Cast(Expression)
MethodReference(Expression)
LambdaExpression(Expression)
Primary(Expression) …

我试图通过在我经常使用的语言Clojure中实现算法W来自学Hindley-Milner类型推断.我遇到了let推理的问题,我不确定我做错了什么,或者我期望的结果是否需要算法以外的东西.

基本上,使用Haskell表示法,如果我尝试推断它的类型:

\a -> let b = a in b + 1

我明白了:

Num a => t -> a

但我应该得到这个:

Num a => a -> a

同样,我实际上是在Clojure中这样做,但我不相信问题是Clojure特有的,所以我使用Haskell表示法使它更清晰.当我在Haskell中尝试它时,我得到了预期的结果.

无论如何,我可以通过将每个let转换为函数应用程序来解决该特定问题,例如:

 \a -> (\b -> b + 1) a

但后来我失去了let多态性.由于我对HM没有任何先验知识,我的问题是我是否在这里遗漏了一些东西,或者这只是算法的工作方式.

编辑

如果有人有类似的问题,并想知道我是如何解决它的,那我就是按照Algorith W Step by Step进行操作.在第2页的底部,它说"将Types方法扩展到列表有时会很有用".因为它对我来说听起来不是强制性的,所以我决定跳过那部分并稍后重新审视.

然后我将ftv函数TypeEnv直接翻译成Clojure,如下所示:(ftv (vals env)).由于我已经实现ftv了一个cond表单并且没有seqs 的子句,所以它只是返回nil了(vals env).这当然正是静态类型系统设计要捕获的那种错误!无论如何,我刚刚重新定义了ftv与env地图有关的条款,(reduce set/union …

以下对 compose 函数的 Hindley-Milner 类型签名的尝试是否正确？

// compose :: (f -> [f]) -> (f -> f -> f) -> [f] -> f
const compose = (...fns) => fns.reduce((f,g) => (...args) => f(g(...args)));

我想了解有关类型推断的规则，因为我希望将其纳入自己的语言中，并且本着这种精神，我一直在研究F＃的类型推断，以下让我感到奇怪。

这将进行编译，并且id为'a -> 'a，（如果我没有记错的话）表示每个调用都使用“新鲜”类型。

let id x = x

let id1 = id 1
let id2 = id "two"

但是，当使用运算符时，似乎是第一次调用确定了该函数的签名。

在这里，mul据报道是int -> int -> int

let mul x y = x * y

let mul1 = mul 1 2
let mul2 = mul 1.1 2.2 // fails here

如果我重新排序，mul则为float -> float -> float：

let mul x y = x * y

let mul2 = mul 1.1 2.2
let mul1 …

有人可以解释一下如何理解这个符号：

((a, b) \xe2\x86\x92 a) \xe2\x86\x92 a \xe2\x86\x92 [b] \xe2\x86\x92 a\n

请参阅： https: //ramdajs.com/docs/#reduce