sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
<sharkdp>
I'm currently working on a complete rewrite of Numbats type checker. It's based on a constraint-typing formulation of Hindley Milner. It is able to infer principal types (most general polymorphic types) for all expressions without any type annotations.
<achin>
exciting!
<sharkdp>
It's still a lot of work, but it can already solve some problems that we currently have. And do some fun things.
<sharkdp>
(1) It solves the issue that 0 is not polymorphic. It also solves the problem that we couldn't type the empty list [] previously.
<sharkdp>
With the new type system, we now have polymorphic values and "type class" constraints, similar to Haskell (or trait bounds in Rust).
<sharkdp>
However, so far, the only existing constraint is `T: Dim`, which says: `T` is a dimension type (i.e. something like 7, 2 m, or 40 m/s^2)
<sharkdp>
So `0` now has the type `forall D. Dim(D) => D`.
<achin>
i'm guessing this was mostly motivated by things like:
<achin>
!nb len([])
<Charbot9000>
Panic: Any { .. }
<sharkdp>
(Similar to how `0` has a type `forall D. Num(D) => D` in Haskell)
<achin>
despite many attempts, i have never quite been able to into haskell
<sharkdp>
Yes... and also, the limitation with zero was a bit annoying. For example:
<sharkdp>
!nb if true then 4 meter else 0
<Charbot9000>
Error: Incompatible types in condition
<sharkdp>
This will be solved with the new type checker
<achin>
so it'll resolve '0' to '0 meter' in this context?
<sharkdp>
No, it will not rewrite terms
<sharkdp>
`0` now has a polymorphic (dimension) type, so it can be added to anything
<sharkdp>
or used in then/else branches
<achin>
hmm, i'm not sure i totally follow
<sharkdp>
So if we typecheck `0 + 4 meter`
<achin>
does this mean that you could do something like "1 gram + if false 4 meter else 0" ?
<sharkdp>
no, that would still be an error!
<sharkdp>
If we typecheck `0 + 4 meter`, we first type-check both leaves of the addition operator
<sharkdp>
on the left, we have `0` with a polymorphic type. We don't know what the concrete type will be, yet. So we choose a fresh type variable for now, and say that `0` has type `T0` (for example)
<sharkdp>
then we check the left hand side, and find that `4 meter` is of type `Length`
<sharkdp>
And for the addition node, we will then enforce that the type on the left and the type on the right have to be the same.
<sharkdp>
So we record a new equality constraint `T0 ~ Length`
<sharkdp>
(which is easy to solve, later on)
<sharkdp>
for `if x then y else z`, things are similar. We add constraints that `type(x) ~ Bool` and `type(y) ~ type(z)`
<achin>
let me go back to basics with a very simple question: if "1" is a non-polymorphic type Scalar, why does "0" need to be polymorphic? why can't "0" remain a Scalar?
<sharkdp>
It could also stay a scalar, but it's not great. Mathematically, you want to have that `0 * x == x` for all x
<sharkdp>
so it is strange that you can compute `4 meter + 0 meter`, but you can't do `4 meter + 0`
<sharkdp>
Now, nobody calculates `4 meter + 0`, of course. But `0` comes up very often as an initial or default value
<achin>
i think you mean "0 * x == 0" -- do you also want "1 * X == X" for all x ?
<sharkdp>
ah, yes. sorry
<achin>
that is, should all Scalars be polymorphic in this way? or just 0 and 1?
<sharkdp>
0 should be polymorphic, 1 should not be!
<sharkdp>
`1 * X == X` will hold anyway
<sharkdp>
you can always multiply with something of type `Scalar` and still have the same type
<sharkdp>
Multiplying two quantities is always possible
<sharkdp>
but for adding/subtracting/comparing/…, they need to be of the same type
<sharkdp>
and in that case, it is helpful to have 0 polymorphic
<sharkdp>
For example: if you want to write `if x > 0 …` for a generic `x`
<achin>
that makes sense
<sharkdp>
Or imagine you want to implement `fn sum<D>(xs: List<D>) -> D`
<sharkdp>
In the future, we might be able to implement this function as `fold(0, |acc, x| acc + x)` or similar
<sharkdp>
Anyway, this polymorphic 0 thing is probably the least exciting thing about the new type checker :-)
<sharkdp>
It also solves another problem that I had when trying to implement lists: for working with lists, we often want to be generic over ALL types, not just dimension types.
<sharkdp>
`fn head<A>(xs: List<A>) -> A`
<sharkdp>
I should be able to run that on a List<String>
<sharkdp>
On the other hand, `sum` above should actually be constrained to dimension types. I should have written `fn sum<D: Dim>(xs: List<D>) -> D`.
<achin>
yeah, summing over a list of bools wouldn't make sense
<sharkdp>
What's I find more exciting: we will be able to just write `fn f(v) = (v * 1 second) + 1 meter`, and Numbat will infer the type `fn f(v: Length/Time) -> Length`
<sharkdp>
Or we can write `fn f(x, y) = x^2 + y`, and it will infer the polymorphic type `fn f<D>(x: D, y: D^2) -> D`
<triallax>
that's awesome
<achin>
is this type of inference mostly only possible with hindley-milner?
<sharkdp>
(return type in the last example should be D^2)
<sharkdp>
So Hindley-Milner is a type system for the lambda calculus (which you can think of as a very small, but powerful, functional programming language)
<sharkdp>
The interesting property of this type system is that you can always infer a type, without any annotations
<sharkdp>
And the inferred type will also be the most general type
<sharkdp>
so `fn f(x) = x` will have a polymorphic type A->A, and not just Bool->Bool (which would also be a correct type for that function)
<sharkdp>
And there is a lot of research that shows how you can extend this type system, in a way that it preserves those properties
<sharkdp>
There are also a lot of things that destroy those properties, like higher-ranked (N>2) polymorphism. Or "System F"-style polymorphism, where the "forall" quantifier can appear in other places.
<sharkdp>
But it turns out that you can generalize Hindley Milner (HM) to something called HM(X), where generic X is a constraint system.
<sharkdp>
And if X satisfies certain properties, than you still get type inference + most general types
<sharkdp>
And adding dimensions types is one of those extensions that works.
<sharkdp>
(that was already shown in the 90s by Kennedy who later went on to implement physical unit types in F#)
<sharkdp>
However, if I understand correctly, F# still needs annotations in some cases (you don't need to name the concrete dimension, but you have to say which of the variables are of dimension type)
<sharkdp>
And they chose to lift *units* to the type level, not physical dimensions
<sharkdp>
Which is a mistake, in my opinion
<sharkdp>
because you can't easily write functions like `fn kinetic_energy(mass: Mass, v: Velocity) -> Energy` without picking a concrete unit system
<sharkdp>
In Numbat, you can write this function and then use it with whatever unit system you like.
<sharkdp>
(by the way, I realize that most Numbat users will not care at all. but I find type systems fascinating)