3 ms·

If you find this sort of thing interesting, you might also find Remora[1], which is a dependently-typed array processing language interesting. Edit: I see the

If you find this sort of thing interesting, you might also find Remora[1], which is a dependently-typed array processing language interesting. Edit: I see the paper they wrote has a shout out to it as well. [1] http://www.ccs.neu.edu/home/jrslepak/typed-j.pdf http://www.ccs.neu.edu/home/jrslepak/typed-j.pdf also https://github.com/jrslepak/Remora/tree/master/remora https://github.com/jrslepak/Remora/tree/master/remora

peterhj 7y ago
To expand a bit, as I understand it, Remora gives a type system (and type inference) to APL- and J-style reranking, which is called rank polymorphism in Remora. The key thing is that type inference in Remora is based on Presburger arithmetic (0,+) which is decidable, unlike the stronger but overly powerful (for their purposes) than full Peano arithmetic (0,1,+,*).
- xelxebar 7y ago
  Just starting to learn J, myself, and this brings to mind Aaron Hsu's "Does APL Need A Type System?" talk: https://www.youtube.com/watch?v=z8MVKianh54 https://www.youtube.com/watch?v=z8MVKianh54 which argues that APL already provides the development ergonomics that are typically acribed to type systems. I.e. why type check your tacit function when it's implementation is about the same length as its type annotation? Anyway, as someone trained in Category Theory and a huge fan of type systems, I found Hsu's argument surprisingly pursuasive. I would love to hear any counterpoint arguments and the motivations behind attempts at giving J a type system.