The World Over Dependent Types


This was originally an answer to a Q&A website question. The question is,

Disregarding Esolang, what can we add to a PL when there’s already dependent types? Or, what extensions can be built on top of dependent type systems?

First of all, considering the three dimensions of the Lambda Cube, most PLs are already equipped with $ \lambda 2 $ (term dependent on type) and they call it polymorphism. Idris and Agda supports this too, so does Haskell with extensions. Shame on you, OCaml.

Then, $ \lambda \omega $ and $ \lambda \Pi $ usually comes together. Consider $ \lambda \Pi $, disregarding simple PLs’ (like Kotlin, Java) Type Constructors, PLs with Type Level operations like C++, Scala can all do something dependently-typedly (aka $ \lambda \Pi $), though limited (like no exhaustiveness check on sums, no termination check but limit the size of expansion).

Therefore those qualified Proof Assistants are all on the top of Lambda Cube, they have the other corners for free when supporting dependent types. There’s no much space for them to improve. So, we can see from another perspective – forget about the word 『type system』, but focus on some side features (or, add-ons) of type systems, or improve the PL industrially.

In conclusion we can see that PLs like Agda, Idris are far above dependent types.

That’s all, at least in my humble sight.

By the way, all these goodies are strongly coupled with the compile-time type checker, which means that it’s impossible in dynamic languages like JavaScript. After type-checking, things (“Views”) like refl are just a singleton. Passing it around is pointless at runtime.


Tweet this Top


This work (The World Over Dependent Types) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.