4 ms·

Are there any type systems that work well for the array programming problem domain? Not the kind of ‘everything is an operator’ syntactic sugar, to be clear. Mo

Are there any type systems that work well for the array programming problem domain? Not the kind of ‘everything is an operator’ syntactic sugar, to be clear. More things like supporting the kind of general operators you see in array languages while also expressing the constraints on dimensions, eg for matrix multiplication you need the number of columns on the left to match the number of rows on the right. But the thing written at the end of this post presumably also does things on arrays of higher rank too…

zozbot234 3y ago
You basically need types that can depend on program constants (like the size of an array) and to be able to do compile-time computation on these constants. These are emerging features of sorts, but languages like C++ and Rust support them. They're also inherent to dependently-typed languages. (Of course you can alternately pick array sizes at runtime, but then you'll be dependent on a runtime check wrt. correctness.)
- dan-robertson 3y ago
  Surely most of the time you don’t need program constants? You could already implement a slow matrix multiplication that is well typed in a language like Haskell or OCaml. It would have a type something like: val matmul : ((float,'a) fixed_length, 'b) fixed_length -> ((float,'c) fixed_length, 'a) fixed_length -> ((float,'c) fixed_length, 'b) fixed_length (And observe the similarity to function composition too: val compose : ('a -> 'b) -> ('c -> 'a) -> ('c -> 'b) .) This could work for dimensions that are unknown at runtime for Haskell or OCaml as their polymorphic functions can be implemented by a single machine code function where C++ templates / Rust generics must monomorphize (generate different machine code functions for different types). You would probably want existential types (though OCaml and Haskell have them). I think the problems are more things like: - that type only works on matrices, you can’t so easily express that eg * in APL works on two scalars, or two vectors of the same length, or a matrix and a rank-3 array so long as their dimensions line up appropriately. - handling operations that change lengths is hard: concat probably wants you to be able to unify through certain arithmetical expressions, and the filter operation (take an vector and a bitvector the same length, and produce the vector of elements where the bit was set) means you probably want a natural way to handle those kinds of existential types for lengths: you get a vector, and it has a length, but you’re not sure what it is.
mlochbaum 3y ago
There's a fundamental opposition between the functional programming approach to types and array programming principles, as I see it. In functional programming (particularly Haskell), types are used to make fine distinctions for safety. Even if an existing type would work for something, it's often recommended to make a new one so two different use cases don't get mixed up. But the APL family works to make as few type distinctions as possible: everything is an array, booleans are numbers, and some k features are to unify multi-dimensional arrays with nested ones and sort-of-unify (it's complicated) functions, dicts, and arrays. The reason to do this is that it allows one function to do more things. As you guessed, the matmul function from the tutorial works if the right argument has rank 1 or more, which means it also does matrix-vector products. Less code is another form of safety, the theory goes. And handling more things with the same function also lets you draw higher-level connections. Of course you can type the arrays anyway. Remora is one attempt. To me it feels like just a technical exercise and I think this question calls for more high-level investigation of what exactly the goals are before jumping into PL theory details. EDIT: Tali Beynon's rainbow arrays don't have all the answers, but I think they're a good example of the sort of investigation I mean: https://math.tali.link/classical-array-algebra/ https://math.tali.link/classical-array-algebra/
- dan-robertson 3y ago
  I want a type system that can reject attempts to add a vector of length 3 to a matrix of size 4x5. And I would want it to allow writing a single type for + rather than the way that Julia (iirc) handles these cases where there are various methods and the rules of method selection are applied to construct the effective method that does the right broadcasting.
- Twey 3y ago
  This isn't really a fundamental disagreement. If we think of array functions as functions `Array<Index1, Element1> → Array<Index2, Element2>`, then essentially all you need to be able to say is that a function is generic over `Index1` and calculates some output index type `Index2` as a function of `Index1`. This is perfectly possible to do with Rust traits or Haskell type classes (although not all that ergonomic).
thesz 3y ago
> Are there any type systems that work well for the array programming problem domain? Do a search for "haskell strongly typed tensor programming."
- tome 3y ago
  Or just look at Orthotope: https://hackage.haskell.org/package/orthotope https://hackage.haskell.org/package/orthotope "Multidimensional arrays inspired by APL"
  - dan-robertson 3y ago
    I don’t understand how to express the type of + with the shaped api. The examples are either operating on equal shapes or take advantage of fromInteger to multiply by a scalar. One could write eg add x y = broadcast x + broadcast y, but that now allows + to output arrays with arbitrary extra outer dimensions, whereas an apl + rejects some inputs but has an output shape that is a deterministic function of the input shapes
    - tome 3y ago
      If you tell me what + should do then maybe I can help. Does it broadcast to the higher-dimensional of the two arguments?
Twey 3y ago
A really nice approach to this I've seen recently is Google's research on [Dex](https://github.com/google-research/dex-lang https://github.com/google-research/dex-lang).

zozbot234 3y ago

You basically need types that can depend on program constants (like the size of an array) and to be able to do compile-time computation on these constants. These are emerging features of sorts, but languages like C++ and Rust support them. They're also inherent to dependently-typed languages. (Of course you can alternately pick array sizes at runtime, but then you'll be dependent on a runtime check wrt. correctness.)

dan-robertson 3y ago
Surely most of the time you don’t need program constants? You could already implement a slow matrix multiplication that is well typed in a language like Haskell or OCaml. It would have a type something like: val matmul : ((float,'a) fixed_length, 'b) fixed_length -> ((float,'c) fixed_length, 'a) fixed_length -> ((float,'c) fixed_length, 'b) fixed_length (And observe the similarity to function composition too: val compose : ('a -> 'b) -> ('c -> 'a) -> ('c -> 'b) .) This could work for dimensions that are unknown at runtime for Haskell or OCaml as their polymorphic functions can be implemented by a single machine code function where C++ templates / Rust generics must monomorphize (generate different machine code functions for different types). You would probably want existential types (though OCaml and Haskell have them). I think the problems are more things like: - that type only works on matrices, you can’t so easily express that eg * in APL works on two scalars, or two vectors of the same length, or a matrix and a rank-3 array so long as their dimensions line up appropriately. - handling operations that change lengths is hard: concat probably wants you to be able to unify through certain arithmetical expressions, and the filter operation (take an vector and a bitvector the same length, and produce the vector of elements where the bit was set) means you probably want a natural way to handle those kinds of existential types for lengths: you get a vector, and it has a length, but you’re not sure what it is.

mlochbaum 3y ago

There's a fundamental opposition between the functional programming approach to types and array programming principles, as I see it. In functional programming (particularly Haskell), types are used to make fine distinctions for safety. Even if an existing type would work for something, it's often recommended to make a new one so two different use cases don't get mixed up. But the APL family works to make as few type distinctions as possible: everything is an array, booleans are numbers, and some k features are to unify multi-dimensional arrays with nested ones and sort-of-unify (it's complicated) functions, dicts, and arrays. The reason to do this is that it allows one function to do more things. As you guessed, the matmul function from the tutorial works if the right argument has rank 1 or more, which means it also does matrix-vector products. Less code is another form of safety, the theory goes. And handling more things with the same function also lets you draw higher-level connections. Of course you can type the arrays anyway. Remora is one attempt. To me it feels like just a technical exercise and I think this question calls for more high-level investigation of what exactly the goals are before jumping into PL theory details. EDIT: Tali Beynon's rainbow arrays don't have all the answers, but I think they're a good example of the sort of investigation I mean: https://math.tali.link/classical-array-algebra/ https://math.tali.link/classical-array-algebra/

dan-robertson 3y ago
I want a type system that can reject attempts to add a vector of length 3 to a matrix of size 4x5. And I would want it to allow writing a single type for + rather than the way that Julia (iirc) handles these cases where there are various methods and the rules of method selection are applied to construct the effective method that does the right broadcasting.
Twey 3y ago
This isn't really a fundamental disagreement. If we think of array functions as functions `Array<Index1, Element1> → Array<Index2, Element2>`, then essentially all you need to be able to say is that a function is generic over `Index1` and calculates some output index type `Index2` as a function of `Index1`. This is perfectly possible to do with Rust traits or Haskell type classes (although not all that ergonomic).

thesz 3y ago

> Are there any type systems that work well for the array programming problem domain? Do a search for "haskell strongly typed tensor programming."

tome 3y ago
Or just look at Orthotope: https://hackage.haskell.org/package/orthotope https://hackage.haskell.org/package/orthotope "Multidimensional arrays inspired by APL"
- dan-robertson 3y ago
  I don’t understand how to express the type of + with the shaped api. The examples are either operating on equal shapes or take advantage of fromInteger to multiply by a scalar. One could write eg add x y = broadcast x + broadcast y, but that now allows + to output arrays with arbitrary extra outer dimensions, whereas an apl + rejects some inputs but has an output shape that is a deterministic function of the input shapes
  - tome 3y ago
    If you tell me what + should do then maybe I can help. Does it broadcast to the higher-dimensional of the two arguments?

Twey 3y ago

A really nice approach to this I've seen recently is Google's research on [Dex](https://github.com/google-research/dex-lang https://github.com/google-research/dex-lang).