News for hackers. Stuff that matters.

A comment on Show HN: Dependently typed language for proofs that you can implement in one day. Parent comment

Re:Show HN: Dependently typed language for proofs that you c... by zozbot234 on Saturday October 02, 2021 @09:24AM (#28728366)
AIUI, the integration of linear types (or substructural types in general) with dependent typing is still a matter of research. Even "simple" type system extensions like higher-kinded types come with a lot of added complexity.

There is also what's arguably a deeper obstacle to "efficient" implementation of dependent types because dependent typing does away with the phase separation between compile-time and run-time. We do have "program extraction" features in many DT languages to mitigate this, but they're still ad-hoc additions, there isn't yet a principled approach to the issue.

[ Parent | on HN ]
Re:Show HN: Dependently typed language for proofs that you c... by AnthonBerg on Friday October 15, 2021 @04:55PM (#28883030)
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...

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.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.

[ Parent | on HN ]