15
$\begingroup$

What's a good approach for extending Hindley Milner with mutual recursion without de-sugaring to let+fix+records? My thinking is (assuming no polymorphic recursion)

  1. Collect mutually recursive lets together in a group.
  2. Add their bindings to an environment with fresh monotype type variables.
  3. Infer right-hand-side of let bindings, and if one of the bindings in the group is referenced, it just looks up the monotype typevar from the environment.
  4. After all bindings in the group have been checked, generalize the monotype typevars to polytypes, and replace the type in the environment.

Is this generalization sound?

$\endgroup$
1
  • $\begingroup$ Just adding to the question (cannot comment yet) with: what would change if polymorphic recursion is possible? For example, how would one typecheck these two? composeB :: (Bool -> Bool) -> (Bool -> Bool) -> Bool -> Bool composeB = compose compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c compose f g x = f (g x) And verify that the first is well-typed, without having the second one's scheme in the context? (Or presenting an error if for example the declared type for composeB was a stupid forall a. (Bool -> Bool) -> (Bool -> Bool) -> Bool -> a) $\endgroup$
    – Damax
    Commented May 21 at 21:35

1 Answer 1

Reset to default
3
$\begingroup$

Yes, and this is essentially what OCaml does, actually.

$\endgroup$
2
  • 2
    $\begingroup$ I don't doubt you, but do you have a reference for this? $\endgroup$
    – cody
    Commented May 1 at 19:21
  • $\begingroup$ Unfortunately, not at hand. I can probably pinpoint the part of the implementation in typecore.ml, but that will take me some time... $\endgroup$
    – xuq01
    Commented May 2 at 17:13

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .