This is an automated archive made by the Lemmit Bot.

The original was posted on /r/programminglanguages by /u/SquareRootCable on 2024-09-15 14:38:32+00:00.

Assume a simple lambda calculus language with basic types Boolean, Integer, String. No polymorphism but a single higher-minded type that is Array[n] (or rather Matrix[m,n] - but it won’t matter since it is just a nested Array). No ‘let’, just abstraction, application and some operators (eg. mmult, dot-product, plus etc.). So basically keeping it as simple as possible but allowing matrices.

What is the simplest static type system that can deal with this? Dependently typed programming will do, but is a burden onto the programmer for proof terms are a pain not every developer can be expected to wrap their brains around. Refinement types can do it too, and would be more ergonomical but the whole SMT machinery is quite enormous compared to a dependent type system…

What is the simplest one? Both in terms of implementation but also ergonomics for the user.

Thanks for your suggestions.