# Is it possible to write a fully-decidable type system for the J language?

I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL). It is unclear to me whether statically typing the J language (without subtyping) without need for type annotation is possible.

Given that J's types are well-bounded not considering array dimensions (only arrays of simple types such as string, int, box, etc.), do the options below allow sound and decidable inference?:

Mutable assignment: Is giving a mutable value a union type to derive multiple ASTs and choose the appropriate AST at runtime correct? Are there better alternatives?

Polymorphism and overloading: Since J simple types are well bounded (which apparently makes Hindley-Milner compatible with function overloading), can I essentially forget about the array part i.e. type Arrayof Int becomes Int, leaving array dimension checks to the runtime?

Thanks!

• Adding a type system to J, especially one that is fully inferable requires deciding on programs you aren't going to allow. That said, for the array programming aspects of J, you will typically care about the shape of the arrays and there have been several type systems over the years to try to capture these kinds of shapes. Some (related) examples are Single Assignment C: efficient support for high-level array operations in a functional setting and Regular, shape-polymorphic, parallel arrays in Haskell. – Derek Elkins left SE Jun 9 '19 at 20:26
• For J, in particular, though, you have the bigger problem that parsing J is undecidable. If you look at the parsing table, it seems simple enough. You just need to look up the appropriate rule in the table based on the part of speech of each word. The problem is that the part of speech of a variable depends on what it has been assigned and can be mutated. In other words, part of speech is a run-time property. – Derek Elkins left SE Jun 9 '19 at 20:26
• @DerekElkins Thank you. Yes, I do understand that parsing J is undecidable. But as I understand, that just makes compilation "useless" (and not infeasible), in the sense that you have to keep all possible parse trees if your program assigns user input into a variable isn't it? So theoretically I could put all possible ASTs under a giant top-level switch statement accounting for all choice points, and require a single type hint at choice points would allow to considerably reduce the number of valid ASTs. Or am I totally lost, here? – Raoul Jun 9 '19 at 20:41
• Since you want to add a type system anyway, the simplest thing to do would be to require (directly or indirectly) that all variables maintain a consistent part of speech. I guess you could compile a branch every time a variable is used based on part of speech. This would likely lead to an exponential growth in code-size. For your purposes, this is still problematic as you would need to ensure all those branches type check and that's very unlikely to happen. – Derek Elkins left SE Jun 9 '19 at 21:01