15 ms·

This is one of my two favorite books in The Little <X>er series. The other is The Reasoned Schemer. The Little Typer provides an introduction to dependent type

by ekidd 4y ago

This is one of my two favorite books in The Little <X>er series. The other is The Reasoned Schemer. The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Two interesting languages using dependent types are: - Idris. This is basically "Haskell plus dependent types (and minus lazy evaluation)": https://www.idris-lang.org/ https://www.idris-lang.org/ - ATS. This is a complex systems-level language with dependent types: http://www.ats-lang.org/ http://www.ats-lang.org/ This fills a niche (vaguely) similar to Rust and Ada Spark, with a focus on speed and safety. The Reasoned Schemer shows how to build a Prolog-like logic language as a Scheme library. This is a very good introduction to logic programming. And the implementation of backtracking and unification is fascinating. (Unification is a powerful technique that shows up in other places, including type checkers.) This is an excellent series overall, but these two books are especially good for people who are interested in unusual programming language designs. I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating.

sixbrx 4y ago
For others: I think what was meant was "The Reasoned Schemer": https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/ https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/
- ekidd 4y ago
  Fixed. Thank you!
haskellandchill 4y ago
> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages I do, these are low hanging fruits for improving software engineering practices.
- ekidd 4y ago
  Here's my reasoning on why dependent types may still be a couple of language generations from the mainstream: - Dependent types are hard to retrofit onto an existing language. (Retrofitting generics has had very mixed results, and dependent types are likely harder to retrofit?) - It takes a good 10 years for a new language to really hit the mainstream, even if everything goes right. (This could change if a big player pushes a language.) - All type systems represent a tradeoff, "Roughly how much extra confidence can I get in this program, and for how little extra time spent learning and coding?" Dependent types give you some very interesting new guarantees, but they require picking up new skills. But a future language in this space might make these tradeoffs more appealing! - I'm not sure that any of the existing dependently-typed languages have hit the magic combination of features and tools that would be needed to break out. In the nearer term, I can imagine dependent typing showing up in at least two niches: 1. If you're currently writing extremely high-assurance software, the sort of thing where you write a proof in Coq and then use that to generate C code, then something similar to Idris might be a win. Ditto for some people using model-checker tools like TLA+? 2. I could imagine a dependent type system being "bolted on" to unsafe Rust to formally verify correctness of code that regular Rust can't verify. This might require using Rust attributes and an external tool. But I could see it happening if somebody loved the The Little Typer and wanted an ambitious thesis project, for example. But even though I don't expect dependent types to go mainstream in the next 5-10 years, they're one of those ideas than might occasionally contribute a major inspiration to a challenging project.
  - ajross 4y ago
    > Dependent types are hard to retrofit onto an existing language. Dependent types are hard to retrofit onto existing problems. Software everywhere wants to work with data of indeterminate size/parametrization at runtime. You want your system that tracks inventory stock to work with three warehouses or four, etc... Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Obviously that's all "solvable", but not in a way that matches the intuition of generations of hackers who have been building these systems. It's in some sense analogous to Haskell's "Death by a Thousand Monad Tutorials". At some point you just have to recognize that this isn't the right metaphor for the problem areas it's trying to address and move on.
klabb3 4y ago
> [Dependent types] can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". As a curious bystander, what else? When are dependent types useful in practice? How do they fit into software development practices such as testing and DRY? As an example of what I'm looking for, I see regular static typing as a way to move a class of runtime errors to compile time errors, increasing your confidence in aspects that otherwise would need repetitive unit tests.
- Warwolt 4y ago
  Dependent types allow for more nuanced statements made by types. You can for instance have a lists that are sorted in ascending order as a type, or implement messaging protocols at the type level where you can only construct a reply in the message exchange if you've received the correct preceding message. It's very cool, but it's very expensive to compile, which is why it's still research stuff, I believe.
  - kaba0 4y ago
    Not only “compile expensiveness”, but you quite literally have to prove your types in the program, which is seldom easy. E.g. if you were to write a merge sort, and have it in the type that it will output a sorted array, you will have a very hard time actually proving it correct, akin to algorithm analysis. Though to be fair most dependent typed languages allows for types without proofs, and having it in the type that an array is sorted for example can be valuable even without formal verification.
- gdprrrr 4y ago
  One example I like is a binary search Funktion which only allows to pass a sorted list
  - kaba0 4y ago
    Well, you can do that in traditional languages as well, just wrap your list in a SortedArray type. Chances are your “sorted” function won’t actually prove the algorithm used formally either in a dependently typed language.
PaulHoule 4y ago
I think variants of Datalog have some traction https://en.wikipedia.org/wiki/Datalog https://en.wikipedia.org/wiki/Datalog full Prolog though is not that great of a language. At first it looks clever that you can write imperative code by taking advantage of the implementation but it's actually really awkward. It was hoped that you could parallelize Prolog but you can't unless you weaken the language and make it even more awkward.
jjtheblunt 4y ago
> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating. why have an expectation one way or the other? the sophistication of compile-time analyses added to, e.g., Rust seems a plausible place such might appear.
wk_end 4y ago
> It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Not sure what you mean here - Coq is a proof tool _based on_ dependent types. It's a dependently typed programming language with a mechanism for constructing proof terms in an (arguably) more pleasant or natural way bolted on top.
- Jtsummers 4y ago
  They probably mean that bringing dependent types into a programming language, proper, partially obviates the need for Coq and similar systems since it renders them (at least partially) redundant. Having dependent types, and having mechanics in-language to produce proofs, would cover a large part of what people (who are producing programs and not focused strictly on the theorem proving side for other purposes) are using Coq & others for.

by ekidd 4y ago

sixbrx 4y ago

For others: I think what was meant was "The Reasoned Schemer": https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/ https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/

ekidd 4y ago
Fixed. Thank you!

haskellandchill 4y ago

> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages I do, these are low hanging fruits for improving software engineering practices.

ekidd 4y ago
Here's my reasoning on why dependent types may still be a couple of language generations from the mainstream: - Dependent types are hard to retrofit onto an existing language. (Retrofitting generics has had very mixed results, and dependent types are likely harder to retrofit?) - It takes a good 10 years for a new language to really hit the mainstream, even if everything goes right. (This could change if a big player pushes a language.) - All type systems represent a tradeoff, "Roughly how much extra confidence can I get in this program, and for how little extra time spent learning and coding?" Dependent types give you some very interesting new guarantees, but they require picking up new skills. But a future language in this space might make these tradeoffs more appealing! - I'm not sure that any of the existing dependently-typed languages have hit the magic combination of features and tools that would be needed to break out. In the nearer term, I can imagine dependent typing showing up in at least two niches: 1. If you're currently writing extremely high-assurance software, the sort of thing where you write a proof in Coq and then use that to generate C code, then something similar to Idris might be a win. Ditto for some people using model-checker tools like TLA+? 2. I could imagine a dependent type system being "bolted on" to unsafe Rust to formally verify correctness of code that regular Rust can't verify. This might require using Rust attributes and an external tool. But I could see it happening if somebody loved the The Little Typer and wanted an ambitious thesis project, for example. But even though I don't expect dependent types to go mainstream in the next 5-10 years, they're one of those ideas than might occasionally contribute a major inspiration to a challenging project.
- ajross 4y ago
  > Dependent types are hard to retrofit onto an existing language. Dependent types are hard to retrofit onto existing problems. Software everywhere wants to work with data of indeterminate size/parametrization at runtime. You want your system that tracks inventory stock to work with three warehouses or four, etc... Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Obviously that's all "solvable", but not in a way that matches the intuition of generations of hackers who have been building these systems. It's in some sense analogous to Haskell's "Death by a Thousand Monad Tutorials". At some point you just have to recognize that this isn't the right metaphor for the problem areas it's trying to address and move on.

klabb3 4y ago

> [Dependent types] can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". As a curious bystander, what else? When are dependent types useful in practice? How do they fit into software development practices such as testing and DRY? As an example of what I'm looking for, I see regular static typing as a way to move a class of runtime errors to compile time errors, increasing your confidence in aspects that otherwise would need repetitive unit tests.

Warwolt 4y ago
Dependent types allow for more nuanced statements made by types. You can for instance have a lists that are sorted in ascending order as a type, or implement messaging protocols at the type level where you can only construct a reply in the message exchange if you've received the correct preceding message. It's very cool, but it's very expensive to compile, which is why it's still research stuff, I believe.
- kaba0 4y ago
  Not only “compile expensiveness”, but you quite literally have to prove your types in the program, which is seldom easy. E.g. if you were to write a merge sort, and have it in the type that it will output a sorted array, you will have a very hard time actually proving it correct, akin to algorithm analysis. Though to be fair most dependent typed languages allows for types without proofs, and having it in the type that an array is sorted for example can be valuable even without formal verification.
gdprrrr 4y ago
One example I like is a binary search Funktion which only allows to pass a sorted list
- kaba0 4y ago
  Well, you can do that in traditional languages as well, just wrap your list in a SortedArray type. Chances are your “sorted” function won’t actually prove the algorithm used formally either in a dependently typed language.

PaulHoule 4y ago

I think variants of Datalog have some traction https://en.wikipedia.org/wiki/Datalog https://en.wikipedia.org/wiki/Datalog full Prolog though is not that great of a language. At first it looks clever that you can write imperative code by taking advantage of the implementation but it's actually really awkward. It was hoped that you could parallelize Prolog but you can't unless you weaken the language and make it even more awkward.

jjtheblunt 4y ago

> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating. why have an expectation one way or the other? the sophistication of compile-time analyses added to, e.g., Rust seems a plausible place such might appear.

wk_end 4y ago

> It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Not sure what you mean here - Coq is a proof tool _based on_ dependent types. It's a dependently typed programming language with a mechanism for constructing proof terms in an (arguably) more pleasant or natural way bolted on top.

Jtsummers 4y ago
They probably mean that bringing dependent types into a programming language, proper, partially obviates the need for Coq and similar systems since it renders them (at least partially) redundant. Having dependent types, and having mechanics in-language to produce proofs, would cover a large part of what people (who are producing programs and not focused strictly on the theorem proving side for other purposes) are using Coq & others for.