3 ms·

It is probably pretty presumptuous to assume, but I think that a lot of programmers that have only every been exposed to C/C++/C#, Java and Python have basicall

by fho 5y ago

It is probably pretty presumptuous to assume, but I think that a lot of programmers that have only every been exposed to C/C++/C#, Java and Python have basically no concept of what a good type system can do for them. Two examples from the top of my head: 1. Encoding matrix sizes into the data- and function-types, so that you can safely have a function `mat[c,b] mat_mult(mat[a,b] a, mat[c,d] b)` or even `mat[w-2,h-2] convolve(mat[w,h] input, mat[3,3] kernel)` and have the compiler check that you never use a matrix of the wrong size. 2. Actually checking the correctness of your implementation. There is a very nice online demo of Liquid Haskell [1], where they defined the properties of ordered lists (each element has to be smaller or equal to the one before, line 119). Then they define a function that takes an (unordered) list and spits out a ordered one by applying a simple quicksort. Now, if you break the algorithm (e.g. flip the < in line 193) and run Check, the compiler will tell you that you messed up your sorting algorithm. Pretty neat. edit: I just realized that LiquidHaskell is almost 10 years old. Sad to see that basically nothing made it into "production". [1] http://goto.ucsd.edu:8090/index.html#?demo=Order.hs http://goto.ucsd.edu:8090/index.html#?demo=Order.hs

mratsim 5y ago
For example one, it works for signal processing or graphics but compile-time dimensions are unusable in Machine Learning or Numerical Computing because it's too much friction on serialization/deserialization and some operations that reduce dimension or rank are based on runtime data (for example some dimensions are 1)
- fho 5y ago
  Sure, but this approach generalizes quite well. Especially in ML you have have a lot of matrices, many of them of known size (e.g. convolution kernels). Also, while it looks like the matrix sizes have to be known at compile time, this is not the case. You are still free to use the same matrix types with dynamic sizes (or even mix them, useful for said convolutions). In Haskell there that is achieved by using a "KnownNat", basically you elevate an integer from the value into the type level during run-time.

by fho 5y ago

mratsim 5y ago

For example one, it works for signal processing or graphics but compile-time dimensions are unusable in Machine Learning or Numerical Computing because it's too much friction on serialization/deserialization and some operations that reduce dimension or rank are based on runtime data (for example some dimensions are 1)

fho 5y ago
Sure, but this approach generalizes quite well. Especially in ML you have have a lot of matrices, many of them of known size (e.g. convolution kernels). Also, while it looks like the matrix sizes have to be known at compile time, this is not the case. You are still free to use the same matrix types with dynamic sizes (or even mix them, useful for said convolutions). In Haskell there that is achieved by using a "KnownNat", basically you elevate an integer from the value into the type level during run-time.