4 ms·
There are lots of things which may go wrong trying to make a mathematics fit into a type system. In particular you need a particularly general typesystem. I thi
by dan-robertson 6y ago
There are lots of things which may go wrong trying to make a mathematics fit into a type system. In particular you need a particularly general typesystem. I think Julia has a better chance than haskell/rust/ml (let alone C++) because types are less rigid so functions may return values of types that are functions of the arguments. The difficulty is subtyping.
For a trivial example, the integers under addition form a group. But they also form a ring, which is that group plus a different monoid structure (and extra rules), and the real numbers form a field (two connected groups with extra structure) which meets with the ring structure of the integers. If I write an algorithm about groups, I want a way to be able to apply it to the additive or multiplicative groups of the reals. You need the ability to easily talk about forgetting extra structure but then taking results back from the simpler structure.
Another example is dimensions. It is, as far as I know, basically impossible to encode something like “force (ie mass times distance per time squared) divided by time is commensurate with current times voltage” in a type system like that in ocaml/haskell/rust (you can maybe do it with c++ but the compiler can’t check that your template is correct)
The next problem with general algorithms is that there are isomorphisms and then there are isomorphisms so things that work in mathematics (this group is cyclic and g is a generator so for my element h, there is some integer a such that g^a=h) are sometimes infeasible on computers (the process described above is trivial in integers under addition, hard in integers mod p under multiplication, and very hard in elliptic curve groups (of rank 1), even though they are all cyclic).
I don’t think these are reasons not to try and I think Julia feels like a good language for a combination of performance and interface ergonomics, as well as the library being useful in the ecosystem of other scientific or mathematical libraries.
- ywei3410 6y agoRegarding 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 agoOk 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 agoRust 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 agoDo 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 agoI don't.
- ywei3410 6y agoI 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