List datatype

[sharkdp]

This is a basic implementation of lists for Numbat. We construct lists using […] notation and the type of lists is specified as List<T> where T can be any type.

>>> [1, 2, 3]

    = [1, 2, 3]    [List<Scalar>]

>>> [1m, 30cm]

    = [1 m, 30 cm]    [List<Length>]

>>> [["foo", "bar"], ["baz"]]

    = [[foo, bar], [baz]]    [List<List<String>>]

Operationally, they work just fine. For example, we can add the functional-programming style primitives head, tail and cons:

fn head<A>(xs: List<A>) -> A
fn tail<A>(xs: List<A>) -> List<A>
fn cons<A>(x: A, xs: List<A>) -> List<A>

and they work as expected:

>>> cons(0, [1, 2, 3])

    = [0, 1, 2, 3]    [List<Scalar>]

We can even write some useful functions like

>>> fn generate(n: Scalar, f: Fn[() -> Scalar]) -> List<Scalar> =
  if n == 1
    then [f()]
    else cons(f(), generate(n - 1, f))

>>> generate(10, random)

    = [0.372604, 0.123614, 0.297907, 0.966904, 0.296039, 0.351666, 0.923613, 0.0140005, 0.254682, 0.518355]    [List<Scalar>]

Type checking of list construction also works fine:

>>> [1 m, 40 cm, 3 kg, 2 m]
error: while type checking
  ┌─ <input:3>:1:2
  │
1 │ [1 m, 40 cm, 3 kg, 2 m]
  │  ^^^         ---- Mass
  │  │            
  │  Length
  │
  = Incompatible types in list: expected 'Length', got 'Mass' instead

However, there are a number of open questions / issues regarding the handling of lists in the type checker:

• We don't have polymorphic values yet. So we can't type the empty list [], which should have the type ∀D. List<D>. We have a similar problem with typing 0, NaN and inf, see Zero, NaN, inf should be polymorphic #37.
• Almost all useful functions on lists will be generic over the element type. Very basic things (like len, head, tail, cons) work fine when implemented via the FFI. But if we want to use those functions to implement map, filter, etc., we are running into type inference problems (already reported as Can not infer type parameter when calling generic function from generic function #166).
• Polymorphism in Numbat only works for dimension types (Scalar, Length, Length^2, Length / Time, etc). But so far, we can't be generic over all types, which means we can not give a type to a function that works on all lists, only on lists of arbitrary dimension types. So we can create things like List<Bool>,List<String> or List<List<Length>>, but we can't run cons, head, tail on them.

related ticket: #261

[sharkdp]

see follow up: #443