When learning Idris with Edwin’s Type-driven Development with Idris, I read about the unique property of Idris that it’s type is a first class construct, compared to other programming languages, and especially to those who also have a dependent type system.
In the book it talks about the potential usage of such feature: database schema, network protocol description and .etc.
With these benefits, my question is two-fold:
- Is it not possible to do these tasks in a merely dependently typed language that has not first-class type?
- What is the negative point of such feature? Why are types in other systems/languages not first class (in Agda or Coq for example)? I assume that this feature introduces some theoretical limitations on what the program can check at compile time, but I don’t know what it is.
Or more concretely:
What are the examples where first-class type can be distinguished from mere dependent type?
I would like to see both some positive examples (benefits) and some negative examples (that it makes compiler difficult to do something, or some other kinds of limitations).
>Solution :
"First-class type" in the Idris book means precisely "dependent type" in the sense of Agda or Coq, so there is no distinction here at all.
GADTs in Haskell and OCaml could be viewed as a form of dependent types which does not entail first-class types in the sense of Idris. Here, there are two different programming languages, for value-level and type-level programming, and types cannot be arbitrarily mixed with values. GADTs allow dependent pattern matching, where in different branches we can learn information about type-level values. But we can’t learn information about runtime values.