Full type inference, list datatype

[sharkdp]

This PR adds proper type inference to Numbat. It also makes the type system more powerful (with respect to generics). A few highlights:

• Full Hindley-Milner-style type inference for arbitrary Numbat programs. Including inference for dimension types (see Functions: full type inference #29)
• Generics for arbitrary types, not just dimension types
• Proper support for List<T> for all types T (see Add a list datatype #261). Together with proper generics handling (see below), this should allow us to implement Add sums and products #66
• Polymorphic values for 0, NaN and inf (see Zero, NaN, inf should be polymorphic #37)
• Type inference works for recursive functions, too. We can get rid of the restriction that the return type needs to be specified.
• Fixes Can not infer type parameter when calling generic function from generic function #166
• Allows us to implement generic numerical differentiation (Numerical derivatives, integrals #145) inside Numbat using:

  let eps = 1e-10
  
  fn diff<X, Y>(f: Fn[(X) -> Y], x: X) -> Y / X =
    (f(x + eps · unit_of(x)) - f(x)) / (eps · unit_of(x))
  

  Example: say you have a function from Time -> Length, then you will get a Velocity as a result from diff.

Other changes:

• Support for variadic functions has been removed. We can cover all use cases with lists
• The Never/! data type has been removed. Instead, the error function now has type forall A. String -> A

Open challenges:

• There is a severe regression concerning error messages for rather basic things like kg m / s^2 + kg m^2 where we will now get a constraint solver error instead of our nice incompatible-dimensions error.
• Properly integrate structs. Field access is currently broken when accessing structs in functions. This could be fixed by requiring annotations for structs. What type should fn f(x) = x.foo have otherwise? The only reasonable option would be to go back to structurally typed records and do something similar to Haskell (or probably better, similar to PureScript).
• DateTime arithmetic is currently broken. The problem is with the overloaded +/- operators. If we have something like x - y with yet-unknown types, we would like to say: either, x and y can be of the same dimension type OR x could be a DateTime and y a Time or a DateTime. This kind of either-or constraint can not be formulated currently. The way this is solved in other Hindley-Milner languages is through type classes / trait bounds. We would need to add (multi-parameter?) type classes to model things like forall D: Dim. Sub(D, D), Sub(DateTime, DateTime) and Sub(DateTime, Time).
• Properly treat Dim constraints and add a new syntax for them, e.g. fn sqrt<D: Dim>(x: D^2) -> D = ….

To do:

• Finish type inference experiments
• Remove variadic functions
• error("hi") + true should be a type check error
• Fix inferred type for e.g. fn test(f, xs) = f(head(xs))
• Completely remove Never type
• Replace Never type with forall D. D or forall D: Dim. D
• Add tests from Type checker: generics handling #253
• Does something like 1 m + 0 * 1 s work?
• Fix ==/!= operator.
• Addition/subtraction needs Dim constraints (and possibly other operators as well): fn f(x)=x+true, fn f(x,y)=x+y
• Arity needs to be checked properly for callables
• fn f(x, y) = x^y, fix todo!(…)
• Test for fn f(x) = x + true
• Add tests for type inference (see typechecker experiments)
• Fix env polution by fn parameter identifiers
• Bring back commented-out tests
• Improve constraint solver error messages
• Improve substitution error messages (how can they trigger?)
• Fix all TODOs
• Bring back readable_types (see TODOs in bytecode_interpreter and type_scheme.rs)
• Bring back printing of function signatures when using info
• Remove to_concrete_type
• Remove instantiate_for_printing?
• Reset deploy.sh

Follow ups:

• Removing logging dependencies?
• Update documentation, update https://numbat.dev/articles/intro.html
• try_trivial_resolution can easily analyze the constraint structure further to discard constraints like List<T0> ~ Bool, which will yield better error messages in return
• Equality on function types should be forbidden. Maybe we need to introduce an Eq type class.
• Better error message for sth. like true(2)
• Lists are embarrassingly slow. I'm sure there are some long hanging fruit...
• Check if we can reduce the number of constraints: (1) by cancelling out equal constraints and (2) by not adding as many constraints. for example, in x + y, we need type(x) ~ type(y) and IsDim(type(x)), but we could potentially save the IsDim(type(y)). On the other hand, that would result in worse error messages.
• Re-read http://typesatwork.imm.dtu.dk/material/TaW_Paper_TypesAtWork_Kennedy.pdf
• Implement mean, stddev, etc in Numbat
• For all (generic) functions that we have, check that we can (1) remove all type annotations and (2) get the same type or a more general type.
• Give quadratic_equation a List<B/A> return type.
• Something like fn foo<D1, D2>(x: D1*D2) = 1 should yield a "missing Dim bound" constraint, because the type parameters are used type annotation dimension expression
• Add tests for type inference with partial annotations
• Better error message for fn f<A: Dim>(x: A) -> A = 2x; f(true)
• When quantifying a function type with annotations, use the user-specified identifiers
• Disallow generic types in dimension / unit definitions (unit magic = 0; 1 m -> magic), allow them in variable definitions
• Improve error messages for callables, see function_types_in_argument_position test
• Fix regression concerning "readable types". For example: let v = 1m/s would previously print let v: Velocity = …. Similarly, it would be cool if we would annotate v in fn f(v)=v+1 knot with a Velocity type
• Bring numerical diff functionality to the prelude (Numerical derivatives, integrals #145)
• Use assert_eq instead of assert in Numbat code tests

Cool stuff:

• Generic list functions, see numbat/modules/core/lists.nbt.
• Infer type of map or fold. Type something like

  fn fld(f, acc, xs) = if xs == [] then acc else fld(f, f(acc, head(xs)), tail(xs))
  

  and see the right type of fold come out
• diff: Check out examples/numerical_diff.nbt on this branch
• Type something like fn f(x) = m² / x + s² * x or fn f(x, y) = x + y^2 and see the correct type being inferred.

closes #29
closes #261
closes #324
closes #37
closes #166

[hamirmahal]

Nice!