14
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – kouta-kun
    Commented May 16, 2023 at 18:09
  • $\begingroup$ I recommend reading about Algorithm W (aka Hindley-Milner type inference) $\endgroup$
    – Jeremy
    Commented Jun 30, 2023 at 14:19
  • $\begingroup$ 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. $\endgroup$
    – James Wood
    Commented Jul 18, 2023 at 21:44

4 Answers 4

11
$\begingroup$

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?)

$\endgroup$
1
  • $\begingroup$ 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 *). $\endgroup$
    – Jon Purdy
    Commented May 26, 2023 at 4:39
8
$\begingroup$

Instead of marking the type as list[<unknown>], give the <unknown> 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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$ Commented Jul 1, 2023 at 6:37
5
$\begingroup$

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[<unknown>] which is a subtype of list[str]. In other words, list[<unknown>] IS-A list[str] and thus [] IS-INSTANCE-OF list[str], so you're really just concatenating two lists of the same type.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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