<p>I'd like to create a type system similar to the one in Swift or Kotlin, where you have top-level functions that declare their parameters and return types, but you have some type inference with local variables and closures. For example, consider this code, which I hope is mostly self-explanatory since it uses typical syntax:</p>
<pre><code>var nums: Array&lt;Int&gt; = [10,20,30,40]
var strs = nums.map { n → foo(n) }
var s = strs[0]
fun foo(i: Int) → String {
    return &quot;i = $i&quot;
} 
</code></pre>
<p>That syntax after the <code>nums.map</code> call is a closure. (Forget that it's probably better to pass <code>foo</code> directly.) The signature of <code>Array&lt;T&gt;.map</code> is probably something like:</p>
<pre><code>class Array&lt;T&gt; {
    fun map(f: T -&gt; U) -&gt; Array&lt;U&gt;
    ...
}
</code></pre>
<p>I'd want the type checker to derive that <code>n</code> is an <code>Int</code>, that the closure is <code>Int -&gt; String</code>, that <code>strs</code> is <code>Array&lt;String&gt;</code>, and <code>s</code> is <code>String</code>.</p>
<p>I've been reading about <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)" rel="noreferrer">unification</a>, which seems like the general purpose way of solving this problem, but it seems like it might be overkill here, because it was originally used for languages where you didn't have to specify the types anywhere and the inference algorithm needed to do more.</p>
<p>Should I learn how to implement unification, or is there a lighter weight algorithm that would be better for this style of language?</p>

<type-checker><type-inference>
Is a unification algorithm overkill for local type inference?
CC BY-SA 4.0
2023-10-13T08:39:17.507Z
Unification is simple. My go to method for implementing all kinds of type systems is to have a simple pass that generate a system of type equations (for whatever typing rules you invented), and then another pass converting the rules into Prolog code. If you have even a simple embedded Prolog implementation inside your compiler (and you should - it can do a lot of heavy lifting for you), this two tiny passes solve all your typing problems in no time.
SK-logic
CC BY-SA 4.0
2023-10-13T13:32:26.063Z
@SK-logic Did you implement a kind of Prolog-inspired logic engine yourself, or did you download a reusable library with Prolog in it?
Rob N
CC BY-SA 4.0
2023-10-13T13:58:59.097Z
I implemented Prolog myself, and then I was reusing it over and over for many different things. Here is an example of a small interpreted Prolog: https://github.com/combinatorylogic/mbase/blob/master/src/l/ext/rules.al
SK-logic
CC BY-SA 4.0
2023-10-13T18:57:46.477Z
Another unification algorithm using triangular substitution is common to miniKanrens, and an explanation of how to implement it is [Hemann & Friedman 2013](http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf). I've implemented this algorithm in [Monte](https://github.com/monte-language/typhon/blob/master/mast/lib/logji.mt) and in [RPython](https://osdn.net/users/corbin/pf/cammy/scm/blobs/master/sampler/cammylib/types.py); that latter example was just for doing type inference.
Corbin
<p>Tyr uses a type inference strategy that is likely very close to what you have in mind. I call it single level return type inference. What happens is that overload resolution gets an expected return type and all the argument types and does inference based on that. If you make a decision, you cannot change it. All global entities have defined parameter types, but may infer return types based on their definitions.</p>
<p>Now, regarding your question, you will need to do something like unification if you want to allow recursive signatures, i.e. ones where a parameter's type uses another parameter. For <a href="https://github.com/tyr-lang/stdlib/blob/a77849fbf2db09716d7f96fad071c810df8224ab/lang/src/eqr.tyr#L52" rel="nofollow noreferrer">example</a> operations on equivalence relations
take the underlying type and a function doing the equivalence check to derive == and != operators. Last time I checked, such definitions wouldn't be allowed in Go. The reason is that even type checking an application requires to do some sort of unification. TBH, I cannot tell the relation to HM.</p>
<p>However, the current binder parameter <a href="https://github.com/tyr-lang/test.conformance/blob/90d6bc84d2a5e8b73468057ec949054ff4b3f886/0.6.0/accept/bufferedIterator/mar.tyr#L20" rel="nofollow noreferrer">inference</a>, which is type-checking wise likely identical to inference of local lambdas, is currently not based on unification. I haven't yet encountered an example where this would be required and, TBH, cannot tell if it would break my &quot;single level&quot; rule. That rule is required to provide somewhat understandable error messages. In essence, it allows creating an error location that is almost always useful.</p>

CC BY-SA 4.0
2023-10-15T07:36:25.957Z
2023-10-15T07:36:25.957Z
feldentm
<p>tl;dr: Yes, you want unification. The question I think you should consider is &quot;How are you going to use it?&quot;</p>
<p>The fun part about unification is that it's very applicable.
Some variant of unification is going to ultimately be the thing you end up implementing, because it's the best tool for the task you're trying to solve - whether you need fully fledged Hindley-Milner/HM inference or not. (which is what I believe is what you're referring to with &quot;because it was originally used for languages where you didn't have to specify the types anywhere&quot; - unification is an algorithm, HM is another algorithm that utilizes unification for full-program type synthesis)</p>
<p>While HM may not be applicable to your ultimate solution in it's entirety, it does seem like a variant of it would be able to do what you want, for example, within the scope of a single function. This is what Rust does, if I recall correctly - You must provide types in various locations, but within the body of a function, it can deduce types through something very similar to HM.</p>
<p>Overall, I would recommend reading up on HM and an implementation of it, like algorithm J, and then consider how that might be applicable within the body of a function. (A hint: it'll be considerably simpler, because the complex part is function type inference, and you don't need that at all if I understand correctly)</p>
<p>Depending on your language, it might be as simple as assigning each unknown type a unifiable reference (commonly referred to as a metavariable in the literature, I believe) as a placeholder for it's type, and then unifying that reference with the real type when something like <code>print_string(s)</code> is found. Then, at the end of a scope of a function, you make sure no variable have an unknown type.</p>
<p>This means you might end up with something like:</p>
<pre><code>let a = []; // type of a is `List $metavariable_0`
a.push(1); // unify `$metavariable_0` with `int`
// now a's type is `List int`
</code></pre>
<p>You'll note how that would work across the whole function with minimal issues due to the use of mutable references - when you change it once inside the unification function, it'll be changed everywhere, so you'll catch any sort of nasty type errors like</p>
<pre><code>let a = [];  // type of a is `List $meta0`
a.push(1) // unify `$meta0` with `int`
// type of a is now `List int`
a.push(&quot;hi&quot;) // type error
</code></pre>
<p>I hope this can provide you some assistance.</p>
<p>ps. HM isn't that complex of an algorithm, most of the time! It's technically not great on worst case, but that worst case simply doesn't exist in good code, so it's really fine most of the time. My typechecker does unification similar to what I think you want to do, and it's ~200 LOC of OCaml.</p>

CC BY-SA 4.0
2023-10-12T09:12:01.640Z
2023-10-12T22:10:47.810Z
2023-10-12T22:10:47.810Z
blueberry
CC BY-SA 4.0
2023-10-12T12:03:53.807Z
Thanks! I probably need to write some demos with simpler situations before I put it in my interpreter. I don't understand the descriptions of the algorithm I've seen so far. I'm also still sorting out the data types within my type-checker implementation. I have an AST for "type exprs" which can be names, like `Int`, `String`, `Array`, `T`; or "calls" like `Array<Int>`, `Option<T>`. Some names are connected to concrete types, but others, like `T`, will be connected to type "parameters", in a given scope. I guess those type params are similar but not the same as the meta vars in unification.
Rob N
CC BY-SA 4.0
2023-10-12T22:10:32.063Z
@D.BenKnoble Thanks, didn't notice that. Have fixed.
blueberry
CC BY-SA 4.0
2023-10-13T00:39:45.863Z
@RobN You're correct - they're somewhat similar, but not the same. Thing of a metavar as "fixed, but unknown" - the type can't change, but you don't know it yet.
blueberry
CC BY-SA 4.0
2023-10-13T21:37:36.193Z
Yes, Rust does local type inference with unification. They pulled their unification algorithms out into a library, [Ena](https://lib.rs/crates/ena).
user570286
<p>I wouldn't describe unification as overkill for anything, or as heavyweight. It's conceptually simple and simple to implement. What you should be asking is whether it will work at all.</p>
<p>Unification means:</p>
<ol>
<li><p>Assign a unique type variable to everything that has a type that you don't already know (every binding and subexpression without a declared type).</p>
</li>
<li><p>For every constraint that must be satisfied for the program to be well-typed, in an arbitrary order, specialize the unknown types as little as possible to satisfy the constraint. If you can't do it, abort with a type error.</p>
</li>
</ol>
<p>If you make it through step 2, then you have perforce a valid typing of the program.</p>
<p>Hindley-Milner type inference is unification plus generalization (let-bound polymorphism), but since you're willing to require type signatures for reusable functions, you don't need the latter.</p>
<p>The problem with unification is that you need a type system designed so that you can &quot;specialize the unknown types as little as possible&quot; using only locally available information. Consider typechecking <code>nums.map {...}</code>. In your toy example, it's fine: you can think of <code>.map</code> as a function from objects to members, and it has an explicit type signature which you know because you collected it in a previous pass. But if you want more than one class to have a member named <code>map</code>, and you want to allow method calls on anything other than variables with explicitly declared types, then it's not so easy. Unification could specialize <code>nums</code> to &quot;some object type that has a <code>map</code> member&quot;, which is basically a Haskell-style typeclass constraint (<code>(HasMap a) =&gt; a</code>). Adding typeclasses is an extra complication, but it's not too bad: you just think of them as constraints on the unknown type variables, and do the minimum necessary to ensure they're satisfied too. Unfortunately, that's not good enough, because <code>nums</code> is more constrained than that: it needs a member named <code>map</code> that is specifically a function that takes a function as its first argument (among other things). To handle that, you could try a multiparameter typeclass constraint, <code>class HasMap o m | o -&gt; m</code> in Haskell syntax, expressing that the object type <code>o</code> has a member named <code>map</code> with the type <code>m</code>. That's more complication. But it won't work either, because the <code>map</code> method of <code>Array&lt;T&gt;</code> has a type that is polymorphic in <code>U</code>, which would require a third parameter to be added to <code>HasMap</code>, but there is no way for unification to know that. You could work around that by requiring members of the same name, even of unrelated classes, to have the same number of type parameters (and the same typeclass constraints on those parameters, if any), but it might be hard to explain that restriction to users.</p>
<p>You will run into similar issues if you want expressions like <code>2*x+1</code> to work whether <code>x</code> is an <code>Int</code> or a <code>Float</code>. My point is that designing a type system that is compatible with unification is not easy. (And if you succeed, you're likely to end up with Haskell's type system.)</p>
<p>These problems are the reason that most languages have ordered, bottom-up type inference: there has to be enough type information in the source code to determine the type of every binding without looking at its uses, and to determine the type of every subexpression without looking at its parent expression. Then it's guaranteed that the type of <code>nums</code> is known when you need to determine the type of <code>.map</code>.</p>

CC BY-SA 4.0
2023-10-12T20:56:57.390Z
2023-10-12T20:56:57.390Z
benrg
CC BY-SA 4.0
2023-10-13T13:40:28.607Z
Thanks! Very useful info. It seems like my example code has a bit of "top down" type inference, in the part where the closure param's type (`n: Int`) is inferred. I'm not sure yet whether I will have more things like that in my language. For now I'm going to play with unification and see if I can get something working.
Rob N
# Is a unification algorithm overkill for local type inference?
Posted by: username_0 on 2023-10-12
I'd like to create a type system similar to the one in Swift or Kotlin, where you have top-level functions that declare their parameters and return types, but you have some type inference with local variables and closures. For example, consider this code, which I hope is mostly self-explanatory since it uses typical syntax:
var nums: Array = [10,20,30,40]
var strs = nums.map { n → foo(n) }
var s = strs[0]
fun foo(i: Int) → String {
    return "i = $i"
} 

That syntax after the nums.map call is a closure. (Forget that it's probably better to pass foo directly.) The signature of Array.map is probably something like:
class Array {
    fun map(f: T -> U) -> Array
    ...
}

I'd want the type checker to derive that n is an Int, that the closure is Int -> String, that strs is Array, and s is String.
I've been reading about unification, which seems like the general purpose way of solving this problem, but it seems like it might be overkill here, because it was originally used for languages where you didn't have to specify the types anywhere and the inference algorithm needed to do more.
Should I learn how to implement unification, or is there a lighter weight algorithm that would be better for this style of language?
**Tags:** type-checker type-inference
> **Comments:**
> **username_1**: Unification is simple. My go to method for implementing all kinds of type systems is to have a simple pass that generate a system of type equations (for whatever typing rules you invented), and then another pass converting the rules into Prolog code. If you have even a simple embedded Prolog implementation inside your compiler (and you should - it can do a lot of heavy lifting for you), this two tiny passes solve all your typing problems in no time.  
> **username_0**: @SK-logic Did you implement a kind of Prolog-inspired logic engine yourself, or did you download a reusable library with Prolog in it?  
> **username_1**: I implemented Prolog myself, and then I was reusing it over and over for many different things. Here is an example of a small interpreted Prolog: https://github.com/combinatorylogic/mbase/blob/master/src/l/ext/rules.al  
> **username_2**: Another unification algorithm using triangular substitution is common to miniKanrens, and an explanation of how to implement it is [Hemann & Friedman 2013](http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf). I've implemented this algorithm in [Monte](https://github.com/monte-language/typhon/blob/master/mast/lib/logji.mt) and in [RPython](https://osdn.net/users/corbin/pf/cammy/scm/blobs/master/sampler/cammylib/types.py); that latter example was just for doing type inference.  
---
## 3 answers
### Answer by username_4 on 2023-10-12. Score: 7
tl;dr: Yes, you want unification. The question I think you should consider is "How are you going to use it?"
The fun part about unification is that it's very applicable.
Some variant of unification is going to ultimately be the thing you end up implementing, because it's the best tool for the task you're trying to solve - whether you need fully fledged Hindley-Milner/HM inference or not. (which is what I believe is what you're referring to with "because it was originally used for languages where you didn't have to specify the types anywhere" - unification is an algorithm, HM is another algorithm that utilizes unification for full-program type synthesis)
While HM may not be applicable to your ultimate solution in it's entirety, it does seem like a variant of it would be able to do what you want, for example, within the scope of a single function. This is what Rust does, if I recall correctly - You must provide types in various locations, but within the body of a function, it can deduce types through something very similar to HM.
Overall, I would recommend reading up on HM and an implementation of it, like algorithm J, and then consider how that might be applicable within the body of a function. (A hint: it'll be considerably simpler, because the complex part is function type inference, and you don't need that at all if I understand correctly)
Depending on your language, it might be as simple as assigning each unknown type a unifiable reference (commonly referred to as a metavariable in the literature, I believe) as a placeholder for it's type, and then unifying that reference with the real type when something like print_string(s) is found. Then, at the end of a scope of a function, you make sure no variable have an unknown type.
This means you might end up with something like:
let a = []; // type of a is `List $metavariable_0`
a.push(1); // unify `$metavariable_0` with `int`
// now a's type is `List int`

You'll note how that would work across the whole function with minimal issues due to the use of mutable references - when you change it once inside the unification function, it'll be changed everywhere, so you'll catch any sort of nasty type errors like
let a = [];  // type of a is `List $meta0`
a.push(1) // unify `$meta0` with `int`
// type of a is now `List int`
a.push("hi") // type error

I hope this can provide you some assistance.
ps. HM isn't that complex of an algorithm, most of the time! It's technically not great on worst case, but that worst case simply doesn't exist in good code, so it's really fine most of the time. My typechecker does unification similar to what I think you want to do, and it's ~200 LOC of OCaml.
> **Comments:**
> **username_0** (2023-10-12): Thanks! I probably need to write some demos with simpler situations before I put it in my interpreter. I don't understand the descriptions of the algorithm I've seen so far. I'm also still sorting out the data types within my type-checker implementation. I have an AST for "type exprs" which can be names, like `Int`, `String`, `Array`, `T`; or "calls" like `Array<Int>`, `Option<T>`. Some names are connected to concrete types, but others, like `T`, will be connected to type "parameters", in a given scope. I guess those type params are similar but not the same as the meta vars in unification.  
> **username_4** (2023-10-12): @D.BenKnoble Thanks, didn't notice that. Have fixed.  
> **username_4** (2023-10-13): @RobN You're correct - they're somewhat similar, but not the same. Thing of a metavar as "fixed, but unknown" - the type can't change, but you don't know it yet.  
> **username_5** (2023-10-13): Yes, Rust does local type inference with unification. They pulled their unification algorithms out into a library, [Ena](https://lib.rs/crates/ena).  
---
### Answer by username_6 on 2023-10-12. Score: 4
I wouldn't describe unification as overkill for anything, or as heavyweight. It's conceptually simple and simple to implement. What you should be asking is whether it will work at all.

Unification means:

1. Assign a unique type variable to everything that has a type that you don't already know (every binding and subexpression without a declared type).
2. For every constraint that must be satisfied for the program to be well-typed, in an arbitrary order, specialize the unknown types as little as possible to satisfy the constraint. If you can't do it, abort with a type error.

If you make it through step 2, then you have perforce a valid typing of the program.

Hindley-Milner type inference is unification plus generalization (let-bound polymorphism), but since you're willing to require type signatures for reusable functions, you don't need the latter.

The problem with unification is that you need a type system designed so that you can "specialize the unknown types as little as possible" using only locally available information. Consider typechecking `nums.map {...}`. In your toy example, it's fine: you can think of `.map` as a function from objects to members, and it has an explicit type signature which you know because you collected it in a previous pass. But if you want more than one class to have a member named `map`, and you want to allow method calls on anything other than variables with explicitly declared types, then it's not so easy. Unification could specialize `nums` to "some object type that has a `map` member", which is basically a Haskell-style typeclass constraint (`(HasMap a) => a`). Adding typeclasses is an extra complication, but it's not too bad: you just think of them as constraints on the unknown type variables, and do the minimum necessary to ensure they're satisfied too. Unfortunately, that's not good enough, because `nums` is more constrained than that: it needs a member named `map` that is specifically a function that takes a function as its first argument (among other things). To handle that, you could try a multiparameter typeclass constraint, `class HasMap o m | o -> m` in Haskell syntax, expressing that the object type `o` has a member named `map` with the type `m`. That's more complication. But it won't work either, because the `map` method of `Array` has a type that is polymorphic in `U`, which would require a third parameter to be added to `HasMap`, but there is no way for unification to know that. You could work around that by requiring members of the same name, even of unrelated classes, to have the same number of type parameters (and the same typeclass constraints on those parameters, if any), but it might be hard to explain that restriction to users.

You will run into similar issues if you want expressions like `2*x+1` to work whether `x` is an `Int` or a `Float`. My point is that designing a type system that is compatible with unification is not easy. (And if you succeed, you're likely to end up with Haskell's type system.)

These problems are the reason that most languages have ordered, bottom-up type inference: there has to be enough type information in the source code to determine the type of every binding without looking at its uses, and to determine the type of every subexpression without looking at its parent expression. Then it's guaranteed that the type of `nums` is known when you need to determine the type of `.map`.
> **Comments:**
> **username_0** (2023-10-13): Thanks! Very useful info. It seems like my example code has a bit of "top down" type inference, in the part where the closure param's type (`n: Int`) is inferred. I'm not sure yet whether I will have more things like that in my language. For now I'm going to play with unification and see if I can get something working.  
---
### Answer by username_3 on 2023-10-15. Score: 0
Tyr uses a type inference strategy that is likely very close to what you have in mind. I call it single level return type inference. What happens is that overload resolution gets an expected return type and all the argument types and does inference based on that. If you make a decision, you cannot change it. All global entities have defined parameter types, but may infer return types based on their definitions.

Now, regarding your question, you will need to do something like unification if you want to allow recursive signatures, i.e. ones where a parameter's type uses another parameter. For [example](https://github.com/tyr-lang/stdlib/blob/a77849fbf2db09716d7f96fad071c810df8224ab/lang/src/eqr.tyr#L52) operations on equivalence relations
take the underlying type and a function doing the equivalence check to derive == and != operators. Last time I checked, such definitions wouldn't be allowed in Go. The reason is that even type checking an application requires to do some sort of unification. TBH, I cannot tell the relation to HM.

However, the current binder parameter [inference](https://github.com/tyr-lang/test.conformance/blob/90d6bc84d2a5e8b73468057ec949054ff4b3f886/0.6.0/accept/bufferedIterator/mar.tyr#L20), which is type-checking wise likely identical to inference of local lambdas, is currently not based on unification. I haven't yet encountered an example where this would be required and, TBH, cannot tell if it would break my "single level" rule. That rule is required to provide somewhat understandable error messages. In essence, it allows creating an error location that is almost always useful.
---
