Correct form of letrec in Hindley

 

I'm having trouble understanding the letrec definition for HM system that is given on Wikipedia, here: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

For me, the rule translates roughly to the following algorithm:

  • infer types on everything in the letrec definition part
  • assign temporary type variables to each defined identifier
  • recursively process all definitions with temporary types
  • in pairs, unify the results with the original temporary variables
  • close (with forall ) the inferred types, add them to the basis (context) and infer types of the expression part with it

    • I'm having trouble with a program like this: 

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

    The behavior I'm observing is as follows:

  • definition of p gets temporary type a
  • definition of x gets some temporary type too, but that's out of our scope now
  • in x , definition of test gets a temporary type t
  • p gets the temporary type a from the scope, using the HM rule for a variable
  • (f 5) gets processed by HM rule for application, resulting type is b (and the unification that ( a unifies with Uint -> b )
  • ((p 5) 5) gets processed by the same rule, resulting in more unifications and type c , a now in result unifies with Uint -> Uint -> c
  • now, test gets closed to type forall cc
  • variable test of in test gets the type instance (or forall cc ) with fresh variables, accrodingly to the HM rule for variable, resulting in test :: d (that is unified with test::t right on)
  • resulting x has effectively type d (or t , depending on the mood of unification)

    • The problem: x should obviously have type Uint , but I see no way those two could ever unify to produce the type. There is a loss of information when the type of test gets closed and instance'd again that I'm not sure how to overcome or connect with substitutions/unifications.

    Any idea how the algorithm should be corrected to produce x::Uint typing correctly? Or is this a property of HM system and it simply will not type such case (which I doubt)?

    Note that this would be perfectly OK with standard let , but I didn't want to obfuscate the example with recursive definitions that can't be handled by let .

    Thanks in advance

    Answering my own question:

    The definition on the Wiki is wrong, although it works to certain extent at least for type checking.

    Most simple and correct way to add recursion to HM system is to use fix predicate, with definition fix f = f (fix f) and type forall a. (a->a) -> a forall a. (a->a) -> a . Mutual recursion is handled by double fixpoint, etc.

    Haskell approach to the problem (described at https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b#binding-groups ) is (roughly) to derive an incomplete type for all functions and then run the derivation again to check them against each other.

    链接地址: http://www.djcxy.com/p/14202.html

    上一篇: “让我们在欣德利进行推理

    下一篇: 在Hindley的letrec的正确形式