PoC: Generics and better type inference

[ysthakur]

This is a proof-of-concept implementing generics and slightly better type inference. It's based on the paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, although I had to make some modifications because their type system is pretty different from ours. I'm not sure yet if the new type inference algorithm will never infer the wrong type, and there's missing pieces here and there. But we should be able to make this general approach to type checking/inference work.

This is what it looks like:

def f<T> [ x: T ] : nothing -> list<T> {
  let z = $x
  [$z]
}
f 123 # Inferred to be of type list<int>

I didn't do subtype/supertype bounds on type parameters, but it shouldn't be terribly hard to implement with the current design.

Other things included in this PR:

• A top type (supertype of all types), a bottom type (subtype of all types), and intersection types (allof). These are only created internally by the typechecker. Users can't write them themselves, but that's a completely artificial restriction; I just didn't feel like working on the parser again.
• Better consideration for any and oneof
• The types of custom command parameters are used when typechecking

Things worsened by this PR:

• ++ requires both operands to be lists, to match how Nushell now works
• Type mismatches for binary operators now have less descriptive error messages
• Repetitive error messages. If you typecheck let x: list<list<int>> = [["foo"]], you'll get 3 error messages instead of just one (one saying "foo" should be an int, one for ["foo"], and one for [["foo"]]).

Things left to do:

• When getting rid of type variables at the end of typechecking, make sure that the lower bound is actually a subtype of the upper bound

Apologies for the big PR. I should probably have done some of these things before implementing generics. That said, it's just a proof-of-concept, so it doesn't need to be reviewed thoroughly.

How type checking/inference work

The typecheck_expr method takes the expected type of the expression it is currently processing and provides an inferred type for every expression it visits. This way, we both check against the expected type and infer a type for the expression at the same time.

For generics to work, the algorithm requires creating and solving type variables. These type variables have a lower bound and an upper bound. As we move through the program, these bounds are tightened further. At the end of the program, the lower bound of each type variable is chosen as its value.

Every time we come across a call to a custom command with type parameters, we instantiate new type variables corresponding to those type parameters. For example, for the expression f 123 above, we instantiate a new type variable '0 with lower bound bottom and upper bound top (essentially unbounded). Because of the signature of f, we know that 123: '0 and f 123: list<'0>.

So we first call typecheck_expr to check/infer the type of 123, providing '0 as its expected type. Since it's just an integer literal, we infer the type to be int. Then, to ensure that this type matches the expected type ('0), we call the constrain_subtype method to ensure that int <: '0. The existing lower bound for '0 was bottom, so we set the new lower bound to oneof<bottom, int> = int.

Then we set the type of f 123 to list<'0>. After all expressions have been processed, we replace all occurrences of '0 with int. So this becomes list<int>.

Recursive bounds are not allowed. The bounds for a type variable (say, '5) can only refer to type variables created before it (here, '0 through '4).

• If, during typechecking, we find ourselves setting the upper bound of '5 to '6, then we instead set the upper bound of '5 to whatever the lower bound of '6 is at that point. This behavior can be improved upon somewhat in the future (in this particular example, we could instead update '6's lower bound to include '5), but I think it's good enough for now.

[kubouch]

Sorry for the late reply. I think the motivation for generic is clear enough, e.g. being able to go from int to list<int>. My worry if that we might be complicating the language too much and it'd look too much like C++. I tried thinking along the lines of using types as values and doing something similar to how Zig handles generics with comptime, but I didn't arrive at anything that would actually work for us. So this might just as well be fine.

It would also be worthwhile to think how this would work with the envisioned typealias feature, something like:

typealias listoflists<T> = list<list<T>>
def foo<T> [x: T] -> listoflists<T> { [[$x]] }

Some short comments, haven't yet looked at the code:

• Would it be possible to also specialize the type, e.g., def foo<T: oneof<int, str>> [ x: T ] -> list<T>? Not necessary in this PR, just in principle I think that's what people would eventually want to do.
• Space or no space (def foo<T> vs. def foo <T>)? (Or both?)

A top type (supertype of all types), a bottom type (subtype of all types), and intersection types (allof). These are only created internally by the typechecker. Users can't write them themselves, but that's a completely artificial restriction; I just didn't feel like working on the parser again.

• Isn't the "top" type just any?
• Is there any use case for these to be explicitly written by the user? If not, we could just keep them internal as an implementation detail.

The error messages is something to look at, but there wasn't much work on them anyway, so that could be also done in some later PR.

[ysthakur]

Type aliases definitely need more thought, the code in this PR isn't prepared for them. I was thinking about having a cache of types (so that we don't create multiple Type objects for listoflist<int>, we only create it once and look it up afterwards). We should probably discuss how we want to handle recursive aliases and stuff.

Regarding the comments:

• Yup, subtype and supertype bounds should be very easy to do with this design. We simply instantiate type variables with those bounds rather than bottom as the lower bound and top as the upper bound.
• I would prefer not caring about spaces so we can allow def foo<T>, def foo <T>, def foo < T >, etc. I'm more concerned about syntax at the call-site, though, if we choose to allow explicitly supplying type arguments. foo <int> bar baz would look really weird in Nushell.
• No, the top type isn't the same as any. any is sort of simultaneously the top and bottom type - it's the supertype of all types but also the subtype of all types. I think this is something you'd only see in a gradually typed language. top is only the supertype of all types, and this is something you'd see in all sorts of languages.
• I think top and bottom should be exposed to users, I was just being lazy keeping them internal. In general, I think it's good for users to be able to represent as many of the types used by the compiler as possible.
  • top is useful for someone who wants to allow arguments of any type to their command. any also works, but it basically disables type checking, which isn't great.
  • bottom is less useful for users, but it lets you say that a particular command won't return. It can be used as the return type for commands that always panic, or commands that loop infinitely. Scala's equivalent of this is Nothing, and I find myself using it pretty often.

[kubouch]

Cache of types sounds reasonable. Agreed also on the spaces.

I think top and bottom should be exposed to users

I'm worried about the cognitive complexity of having all any, top and bottom. We're supposed to be noob-friendly scripting language and I think this would add too much PL jargon.

I still struggle to find a practical difference between any and top, could you give an example? To me, it seems that any is used in scenarios where the user wants top, so shouldn't we keep just top and rename it to any?

For bottom, I guess it could be named noreturn (and allowing it only as a return type because it does not make sense elsewhere?). Then, seeing def foo []: nothing -> noreturn { loop {...} } seems quite intuitive.

[kubouch]

It would be good to add a reference to the paper in the top-level comment so that it shows in the (future) documentation what the type checking is based on.

[kubouch]

Perhaps the whole text where you explained how it works in the PR description under "How type checking/inference work" should be stored somewhere. Either as a top-level module comment here, or have a Markdown doc somewhere in the repo and refer to it. I'm just thinking from the perspective of a new contributor opening this file and trying to figure out how it works.

[ysthakur]

Good idea. A Markdown doc would probably be easier to read.

[kubouch]

I also just noticed the "allof" (intersection) type, I quite can't wrap my head around it. Can you give an example how it differs from "oneof" (union) type, or what it is used for in the type checker? Is allof<...> something that would be useful in the language, like oneof<...>, or is it only implementation detail?

[ysthakur]

I'm worried about the cognitive complexity of having all any, top and bottom. We're supposed to be noob-friendly scripting language and I think this would add too much PL jargon.

Yeah, that's a fair point. We could get away with only having any, and then we could try our best to hide top and bottom from users in error/warning messages (for example, if a type has upper bound top, we can just say it has no upper bound).

I still struggle to find a practical difference between any and top, could you give an example?

Consider a custom command that takes any input, converts it to a string, and truncates it:

# Both of these signatures are the same to people *calling* the command
def truncate [ x: top ] { $x | str substring 0..5 }
def truncate [ x: any ] { $x | str substring 0..5 }

Except the implementation here is incorrect. $x may not be a string, so str substring can't be called on it before converting it to a string. If you use x: top, this will be caught at parse time, but not if you use x: any, since any disables typechecking. So I guess the difference between the two is: people who want strict typechecking will use top, people who don't care so much (or need to disable typechecking) will be fine with any.

I'm assuming top won't be used very often, so it's fine to not allow users to refer to it and only construct it internally. But then we'll also have to avoid showing it in diagnostics, because otherwise, users would have to know what it means anyway, and at that point, why not let them construct it themselves too?

To me, it seems that any is used in scenarios where the user wants top, so shouldn't we keep just top and rename it to any?

If you're saying we should get rid of any, I don't think we can do that, because that's the thing that enables Nu's gradual typing. Without any, I don't see a way to tell the compiler: "shut up, this code is safe even if it won't typecheck."

For bottom, I guess it could be named noreturn (and allowing it only as a return type because it does not make sense elsewhere?). Then, seeing def foo []: nothing -> noreturn { loop {...} } seems quite intuitive.

I like noreturn! I was going to suggest something like impossible as a "friendly" name, but I don't really see the bottom type used for anything but return types. In other languages, it can be used for all sorts of tricks, but Nushell's too simple for that.

---

Tangent about naming: TypeScript also has an any type that's like our any type. The bottom type is never. In 2018, TS added unknown, which is the top type (so I guess we can get away with not having a top type, at least for a bit). It's completely irrational, but this naming brings me SO MUCH pain. I wish so badly that TS would swap the names for any and unknown, because that just makes so much more sense to me.

In Nushell, if heavy breaking changes are on the table, I'd love to name the top type any, because an instance of this type could be anything. What we currently call any could be renamed to something that more clearly indicates that this is a special type for disabling typechecking (maybe unchecked or untyped).

[ysthakur]

I also just noticed the "allof" (intersection) type, I quite can't wrap my head around it. Can you give an example how it differs from "oneof" (union) type, or what it is used for in the type checker? Is allof<...> something that would be useful in the language, like oneof<...>, or is it only implementation detail?

An value of type allof<A, B, C> is a value that is of types A, B, and C simultaneously. In general, this is pretty useless outside the typechecker, because a value can only be of multiple types when it's a record (or a list of records).

Some examples with simple types. It's useless here, because it simplifies to something the user could've written themselves:

• allof<int, string> is the bottom type, because nothing can be both an integer and a string at once
• allof<int, number> is int, because int is a subtype of number
• allof<int, top> is int (same principle as allof<int, number>)

Some examples with records. Here, it's essentially a deep merge operator:

• allof<record<a: int>, record<b: int>> is record<a: int, b: int>
  • This is recursive, going inside both records and lists. For example: allof<list<record<a: int>>, list<record<b: int>>> is list<record<a: int, b: int>>
• allof<record<a: int>, record<a: string>> is record<a: allof<int, string>>, which simplifies to record<a: bottom>. This really ought to simplify to bottom, because there's no way to construct a record<a: bottom>, but I don't think my current implementation handles that.

This record type merging can be useful if you're working with type parameters. You can define a signature like this (warning: stupidly contrived example incoming):

def copyAndIncrementA<T> [ x: T, y: T & record<a: int> ] : nothing -> T & record<a: int> {
  { ...$x, a: $y.a + 1 }
}

> copyAndIncrement {b: 1} {b: 2, a: 3} # Type: record<b: int, a: int>
{b: 1, a: 4}

Within the typechecker, type parameters are what justify the existence of the Type::AllOf variant. If it weren't for references to type parameters, allof<a, b, ...> would always simplify to a proper type not containing allof. But you can't simplify something like allof<T, record<a: int>> (where T is a type parameter), so the AllOf variant represents types like that.

In addition to references to type parameters, allof types involving type variables also can't be simplified, because again, in allof<'1, '2>, you have no idea what the type variables '1 and '2 are yet. Type variables are an internal thing, though, not visible to users.

allof is also essential for putting constraints on type variables. Suppose the typechecker has a type variable '1 with bounds bottom <: '1 <: '2, where '2 is some other type variable. Now suppose it comes upon a piece of code that provides it with the following information: "'1 is a subtype of number." Now we want to update '1's upper bound to express the fact that it is a subtype of both '2 and number. This can be done by updating '1's bounds to bottom <: '1 <: allof<'2, number>.

Does that help? I really hope I didn't make you read that wall of text for nothing. I'll come up with an actual piece of Nushell pseudocode that demonstrates that allof-constraint thing I mentioned (later, when I'm not functioning on 4 hours of sleep).

[kubouch]

Thanks! Very helpful. I'll need to re-read the allof part again, but it sounds like something we don't really need to be user-facing, ie. can be kept as an implementation detail in the parser.

Just to clarify top, in this example

def truncate [ x: top ] { $x | str substring 0..5 }

the typechecker would infer the type of $x to be string, then give you a compile error if you do truncate 1.0? Then, in the case of

def def truncate [ x: top, --test ] { 
    if $test {
        $x | str substring 0..5
    } else {
        $x + 1
    }
}

the $x would be inferred as oneof<string, number>? If so, I can imagine this being annoying/undesirable sometimes and the user wanting to use any instead. However, there is also a fundamental problem that now it's not possible to figure out what type of x is expected by truncate only from reading the code (if the function is more complex..). So from this perspective, it might not be desirable to expose it to the user and we'd require0- to manually type oneof<string, number. This can be remedied by LSP, help message etc. which could show the underlying concrete expected type, however.

So either we keep any as-is and disallow top to be user defined, or we allow both, but we need to think about naming. I'd propose using auto as the name for top. Something that suggests that the type is inferred to some concrete type, and auto has the advantage of being both intuitive and understandable to anyone who's ever programmed C++. Changing any is on the table (there are/will be many other breaking changes in the new parser anyway...) but I quite like it in its current role. Alternatively, something like unknown, unchecked, etc. could be also considered, though they are quite long (untyped sounds like it has no type).

I think noreturn is pretty self-explanatory if used only as a return type so I think making it user-facing would be OK.

But yeah, I think most of this can be left for further discussion. I'd like to check the code a bit just to make sure I understand is, but otherwise the PR looks good.

One more thing: Could you run some benchmarks before/after this PR?

[ysthakur]

I'll need to re-read the allof part again, but it sounds like something we don't really need to be user-facing, ie. can be kept as an implementation detail in the parser.

Yup, it should be fairly easy to hide from the user in error messages.

---

Just to clarify top, in this example the typechecker would infer the type of $x to be string, then give you a compile error if you do truncate 1.0?

No, sorry, I don't think I explained correctly. This StackOverflow question talking about TypeScript's unknown (same as top here) and any might help. top is just a normal type, similar to Java's Object. It has nothing to do with C++ auto.

When you declare a parameter or variable as x: top, the type of $x is just top. No type inference is done. The type of $x will never change from what the user specified to int or something. If you did the following, you'd just have two errors:

def truncate [ x: top, --test ] { 
    if $test {
        $x | str substring 0..5 # Error: `str substring` expects string input, got top
    } else {
        $x + 1 # Error: '+' isn't supported on top and int
    }
}

I don't think we need to bother implementing syntax like C++'s auto/Rust's _ right now. If someone wants the type of a parameter to be inferred, they could simply omit the type annotation (same way variable declarations work). Currently, if you have a parameter without a type annotation, its type annotation is just set to any, but making the type be inferred instead shouldn't be hard. Then, in the following command definition, x would be inferred as a oneof<string, number>, like you said.

def truncate [ x, --test ] { 
    if $test {
        $x | str substring 0..5
    } else {
        $x + 1
    }
}

So either we keep any as-is and disallow top to be user defined, or we allow both, but we need to think about naming.

Yeah, the name top definitely won't work, even if we only display it occasionally in error messages. I think we could leave this sort of thing to a discussion on Discord, though. I'm sure in a large enough group of people, someone can think of a decent name.

---

One more thing: Could you run some benchmarks before/after this PR?

Good idea, I'll figure them out sometime this week. Will definitely be slower :(

[132ikl]

I think renaming any to unknown, unchecked, untyped would be a reasonable option since I assume most people leave off the annotation rather than explicitly doing foo: any. I think having the top type exposed could be a good direction. I think this would allow us to better express commands in Nu which would be written a big match over Value variants in Rust commands, although it's not exactly clear to me how you would use it in practice. Would we need to have some kind of way to coerce top into concrete types?

[ysthakur]

Just to clarify, right now, if you leave the type annotation off a variable declaration, its type is inferred rather than defaulting to any, e.g., let x = 3 means x is an int, not an any. That said, I don't think thr extra typing would be too bad - making it a little harder to use any might discourage users from overusing it.

For matching on x and then coercing it to a lower type, here's what I can think of (not mutually exclusive options):

• Flow typing (overkill)
• Explicit downcast command
• Don't coerce at all, just create new variables with narrower types. This is what Scala does and it works quite well. An example (Scala's Any is the top type):

def foo(x: Any) =
  x match {
    case i: Int => i + 2
    case s: String => s + "bar"
    case List(a: Int, b: String) => println("this is a list containing an int and then a string)
  }

[ysthakur]

Unfortunately, I can't compare the benchmarks with the compare command because I get the following error, any idea why?

thread 'main' panicked at /home/ysthakur/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tango-bench-0.6.0/src/dylib.rs:62:60:
called `Result::unwrap()` on an `Err` value: UnableToLoadSymbol(DlSym { desc: "/home/ysthakur/new-nu-parser/tango/bin/main/benchmarks.patched: undefined symbol: tango_init" })

I did run them separately and put the results in this gist.

[132ikl]

benchmarks are looking good, that's a lot of power in the type system for not much performance penalty

[132ikl]

i also played around with the benchmarks a bit to make them a bit easier to interpret at a glance, this is the sum of the min/avg/max for each test category:

before:

name	min	avg	max
def	5µs 792ns	8µs 79ns	25µs 500ns
if	4µs 107ns	6µs 145ns	16µs 651ns
combined	22µs 909ns	35µs 100ns	97µs 100ns
combined10	228µs 700ns	358µs 900ns	1ms 299µs 200ns
combined100	2ms 747µs 100ns	3ms 803µs 300ns	11ms 361µs
combined1000	40ms 961µs 800ns	57ms 900µs	126ms 600µs
int100	42µs 700ns	55µs 100ns	115µs 100ns

after:

name	min	avg	max
def	6µs 161ns	8µs 379ns	17µs 875ns
if	4µs 951ns	6µs 709ns	17µs 7ns
combined	32µs 457ns	43µs 200ns	108µs 500ns
combined10	343µs 800ns	460µs 800ns	1ms 577µs 300ns
combined100	3ms 825µs 400ns	4ms 829µs 800ns	11ms 70µs
combined1000	48ms 915µs 800ns	63ms 400µs	125ms 700µs
int100	50µs 900ns	67µs 600ns	222µs 400ns

code

$results
| lines
| parse "{name} {_} [ {min} ... {avg} ... {max} ]{_}"
| str replace -a " " "" min avg max
| into duration min avg max
| where name !~ nu_old
| group-by { get name | split row '_' | get 0 } --to-table
| insert min {|e| $e.items.min | math sum }
| insert avg {|e| $e.items.avg | math sum }
| insert max {|e| $e.items.max | math sum }
| rename name
| reject items

[kubouch]

No type inference is done.

OK, perfect. I don't think we should be inferring parameter types because it would be hard to track and debug for the user. It would be impossible to tell just from the command signature what types it expects. This would also prevent (imagined possible) features like linking from working.

• Explicit downcast command

We have into commands which work like that.

• Don't coerce at all, just create new variables with narrower types.

Seems good enough to me. We have describe already, but we can tweak it to make this stuff more ergonomic. Together with into, specific cast commands could be implemented as regular Nu commands by users.

Much of the discussion was about the top/bottom parts being exposed to the user. I think we can just leave that for a future PR, but to summarize:

• any would be renamed to unchecked
• top would be any
• bottom would be noreturn and allowed only as a command return type
  If we're going to do this, then it's not necessary to fix the error messages because we'd have to fix them again once these types are exposed.

[kubouch]

Benchmarks: There is clearly a performance hit, but doesn't seem too dramatic (eg. about 10% on the combined1000 benchmark). I think it's to be expected as we add new features, but it's good to check to prevent accidental excessive regressions.

Yeah, I've noticed the tango panic. We might want to swap to something else, maybe criterion, or even default cargo bench.

[kubouch]

Looked at the code, it seems good. The allof is also clarified. I'd say let's go with it. I'm still leaving it unmerged since it's still in draft, but when you're ready, we can merge.

[132ikl]

any would be renamed to unchecked
top would be any

@kubouch we brought up this idea with the team at the last meeting and it seems like people were generally leaning away from it. I think the general consensus was that it would be okay to make a top type usable for power users; folks at the meeting are satisfied with how any works right now and that the distinction between the unchecked and top types wouldn't matter enough for most people to name the top type any.

I do like the idea still but I understand the concerns. If you think we should go this route then I think it would mean a lot to the team coming from you, but maybe we should reconsider if you're not set on it.

If we are still interested in possibly going this route I think it might also be good to get a solid understanding of what this would look like in practice, like under what circumstances you would actually need to specify unchecked rather than top. If it's relatively seamless and you could use top in most/all the places you can use any right now, then maybe it would be fine? I think the biggest concern is that it makes things too confusing/complex but if the average person using Nushell can get by with just using any/top then folks might be more on board, but I definitely can get behind wanting to keep things simple.

Stefan also pointed out that we would want to use the old parser tests for the new parser and this kind of change would make it a lot more difficult, but you did mention that there are already breaking changes in the new parser so I suppose that's an issue regardless

[ysthakur]

Forgot about this PR. I threw in a document contributing/typechecking.md and basically just copied my PR description into that. I'll update the documentation more in subsequent PRs.

[132ikl]

I'll merge this since it seems like documentation was the last outstanding issue and Kubouch was in favor of merging this:

Thanks for the reply on the type system PR. I think we can merge it as-is basically, and continue the discussion about top/bottom/any outside of that. I personally don't care much about the naming, as long as it's recognizable