|
|
|
|
|
|
by peterhj
2434 days 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,+,*). |
|
|
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.