<p>I have a language like this:</p>
<pre><code>var s is str         &quot;&quot;;
var l is list[int]   [];
var m is map[int]str {};
</code></pre>
<p>where <code>[]</code> is the empty <code>list</code> literal, and <code>{}</code> is the empty <code>map</code> literal.</p>
<p>I want this language to have these type annotations be optional, and inferred by basing it on the literal:</p>
<pre><code>var s is &quot;&quot;;
var l is [];
var m is {};
</code></pre>
<p>However, this causes problems because, currently, my inference code marks the empty literals' inner types with a placeholder &quot;unknown&quot; type. So, when the empty literal is used, my type checker throws an error because &quot;unknown&quot; is incompatible with the known inner type:</p>
<pre><code>var strs is [&quot;hello!&quot;]; // list[str]
var ints is [0,1,2,3];  // list[int]
          // actual:
strs + [] // error: list[str] is incompatible with list[unknown]
ints + [] // error: list[int] is incompatible with list[unknown]
          // want:
strs + [] // ok, [] is inferred to be a list[str]
ints + [] // ok, [] is inferred to be a list[int]
</code></pre>
<p>How can I go about inferring the type of empty list and map literals?</p>

<types><type-inference><implementation>
How can I infer the type of an empty literal?
CC BY-SA 4.0
2023-06-30T14:19:52.913Z
I recommend reading about Algorithm W (aka Hindley-Milner type inference)
Jeremy
CC BY-SA 4.0
2023-07-18T21:44:36.497Z
For what it's worth, the bidirectional answer is to not infer the types of literals – only check them against a known type. This gives you overloaded numeric literals, among other things.
James Wood
CC BY-SA 4.0
2023-05-16T18:09:51.477Z
I believe that Rust handles this by inferring `<unknown>` generic types as the type of the first array interacts with, so for example you define a `Vec::new();`, it's an unknown type, and then when it's concatenated with a `Vec::<i32>::new()` the old variable is marked as an `<i32>` type array because that's the only way the operation can be valid.
kouta-kun
<p>As you said, &quot;unknown&quot; is a <em>placeholder</em>. It holds the place for a concrete type that has not yet been seen.</p>
<p>When you see <code>[&quot;hello&quot;] + []</code>, you're seeing three things:</p>
<ul>
<li><code>[&quot;hello&quot;]</code>, value of type <code>list[str]</code></li>
<li><code>+</code>, infix function (operator) with signature (type) <code>(list[T], list[T]) -&gt; list[T]</code></li>
<li><code>[]</code>, value of type <code>list[unknown]</code></li>
</ul>
<p>If I were the type checker, here's how I would do it:</p>
<ul>
<li>there's a type variable in the signature of the <code>+</code> I'm using here: <code>T</code>. Let's keep it in a corner of our head. We can think of the value of <code>T</code> as being <code>unknown</code> for now.</li>
<li><code>+</code> is called with a first operand of type <code>list[str]</code>, so I ask myself: does <code>list[str]</code> &quot;look like&quot; <code>list[T]</code>? Yes, if we assign <code>T=str</code>.</li>
<li>since we know the value of <code>T</code>, we know that the full signature of <code>+</code> here is <code>(list[str], list[str]) -&gt; list[str]</code></li>
<li>the second operand has type <code>list[unknown]</code>, which looks like <code>list[str]</code> if we assign <code>unknown=str</code>. Hence, the second operand has type <code>list[str]</code>.</li>
</ul>
<p>This is basically the Hindley-Milner algorithm, ran by hand. You have a set of unknowns (type variables), and your goal when analyzing the code is to find values (concrete types) to fill them. If any type variable is left unfilled (unknown) at the end of the analysis, you know the program is underspecified (for example, creating an empty list and never using it: what type is that list?)</p>

CC BY-SA 4.0
2023-05-16T18:12:21.733Z
2023-05-16T18:12:21.733Z
zdimension
CC BY-SA 4.0
2023-05-26T04:39:28.547Z
Unsolved local metavariables also aren’t _necessarily_ errors—you may or may not want to assign semantics to them. For example, in Haskell, unsolved variables are _defaulted_ when they have a suitable constraint such as `Num` or `IsString` arising from an overloaded literal. _Unconstrained_ type variables can’t affect the program, so they become the placeholder type `GHC.Types.Any`; while unsolved _kind_ variables become `Type` (the kind formerly known as `*`).
Jon Purdy
<p>If your language has <a href="https://wikipedia.org/wiki/Subtyping" rel="nofollow noreferrer">subtyping</a> and <a href="https://wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)" rel="nofollow noreferrer">(co-)variance</a>, and your lists are immutable, you can use those features.</p>
<p>In Scala, <a href="https://scala-lang.org/api/3.3.0/scala/Nothing.html" rel="nofollow noreferrer"><code>Nothing</code></a> is a <a href="https://wikipedia.org/wiki/Bottom_type" rel="nofollow noreferrer"><em>bottom type</em></a>, i.e. a subtype of every other type. That means, a value of type <code>Nothing</code> could be substituted for a value of any other type. (However, there exists no value of type <code>Nothing</code>, the type is uninhabited – <a href="https://scala-lang.org/api/3.3.0/scala/Predef$.html#???-0" rel="nofollow noreferrer">there are methods which have the return type <code>Nothing</code></a>, though, which means they don't return, and a call to such a method can be substituted for a value of any other type as well.)</p>
<p>The <a href="https://scala-lang.org/api/3.3.0/scala/collection/immutable/List.html" rel="nofollow noreferrer"><code>List</code></a> type constructor is covariant in the element type: <code>List[+A]</code>. Therefore, if <code>B</code> is a subtype of <code>A</code>, then <code>List[B]</code> is a subtype of <code>List[A]</code> and a value of type <code>List[B]</code> can be substituted for a value of type <code>List[A]</code>.</p>
<p>Since <code>Nothing</code> is a subtype of every other type and <code>List[+A]</code> is covariant, that means <code>List[Nothing]</code> is a subtype of every other list type. So, in Scala, the empty list (called <a href="https://scala-lang.org/api/3.3.0/scala/collection/immutable/Nil$.html" rel="nofollow noreferrer"><code>Nil</code></a>) has the type <code>List[Nothing]</code> and it can be passed wherever any list type is expected.</p>
<p>The method to prepend a list in front of another list (which is spelled <a href="https://scala-lang.org/api/3.3.0/scala/collection/immutable/List.html#:::-fffff631" rel="nofollow noreferrer"><code>:::</code></a> in Scala) has the type:</p>
<pre class="lang-scala prettyprint-override"><code>class List[+A]:
  def :::[B &gt;: A](prefix: List[B]): List[B]
</code></pre>
<p>I.e. it prepends a list whose element type is a super type of the list element type and returns a list of that super type. This would allow your example to type check in both directions (I am assuming that the <code>+</code> in your question is left-associative, i.e. that it is a method of the left operand):</p>
<pre class="lang-none prettyprint-override"><code>[] + strs
</code></pre>
<p>works because <code>+</code> allows the element type of the right hand operand to be a super type of the element type of the left hand operand and the result type is a list of the right hand operand's element type, i.e. a <code>list[str]</code>.</p>
<pre class="lang-none prettyprint-override"><code>strs + []
</code></pre>
<p>works because <code>[]</code> is of type <code>list[&lt;unknown&gt;]</code> which is a subtype of <code>list[str]</code>. In other words, <code>list[&lt;unknown&gt;]</code> <strong>IS-A</strong> <code>list[str]</code> and thus <code>[]</code> <strong>IS-INSTANCE-OF</strong> <code>list[str]</code>, so you're really just concatenating two lists of the same type.</p>

CC BY-SA 4.0
2023-07-01T07:06:20.810Z
2023-07-01T07:12:58.213Z
2023-07-01T07:12:58.213Z
Jörg W Mittag
<h1>Check usage</h1>
<p>While you may not know the type of the variable at first, you as the programmer can infer what type a variable is by looking at its usages later on. Is an integer added to it later, or is it passed to a function requiring a <code>list[point]</code>? Similarly, the type checker can do the same thing.</p>

CC BY-SA 4.0
2023-05-16T18:12:30.117Z
2023-05-24T00:07:48.290Z
2023-05-24T00:07:48.290Z
Seggan
<p>Instead of marking the type as <code>list[&lt;unknown&gt;]</code>, give the <code>&lt;unknown&gt;</code> a name in the form of a variable. Say, <code>list['a]</code>. Then, later in the same function, if someone comes along and treats an element of that list as an <code>int</code>, or tries to append an <code>int</code> to it, you can <em>unify</em> <code>'a</code> with <code>int</code>, providing additional information. If you get to the end of the function and there are still free variables in the type, then produce a &quot;failed to infer types&quot; compile error.</p>
<p>Alternatively, if your list type is immutable and your language has subtyping, you can just always infer the type to be <code>list[nothing]</code> (where <code>nothing</code> is the bottom type in your language), since immutable lists are covariant.</p>

CC BY-SA 4.0
2023-05-16T18:12:59.003Z
2023-05-16T18:12:59.003Z
Silvio Mayolo
CC BY-SA 4.0
2023-07-01T06:37:17.810Z
That's what Haskell does. In Haskell, values can be polymorphic, and the type of the empty list is just `[a]`, i.e. `List<T>` in the maybe more familiar C++/Java/C#-style syntax.
Jörg W Mittag
# How can I infer the type of an empty literal?
Posted by: username_0 on 2023-05-16
I have a language like this:
var s is str         "";
var l is list[int]   [];
var m is map[int]str {};

where [] is the empty list literal, and {} is the empty map literal.
I want this language to have these type annotations be optional, and inferred by basing it on the literal:
var s is "";
var l is [];
var m is {};

However, this causes problems because, currently, my inference code marks the empty literals' inner types with a placeholder "unknown" type. So, when the empty literal is used, my type checker throws an error because "unknown" is incompatible with the known inner type:
var strs is ["hello!"]; // list[str]
var ints is [0,1,2,3];  // list[int]
          // actual:
strs + [] // error: list[str] is incompatible with list[unknown]
ints + [] // error: list[int] is incompatible with list[unknown]
          // want:
strs + [] // ok, [] is inferred to be a list[str]
ints + [] // ok, [] is inferred to be a list[int]

How can I go about inferring the type of empty list and map literals?
**Tags:** types type-inference implementation
> **Comments:**
> **username_3**: I believe that Rust handles this by inferring `<unknown>` generic types as the type of the first array interacts with, so for example you define a `Vec::new();`, it's an unknown type, and then when it's concatenated with a `Vec::<i32>::new()` the old variable is marked as an `<i32>` type array because that's the only way the operation can be valid.  
> **username_1**: I recommend reading about Algorithm W (aka Hindley-Milner type inference)  
> **username_2**: For what it's worth, the bidirectional answer is to not infer the types of literals – only check them against a known type. This gives you overloaded numeric literals, among other things.  
---
## 4 answers
### Answer by username_4 on 2023-05-16. Score: 12
As you said, "unknown" is a *placeholder*. It holds the place for a concrete type that has not yet been seen.

When you see `["hello"] + []`, you're seeing three things:

* `["hello"]`, value of type `list[str]`
* `+`, infix function (operator) with signature (type) `(list[T], list[T]) -> list[T]`
* `[]`, value of type `list[unknown]`

If I were the type checker, here's how I would do it:

* there's a type variable in the signature of the `+` I'm using here: `T`. Let's keep it in a corner of our head. We can think of the value of `T` as being `unknown` for now.
* `+` is called with a first operand of type `list[str]`, so I ask myself: does `list[str]` "look like" `list[T]`? Yes, if we assign `T=str`.
* since we know the value of `T`, we know that the full signature of `+` here is `(list[str], list[str]) -> list[str]`
* the second operand has type `list[unknown]`, which looks like `list[str]` if we assign `unknown=str`. Hence, the second operand has type `list[str]`.

This is basically the Hindley-Milner algorithm, ran by hand. You have a set of unknowns (type variables), and your goal when analyzing the code is to find values (concrete types) to fill them. If any type variable is left unfilled (unknown) at the end of the analysis, you know the program is underspecified (for example, creating an empty list and never using it: what type is that list?)
> **Comments:**
> **username_5** (2023-05-26): Unsolved local metavariables also aren’t _necessarily_ errors—you may or may not want to assign semantics to them. For example, in Haskell, unsolved variables are _defaulted_ when they have a suitable constraint such as `Num` or `IsString` arising from an overloaded literal. _Unconstrained_ type variables can’t affect the program, so they become the placeholder type `GHC.Types.Any`; while unsolved _kind_ variables become `Type` (the kind formerly known as `*`).  
---
### Answer by username_8 on 2023-05-16. Score: 8
Instead of marking the type as `list[]`, give the  a name in the form of a variable. Say, `list['a]`. Then, later in the same function, if someone comes along and treats an element of that list as an `int`, or tries to append an `int` to it, you can *unify* `'a` with `int`, providing additional information. If you get to the end of the function and there are still free variables in the type, then produce a "failed to infer types" compile error.

Alternatively, if your list type is immutable and your language has subtyping, you can just always infer the type to be `list[nothing]` (where `nothing` is the bottom type in your language), since immutable lists are covariant.
> **Comments:**
> **username_6** (2023-07-01): That's what Haskell does. In Haskell, values can be polymorphic, and the type of the empty list is just `[a]`, i.e. `List<T>` in the maybe more familiar C++/Java/C#-style syntax.  
---
### Answer by username_6 on 2023-07-01. Score: 5
If your language has subtyping and (co-)variance, and your lists are immutable, you can use those features.
In Scala, Nothing is a bottom type, i.e. a subtype of every other type. That means, a value of type Nothing could be substituted for a value of any other type. (However, there exists no value of type Nothing, the type is uninhabited – there are methods which have the return type Nothing, though, which means they don't return, and a call to such a method can be substituted for a value of any other type as well.)
The List type constructor is covariant in the element type: List[+A]. Therefore, if B is a subtype of A, then List[B] is a subtype of List[A] and a value of type List[B] can be substituted for a value of type List[A].
Since Nothing is a subtype of every other type and List[+A] is covariant, that means List[Nothing] is a subtype of every other list type. So, in Scala, the empty list (called Nil) has the type List[Nothing] and it can be passed wherever any list type is expected.
The method to prepend a list in front of another list (which is spelled ::: in Scala) has the type:
class List[+A]:
  def :::[B >: A](prefix: List[B]): List[B]

I.e. it prepends a list whose element type is a super type of the list element type and returns a list of that super type. This would allow your example to type check in both directions (I am assuming that the + in your question is left-associative, i.e. that it is a method of the left operand):
[] + strs

works because + allows the element type of the right hand operand to be a super type of the element type of the left hand operand and the result type is a list of the right hand operand's element type, i.e. a list[str].
strs + []

works because [] is of type list[] which is a subtype of list[str]. In other words, list[] IS-A list[str] and thus [] IS-INSTANCE-OF list[str], so you're really just concatenating two lists of the same type.
---
### Answer by username_7 on 2023-05-16. Score: 4
# Check usage

While you may not know the type of the variable at first, you as the programmer can infer what type a variable is by looking at its usages later on. Is an integer added to it later, or is it passed to a function requiring a `list[point]`? Similarly, the type checker can do the same thing.
---
