3 ms·

To slightly elaborate: when this comment say "first class types" they're referring to dependent types. For programmers who are not aware: think about functions

To slightly elaborate: when this comment say "first class types" they're referring to dependent types. For programmers who are not aware: think about functions in functional programming languages. They're "first class citizens" in the sense that there is no difference between functions and any other values, such as `3` or `"hello"`. In dependently types languages, there is no difference between types and other values. Types are just any other value. For example, normally `Int` would be a type, but in these kind of programming languages `x: Int, x > 5` would also be a type even though the type depends on the value `x`. In terms of software engineering, one bonus you get is being able to encode your unittests in your type system. For example, you can do (in Agda): _ : myFunction x y z == 33 _ = refl -- refl is of type `x == x` and compiler will run this test for you at compile-time while type-checking your program. Two popular "practical" dependently typed languages are Agda and Idris. Of these two, Idris is relatively designed for software engineers, whereas Agda also wants to be a state-of-the-art automated theorem proving tool. I would strongly recommend checking both if you want to explore this area of programming languages. I wrote practical programs in Agda (e.g. language parsers, JSON parser etc) and I think it can make a programmer extremely productive, if you like this kind of workflow. Correctness is very easy to reason in these languages, and although it may look daunting at first, writing practical programs are very approachable (about as hard, maybe ever-so-slightly harder than writing code in Haskell). Have fun!

satvikpendem 4y ago
So I could also write all my code purely in the type system too, right?
- gnulinux 4y ago
  Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this would mean compilation will infinitely loop. Different languages deal with this problem differently. E.g. in Agda, there is a "safe" subset of language that is not Turing Complete such that all programs can be algorithmically proven to be halting. But you can work around this via pragmas. Speaking from experience, the safe subset of Agda is all you need to write useful programs. You just need a tiny shell (maybe only few lines of code) that will handle IO and Haskell FFI. The rest of the code will be purely functional, safe, Turing Incomplete Agda.

satvikpendem 4y ago

So I could also write all my code purely in the type system too, right?

gnulinux 4y ago
Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this would mean compilation will infinitely loop. Different languages deal with this problem differently. E.g. in Agda, there is a "safe" subset of language that is not Turing Complete such that all programs can be algorithmically proven to be halting. But you can work around this via pragmas. Speaking from experience, the safe subset of Agda is all you need to write useful programs. You just need a tiny shell (maybe only few lines of code) that will handle IO and Haskell FFI. The rest of the code will be purely functional, safe, Turing Incomplete Agda.