Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

List datatype #432

Closed
wants to merge 4 commits into from
Closed

List datatype #432

wants to merge 4 commits into from

Conversation

sharkdp
Copy link
Owner

@sharkdp sharkdp commented May 16, 2024

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
Copy link
Owner Author

sharkdp commented Jun 3, 2024

see follow up: #443

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant