4 ms·

Regarding your point about dimensions, it really isn't impossible; it requires a little bit of type-level mechanisms, but not very much and quite a few language

Regarding your point about dimensions, it really isn't impossible; it requires a little bit of type-level mechanisms, but not very much and quite a few languages already have it. Here are some examples in some languages. The author of Libra (which I /think/ was the first to use this technique) gave a good talk [4] on the mechanism. [1] https://to-ithaca.github.io/libra/ https://to-ithaca.github.io/libra/ (Scala) [2] https://hackage.haskell.org/package/dimensional https://hackage.haskell.org/package/dimensional (Haskell) [3] https://docs.rs/dimensioned/0.7.0/dimensioned/ https://docs.rs/dimensioned/0.7.0/dimensioned/ (Rust) [4] https://www.youtube.com/watch?v=CrwVD0Pco5Q https://www.youtube.com/watch?v=CrwVD0Pco5Q

dan-robertson 6y ago
Ok I guess I concede that it is technically possible in haskell and rust. But note that the way it works in both cases is quite hacks, relying on typeclasses with associated types (ie effectively type-level functions) to fake numbers (up to some maximum), and then representing the dimension of something as a fixed length vector of these numbers. This is fine for dimensional analysis of real world physical things I guess but as soon as you’re trying to look at dimensions of something to see if a calculation makes sense it will fail because there won’t be an appropriate slot in your vector, or will need you to reimplement or modify the hacks. I don’t think it is sustainable to need to jam that kind of trickery into every step.
- steveklabnik 6y ago
  Rust is getting real type-level numbers in a couple of weeks. It’s just the bare minimum though. More to come in the future.
  - ywei3410 6y ago
    Do you know whether there's going to be any near term support for ordering constraints (i.e. N < M) with the type-level numbers?
    - steveklabnik 6y ago
      I don't.
- ywei3410 6y ago
  I don't understand why you call it "trickery or "fake". Church encoding of natural numbers is the same technique used in Agda, Coq and Idris to represent the Peano numbers. It's a completely valid encoding and isomorphic to any other representation. You don't need to use a fixed-length array either - you can used a recursive linked list at the type-level for an unbounded encoding [1]. The Scala library is an example of that; the Github page even has an example of encoding arbitrary units like sheep and wheat. [1] https://github.com/lloydmeta/frunk https://github.com/lloydmeta/frunk
  - dan-robertson 6y ago
    The trickery here is basically pushing the type system to the extreme for relatively simple things. I wonder how the type system might cope for more complicated things. Another consequence is type errors. You won’t get something about trying to add a length to a time but rather something like “can’t unify type Pos1 with Zero,” or “error Units<f64,(z,(z,(z,(z,(s<z>,(z,()))))))> does not implement trait Add<Units<f64,(z,(z,(z,(s<z>,(z,(z,()))))))>>.” This is confusing enough in a trivial example but I wonder how this would go if the example were buried deep in the code. The encodings used in the haskell library were not a church encoding (they could only express integers between about minus 9 and 9) though to be fair they claimed to be only there until better type level literals. I don’t know about the rust implementation. Coq and Idris are quite weird languages. The reason they use Peano arithmetic at the type level is that it is easy for them to reason about. But in dependently typed languages where the type and value levels aren’t really separate, if you want to prove things about your programs, they also need to use these numbers which means you either need special language support for making them fast or you have slow programs, which is not suitable for the topic of efficient systems for computer mathematics. The other problem is that the computer can’t help much with the types and they require a lot of manually specifying things which many practitioners would consider trivial enough to be tacit. This is not good for having an expressive system for computer mathematics. Another example of a system which tried to offer better mathematical foundations is fortress. They started out as something like “fortran but better at mathematics and without so much history” and ended up with something a lot more like haskell with a typeclass-like mechanism and mostly function language. They had a lot of issues with making the type system work with mathematics (one case is that it is hard to specify that something can be a (eg) a monoid. In mathematics, it’s often obvious or said very simply, but computers aren’t so good at knowing what is obvious. It can be complicated to say eg “this is a monoid with identity 1 and operation x,” or “this is a monoid with identity 0 and operation +” because your type system needs a way to disambiguate between the two monoids (or the language will need some bad ergonomics where it is very manually expressed). If your type system ends up needing to know about the names of things and having eg type classes dispatch on the operation or something, it could become tricky.

dan-robertson 6y ago

Ok I guess I concede that it is technically possible in haskell and rust. But note that the way it works in both cases is quite hacks, relying on typeclasses with associated types (ie effectively type-level functions) to fake numbers (up to some maximum), and then representing the dimension of something as a fixed length vector of these numbers. This is fine for dimensional analysis of real world physical things I guess but as soon as you’re trying to look at dimensions of something to see if a calculation makes sense it will fail because there won’t be an appropriate slot in your vector, or will need you to reimplement or modify the hacks. I don’t think it is sustainable to need to jam that kind of trickery into every step.

steveklabnik 6y ago
Rust is getting real type-level numbers in a couple of weeks. It’s just the bare minimum though. More to come in the future.
- ywei3410 6y ago
  Do you know whether there's going to be any near term support for ordering constraints (i.e. N < M) with the type-level numbers?
  - steveklabnik 6y ago
    I don't.
ywei3410 6y ago
I don't understand why you call it "trickery or "fake". Church encoding of natural numbers is the same technique used in Agda, Coq and Idris to represent the Peano numbers. It's a completely valid encoding and isomorphic to any other representation. You don't need to use a fixed-length array either - you can used a recursive linked list at the type-level for an unbounded encoding [1]. The Scala library is an example of that; the Github page even has an example of encoding arbitrary units like sheep and wheat. [1] https://github.com/lloydmeta/frunk https://github.com/lloydmeta/frunk
- dan-robertson 6y ago
  The trickery here is basically pushing the type system to the extreme for relatively simple things. I wonder how the type system might cope for more complicated things. Another consequence is type errors. You won’t get something about trying to add a length to a time but rather something like “can’t unify type Pos1 with Zero,” or “error Units<f64,(z,(z,(z,(z,(s<z>,(z,()))))))> does not implement trait Add<Units<f64,(z,(z,(z,(s<z>,(z,(z,()))))))>>.” This is confusing enough in a trivial example but I wonder how this would go if the example were buried deep in the code. The encodings used in the haskell library were not a church encoding (they could only express integers between about minus 9 and 9) though to be fair they claimed to be only there until better type level literals. I don’t know about the rust implementation. Coq and Idris are quite weird languages. The reason they use Peano arithmetic at the type level is that it is easy for them to reason about. But in dependently typed languages where the type and value levels aren’t really separate, if you want to prove things about your programs, they also need to use these numbers which means you either need special language support for making them fast or you have slow programs, which is not suitable for the topic of efficient systems for computer mathematics. The other problem is that the computer can’t help much with the types and they require a lot of manually specifying things which many practitioners would consider trivial enough to be tacit. This is not good for having an expressive system for computer mathematics. Another example of a system which tried to offer better mathematical foundations is fortress. They started out as something like “fortran but better at mathematics and without so much history” and ended up with something a lot more like haskell with a typeclass-like mechanism and mostly function language. They had a lot of issues with making the type system work with mathematics (one case is that it is hard to specify that something can be a (eg) a monoid. In mathematics, it’s often obvious or said very simply, but computers aren’t so good at knowing what is obvious. It can be complicated to say eg “this is a monoid with identity 1 and operation x,” or “this is a monoid with identity 0 and operation +” because your type system needs a way to disambiguate between the two monoids (or the language will need some bad ergonomics where it is very manually expressed). If your type system ends up needing to know about the names of things and having eg type classes dispatch on the operation or something, it could become tricky.