<p>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)</p>
<ol>
<li>Collect mutually recursive lets together in a group.</li>
<li>Add their bindings to an environment with fresh monotype type variables.</li>
<li>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.</li>
<li>After all bindings in the group have been checked, generalize the monotype typevars to polytypes, and replace the type in the environment.</li>
</ol>
<p>Is this generalization sound?</p>

<type-checker><recursion><type-inference>
Extending Hindley Milner with (mutual) recursion
CC BY-SA 4.0
2024-05-21T21:35:53.940Z
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`)
Damax
<p>Yes, and this is essentially what OCaml does, actually.</p>

CC BY-SA 4.0
2024-05-01T11:20:49.920Z
2024-05-01T11:20:49.920Z
xuq01
CC BY-SA 4.0
2024-05-01T19:21:12.853Z
I don't doubt you, but do you have a reference for this?
cody
CC BY-SA 4.0
2024-05-02T17:13:09.063Z
Unfortunately, not at hand. I can probably pinpoint the part of the implementation in typecore.ml, but that will take me some time...
xuq01
# Extending Hindley Milner with (mutual) recursion
Posted by: username_0 on 2023-09-10
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?
**Tags:** type-checker recursion type-inference
> **Comments:**
> **username_1**: 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`)  
---
## 1 answers
### Answer by username_2 on 2024-05-01. Score: 3
Yes, and this is essentially what OCaml does, actually.
> **Comments:**
> **username_3** (2024-05-01): I don't doubt you, but do you have a reference for this?  
> **username_2** (2024-05-02): Unfortunately, not at hand. I can probably pinpoint the part of the implementation in typecore.ml, but that will take me some time...  
---
