Type system extensions

[sharkdp]

This issues is a collection of notes regarding future extensions of Numbats type system.

Overview of what we have at the moment

This page in the documentation gives a rough overview.

Types

• Dimension types for dealing with physical dimensions: ¹
  • Fundamental/base dimension types (1, Length, Time, Mass, …)
  • Combinations of dimension types (Length / Time, Current × Time, …)
  • Exponentiation (Length³)
  • Type aliases for dimension types (dimension Frequency = Time^(-1))
• Base types (non-dimension types):
  • Bool
  • String
  • DateTime
  • ! ("Never"), a bottom type that we currently use to type functions like error (String -> !).
• Structs — nominally typed records like struct Pair { s: Length, t: Time }. In the PR that introduced structs, there is a discussion on whether we should have structurally typed or nominally typed records in Numbat.
• Function types
  • Example: Fn[(A, B, C) -> X] is the type of a function with parameter types A, B, C and return type X.

Type system features

• Function types (but no closures so far, see Closures #347)

  fn twice(f: Fn[(Scalar) -> Scalar], x: Scalar) = f(f(x))

• Type inference (limited, see Functions: full type inference #29)

  fn f<A, B>(a: A, c: A × B²) -> B = sqrt(c/a)
  f(2 m, 3 m s²)

• Parametric polymorphism (currently limited, see Can not infer type parameter when calling generic function from generic function #166):

  fn max<T>(a: T, b: T) -> T = if a > b then a else b

• Recursion (somewhat limited, see this page)

  fn fib(n: Scalar) -> Scalar =
    if n ≤ 2
      then 1
      else fib(n - 2) + fib(n - 1)

• Some form of compile-time evaluation ("consteval") to support exponentiation of dimension types, as explained in this article

Overview of things that we (might) want to have

Types

• We may want to distinguish between integers and floats. We may also wish to add other numerical types such as ratios or complex numbers. It is currently unclear how the syntax for these types would look like, given that we would still want to support dimension types on top. Maybe something like Length<Float>, Length<Int> with an alias Length = Length<Float>.
• List<A>, see Add a list datatype #261 and List datatype #432
• ∀A. A: polymorphic values. We need them for things like the empty list ([]: ∀A. List<A>), zero/nan/inf (∀A. A, see Zero, NaN, inf should be polymorphic #37)
• Algebraic data types to support things like Option<T>/Maybe<T>.
• If we don't have ADTs, we might at least want enums.

Type system features

• Full type inference
  • We currently only have a limited version of this.
  • We want to be able to just write fn f(x) = 10 x + 2 and have x: Scalar and f: Scalar -> Scalar be inferred.
  • Full Hindley-Milner-style type inference should be possible, see Functions: full type inference #29 and ¹
• Full Hindley-Milner-style polymorphism
  • An interesting change from standard Hindler-Milner might be to omit a generalized let, as hinted at in ²:

    While generalisation for local let bindings is straightforward in Hindley-Milner, we show that it becomes much more complicated in more sophisticated type systems. The extensions we have in mind include […] units of measure (Ken96)

• Polymorphism for all types, not just dimension types
  • Right now, a function like fn id<A>(x: A) -> A = x only works for dimension types, but not for other types like Bool, String, etc.
  • This is probably too limiting if we introduce lists, because we want list-functions to also be able to operate on List<Bool>, List<String>, etc.
  • One way to implement this would be via bounded quantification, similar to type class constraints in Haskell/Rust. We might have a constraint like Dim for dimension types, which would let us distinguish:

    fn id<A>(x: A) -> A = x    # now works on all types
    fn sqrt<A: Dim>(x: A²) -> A = x^(1/2)    # only works on dimension types
    

• Subtyping
  • mpunits has an interesting concept of "quantity kinds", which allows for a more fine-grained view on physical dimensions (or quantities). For example, a user might want to distinguish between a Width and a Height, where both would be a kind of Length. And it can be useful to build full hierarchies of those quantity/dimension kinds. Supporting something like this would require us to support some kind of subtyping where Width/Height would be subtypes of Length.
  • Subtyping might also be required if we add integer types but still want to support expressions like 1 + 0.5 where the lhs is of type Int and the rhs is of type Float. Another (potentially better) way to do this would be via type classes like Num in Haskell, where (+) :: Num a => a -> a -> a.
• Type constructors
  • To support things like ADTs

Other Ideas

• Once we have full support for parametric polymorphism, we might be able to get rid of the !/Never bottom type and instead type error as String -> ∀A. A, which is also what languages like ML and Haskell do ³

Footnotes

1. Programming Languages and Dimensions, Andrew John Kennedy, University of Cambridge, Computer Laboratory, 1996 (https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf) ↩ ↩²

2. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tldi10-vytiniotis.pdf ↩

3. Pierce, Types and Programming Languages, chapter 15.4 ↩

[sharkdp]

Most of this is now implemented, see #443. Let's discuss further extensions to the type system separately.