Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and

Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and many). It’s a great language. https://idris2.readthedocs.io/en/latest/updates/updates.html#new-core-language-quantities-in-types https://idris2.readthedocs.io/en/latest/updates/updates.html... The locus of the research that Idris’ linear types are based on might be Conor McBride’s paper I Got Plenty O’ Nuttin: https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.p... It’s a beautiful paper. There are other papers in between McBride’s paper and the implementation. They’re great papers too. I find it telling that the Idris 2 source code for quantitative types in the Idris 2 compiler is beautifully readable and understandable. This is what tends to happen in Idris code. Clarity.