I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover.
lookup : (a : array) -> (n : int if 0 <= n < length(a)) -> whatever
In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependent types, but possibly restricted in some way. Can you explain the restrictions you have in mind to clarify (and motivate) the relationship between full dependent types and your refined ones? Is it something purely syntactic like "linear arithmetic only" (as I believe was the case for Liquid Types, at least originally) to ensure decidability?
Edit: Even the very first sentence of the very first paper about Liquid Types (the base of Liquid Haskell) talks about dependent types: "We present Logically Qualified Data Types, abbreviated to
Liquid Types, a system [...] to automatically infer dependent types precise enough to prove a variety of safety properties." (emphasis mine)
Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math").
The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up.
Dependent types: everything is proved, by hand, by the user, who has to build up the whole program from basic blocks. Usually the "foundation" is taken to be some kind of type theory, either Martin-Löf Type Theory or more recently Homotopy Type Theory, which has some complexities (e.g. multiple types of equality) and limitations (e.g. languages cannot be Turing complete) that I don't really understand. "Pi types" abound. I'm not sure how much of this description really is fundamental about Type Theory, and how much is just due to the specifics of the implementations I've seen (Coq, Agda, Idris).
Refined types: start with a program and add some assertions about the values (and possibly functions, but this can then get more complicated) in the program. The idea is that many of these can ideally be proven by automated SMT solvers, which support some "theories" (e.g. natural numbers, real numbers, bitfields (i.e. machine integers and floating point numbers), algebraic datatypes) and can prove some statements in these theories. As you mentioned, "linear arithmetics", along with "real number algebra", are complete and decidable theories, so in theory you should be able to prove anything about them, but I'm guessing that in practice you'd still want some timeout parameter on your SMT solver (like in type systems, where there are exponential edge cases, that thankfully don't arise often in practice), but they aren't very useful, so hopefully you can prove more than that, using the heuristics embedded into SMT solvers (e.g. you should be able to prove many non-linear properties of two-dimensional loops by lifting integers into reals). If the solver is unable to solve something, the programmer can still add hints (but this quickly gets complicated).
A concrete difference would be, in dependently-typed language, you define a list type as
type List a n =
| Nil : List 'a 0
| Const : a -> List a n -> List a (n + 1)
in a language with refined types, you can add length afterwards:
type List a = <... whatever ...>
property length : List a -> Nat
And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things.
Not sure if this makes a lot of sense, I haven't looked into this in a while and am also not aware of the most recent research in these fields. Hopefully someone can explain better!
> Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really understand …
One sentence summary that glosses over a lot of things:
In a dependently typed language, types can contain programs, and we want typechecking to terminate.
You may also want to read how the author of Idris explains partial and total functions:
OK, I think I see where you're coming from. I don't think the distinction you make is a useful one.
> A concrete difference would be, in dependently-typed language, you define a list type as [...]
Coq is a dependently typed language, and while it has a definition like this for some thing (called vector, maybe? I forget), the definition for lists in the standard library is not dependent, and length is a separate function. You can still write a function like
Fixpoint lookup (xs: list a) (idx: {n: nat | n < length xs}): a := ...
I don't know how much experience you have with dependently typed languages, but it looks like you might have misunderstood tutorials showing that one can define a dependent list type as saying that one must define lists dependently?
> And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things.
Treating it as uninterpreted is quite weak. It allows you to prove simple callers of the lookup function, but not the implementation. Also, you would not be able to prove something like this:
if idx < length xs then
lookup (Cons foo xs) (idx + 1)
else
...
This is admittedly a silly example, but it should be provable. But you can only do that if you can reason about the relationship between length and Cons.
As for automating proofs, I very very much agree that we need a lot more automation. But if that means crippling our theories to an extend that they are no longer expressive enough to verify our software, not much is won.
The problem I have is that it's not so obvious to the human reader which things are automatically provable. Constraint solvers are often surprisingly good, and occasionally surprisingly bad, so I'm constantly scared of getting into a "it's working, don't touch it" situation where seemingly simple changes make code stop working.
We're constantly told that traditional typechecking is very limited compared to other forms of formal analysis. But I've always found dependent type systems are enough to express the relevant business constraints, and making the actual typechecking stage trivial seems very worthwhile.
Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...
> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove.
"Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies.
> Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc).
You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems.
> So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...
Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
> Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
> All practical languages (even Rust and Haskell) fail for "division by zero"
Well, they don't have dependent types. In something like Idris you can do safe natural division.
> most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks.
The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).
> 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"?
Type declarations that are sometimes wrong can be misleading enough that I find code with them harder to work on than code with no types at all, personally.
> 2) What's the big pain ("all the pain") in static strong typing?
It's not a huge pain, but adding and maintaining types does have a cost (particularly when tooling support is limited).
> 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?
Because you can't trust the types to be correct in any given piece of code. You end up having to do all the things you would have to do in an untyped languge (high test coverage, carefully rechecking all the types when debugging issues, etc.).
That's not gradual typing, just the most common implementation of gradual typing (e.g. in Dart, TypeScript, Python, but not e.g. in Clojure and Perl 6 AFAIK). Although maybe this is just a "no true Scotsman" argument...
Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations:
This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more.
> Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast.
This is an explainabrag which is also wrong: languages without these features can also have "clean, maintainable code" and nothing about this list implies "runs fast."
> Memory unsafe languages, such as C, lead to the worst sort of bugs and security vulnerabilities (buffer overflows and memory leaks).
Is a memory leak meant to be the "worst sort of bug" or a "security vulnerability?"
The implication is that memory-safe languages do not have memory leaks, which is completely false. Haskell is particularly prone to "space leaks" due to its laziness.
> Memory safe languages form two groups: the ones that rely on a garbage collector, and Rust.
What a profoundly dismissive attitude. Why bring up Cyclone and not, say, Swift? Or is Swift meant to be included in "garbage collected languages?"
> Dynamically typed (or, rather, unityped)
No these are not the same and this is an absurdly wrong conflation. Dart, Objective-C, TypeScript, and others are dynamically typed languages with static type checking. You can't "or rather" this distinction away.
The author rushes past real-world facts to get to the architecture-astronaut rocket ship, solving type-theoretical problems and pretending it's an engineering exercise. Blast off, I guess.
It only reads like a troll piece because you are deliberately taking his statements in an adversarial context. It's weird to complain about the tone of other posts, and then go on to write a comment like yours.
> This is an explainabrag which is also wrong: languages without these features can also have "clean, maintainable code" and nothing about this list implies "runs fast."
I agree with you here. However, I would also agree with the claim that Haskell is simple at its core. It's simple in a mathematical sense, and that doesn't imply that the language is easy to understand or that such simplicity offers all kinds of advantages other languages lack.
> The author rushes past real-world facts to get to the architecture-astronaut rocket ship, solving type-theoretical problems and pretending it's an engineering exercise. Blast off, I guess.
The author writes a small inaccurate section on the current state of affairs, before writing a very well-explained piece on how to get GHC to be better dependently typed.
Dependent types are not something you care about, so its quite obvious why you are only responding to a small preface section of the post, while dismissing the meat of it as "solving type-theoretical problems".
I assure you that dependent types, how to get there, are very important to a large number of people. An inaccurate preface doesn't take away from, or affect, this exercise.
I wish other readers reading this comment take time to read the bulk of the article, if they are interested in dependent types(or want to learn about it).
It is very well written and explained, and it is not a comparative study of mainstream languages with Haskell, in case you get that impression from the other comments here.
If you want to engage productively, remember that people tend to say things they think are true, so look for a way to read it that makes sense rather than going out of your way to find a way to read it that makes it false. (I guess nitpicking the phrasing for a "middlebrow dismissal" is the best way to get upvotes here nowadays).
> nothing about this list implies "runs fast."
It doesn't imply it, but it enables it; read "allow" that way.
> Is a memory leak meant to be the "worst sort of bug" or a "security vulnerability?"
Maybe the one that makes sense rather than the one that doesn't make sense.
> The implication is that memory-safe languages do not have memory leaks, which is completely false.
There's no such implication, only that memory-unsafety leads to memory leaks, which is true.
> Or is Swift meant to be included in "garbage collected languages?"
Yes it is.
> No these are not the same and this is an absurdly wrong conflation.
They are the same; traditional dynamic typing is exactly unityping. That it's possible to combine dynamic typing with other things just means that alternatives are possible, not that dynamic typing is something different.
> > The implication is that memory-safe languages do not have memory leaks, which is completely false.
> There's no such implication, only that memory-unsafety leads to memory leaks, which is true.
If we're going to read in the spirit of "looking for a way to read things that make sense rather than going out of your way to find a way to read it that makes it false"...
It does reference counting, but it's not mark-and-sweep stop the world reference counting. It's as garbage collected as shared_ptr<T> and doesn't try to collect cycles. Feels a bit weird to put that under the same bucket as Java.
Any CS book on garbage collection algorithms worth its place on a good paper bibliography, places reference counting among the possible implementations of garbage collection.
What the common dev without compiler background knowledge calls GC is actually named as tracing GC on CS literature.
Academically, both reference counting (C++, Swift, some patterns in Rust) and tracing garbage collection (Java, C#) fall under the umbrella of garbage collection.
The important distinction, then, is obligate garbage collection. Can I write a substantial program that does, and needs, no garbage collection of any kind? In C++ and Rust, yes, trivially, every day.
The distinction matters because without obligate GC, you get the benefit of destructors (or in Rust, the Drop trait), and have the tool for resource management of every kind, usually written "}". Reference counting GC is rarely used in well-designed C++ and Rust programs, simply because there is rarely any need for it. Reliance on shared_ptr or ARC is recognized as a disease of forced Java converts.
T.b.h. I skimmed the "Haskell is the best" part and read just through the "Can we get performance of Haskell with the type-features of Agda without sacrificing the ergonomics of either?" and found it informative :)
My goal here was to show that standard Haskell boils down to a small set of features, therefore it's a simple language. Surely, "simple" does not imply "good" (Brainfuck is also simple), so I then assert that the combination of features that Haskell consists is fertile soil for writing maintainable and performant code.
> languages without these features can also have "clean, maintainable code"
Some people may prefer ML modules to type classes, sure. As to the other features, I have a hard time imagining a clean codebase in a language without some form of polymorphism, first class functions, and algebraic data types. (And lazy evaluation is a great addition to the list). Perhaps there are other sweet spots in the language design space, but I have not seen them yet.
> and nothing about this list implies "runs fast."
> Is a memory leak meant to be the "worst sort of bug" or a "security vulnerability?"
It's often hard to debug, and it means that the program can't be running for a long period of time. I suppose I should've used a better example, e.g. "use-after-free", to highlight the dangers of manual memory management.
> Haskell is particularly prone to "space leaks" due to its laziness.
Space leaks are benign compared to memory leaks in that the memory is eventually freed. That said, I'd be happy to have some sort of static analysis to prevent them.
> Why bring up Cyclone and not, say, Swift? Or is Swift meant to be included in "garbage collected languages?"
Swift relies on automatic reference counting, which is similar to garbage collection in that it isn't done by the programmer and has a runtime performance cost. Remarkably, it seems to be worse on both accounts: the cost of decrementing/incrementing these counters is very real, and handling reference cycles is not automatic (you need to carefully use weak references).
Rust, on the other hand, offers a static analysis with no runtime performance overhead to manage memory safely.
> dynamically typed languages with static type checking
You're talking about gradually typed languages. Sure, these are not unityped, but they also not purely dynamically typed (you said it yourself – they have static type checking). Perhaps that's just a difference between our uses of the term "dynamically typed" and we don't have a true disagreement here?
By the way, Haskell can do that too, we have the `Dynamic` type right in the `base` package.
> the cost of decrementing/incrementing these counters is very real
Only true if you use pervasive reference counting, with atomic updates. Swift essentially does this, but other languages don't.
One of the reasons why it makes sense to single out tracing GC (as opposed to RC) is that it's essentially a package deal; your whole program needs to be structured to use memory as essentially an in-RAM database, where every single object or reference can be traced after the fact at some arbitrary time in the future. (There are reasons to do this in some cases, even in 'low-level' languages which are not ordinarily garbage collected - see e.g. the use of "entity component systems" in such languages - but it's obviously not a generally-appropriate solution in any real sense!). RC is self-contained, and it need not even be locally inefficient.
> You're talking about gradually typed languages.
Interestingly, gradual typing does seem to end up with a "worst of both worlds"-type situation - the dynamic tag checks and conversions that have to be inserted at every boundary between statically- and dynamically-typed parts of the program introduce pervasive inefficiency, which is only resolved when static typing is used essentially throughout.
The term for languages like Swift, Java, and Haskell is "obligate GC". The cost of obligate GC is only superficially just the poor memory locality, interruptions, and bad citizenship -- worse is that the power of destructors is denied you, and with it the power to automate managing every other kind of resource.
> worse is that the power of destructors is denied you, and with it the power to automate managing every other kind of resource.
These are orthogonal concerns. Plenty of languages without GC do not have good support for ARM (e.g. C), and a GCed language can still have good support for ARM (e.g. monadic regions in Haskell). C++ is really the only language that conflates the two, and IME its RAII style is overrated in practice (there are a lot of rules you have to follow to avoid leaking, and for many of them you get very little warning if you break it).
> I have a hard time imagining a clean codebase in a language without some form of polymorphism, first class functions, and algebraic data types
You don't have any definition of 'clean', so maybe you mean something precise or maybe you don't, but I have seen clean codebases in all kinds of languages - C, C++, Go, Java. The language doesn't dictate whether your code is clean or not, the programmer does.
Bad programmers will write bad code in any language, but in some languages even the best programmers will struggle to write good code. E.g. I've found even the best C tends to look quite cluttered, because the lack of first-class functions forces the programmer to thread state through "by hand", and the lack of polymorphism means the programmer can't clearly separate the what from the how but has to interleave the two. (Indeed I would say bad C can sometimes look superficially cleaner: things like using global variables for state remove some of the clutter, but ultimately the cure is worse than the disease)
I love haskell, but agree that the article is corny as hell (sorry, author!). Having the text read by multiple people before publishing could have made this a lot better (and still can).
Dependent types on the other hand are great! Looking forward, good luck!
It only feels like "explainabrag"ing to some, I would imagine. The terms are all really standard, and listing out features by their names hardly feels braggy. It's a clear, concise way of stating features of a language. Coming from other languages with those features I think the information was conveyed well - but for others it would just look like jargon.
To me, the author was setting up the post - framing the conversation by explaining their view of Haskell as a set of core features. Then they moved on to discuss another feature - dependent types. This makes a lot of sense in the context of dependent types - I think this HN post really nicely conveys why:
> What a profoundly dismissive attitude. Why bring up Cyclone and not, say, Swift? Or is Swift meant to be included in "garbage collected languages?"
It's like, pretty mostly true. There are other languages that are memory safe without GC but I don't know of any that are mainstream/ even in use, or that allow free'ing of memory.
> No these are not the same and this is an absurdly wrong conflation. Dart, Objective-C, TypeScript, and others are dynamically typed languages with static type checking. You can't "or rather" this distinction away.
I don't think so.
"Dynamically typed with static type checking" makes no sense. The languages listed are statically typed. They may coincidentally compile to code that checks the type at runtime as well, or code that has or lacks implicit casts, or otherwise carries type information around with the data, or whatever, but the types are statically defined.
Also, dynamic types are often considered to be unityped - every value inhabits one giant union of all possible types.
Here is a source demonstrating that this view is not unique. You are free to disagree (some do), but it's hardly an "absurdly wrong conflation".
I think your post was pretty unnecessarily critical. You didn't like the post, ok. But maybe you should have challenged that gut reaction - that "rubbed me the wrong way" feeling, because I think your post has considerably more inaccuracies than the article and is unequivocally more hostile. If you'd challenged that feeling maybe you would have learned something?
I dunno. It can just be that the intended audience is expected to know these terms already. It'd be weird to call any Nature paper an explainbrag simply because it uses field-specific terminology.
Personally, when little things like that piss me off, I find it more helpful to introspect "why do I have such a strong emational reaction to this little thing?" than to go about laying moral judgement. I find this approach is especially good at promoting effective communication in places where it's easy to misinterpret intenions, like text.
At first I thought it was a joke along the lines of "A monad is just a monoid in the category of endofunctors, what's the problem?", but no, it seems to be being said non-ironically.
- polymorphic lambda calculus: Lambda calculus with generics
- lazy evaluation: Well, lazy evaluation. Not sure how else to describe this
- algebraic data types: Again, how else to describe this? Put in a full description of what algebraic data types are?
- type classes: Haskell has type classes.
I really don't see what the problem is. If you're coming in to an article about dependent types, and you don't know what these things are, I think don't think the reasonable response is for the author to explain all of it to the reader. This isn't a beginner's introduction to Haskell.
It's not. Maybe it seems that way because you're not familiar with the terms, so it seems like someone trying to name drop all the stuff they know? But if you are familiar with the terms, it's just informative, and serves to situate you in the space of possible language designs. It's a lambda calculus as opposed to a process calculus, polymorphic as opposed to simply typed, lazy as opposed to strict etc.
I'd argue that the informative value is pretty much zero: If a programmer is familiar with lambda calculus, lazy languages, and algebraic types, then there's just no way that person isn't also somewhat familiar with haskell. The explanation is gibberish for those who need it, so its only use is to be self congratulatory for those who don't.
This point of view is alien to me. Why, when you see words you don’t understand, don’t you make an effort to learn what they mean? How on earth did you ever become a coder with this kind of attitude?
I do understand them, I'm into functional programming and I've toyed with haskell in the past. I'm just aware that such a definition makes it sound more daunting than it really is, mostly because of that "just".
It's kinda like the running joke of "a monad is a monoid in the category of endofunctors, what's so hard about it?", but said in a non-sarcastical manner.
I would assume that some haskell knowledge is assumed, and the author is simply framing the conversation by stating their view of haskell as a set of core features, which they named.
Why do you say "self congratulatory" and not "communicative"? You are assuming your conclusion: that it was snobby. But it wasn't. It was just informative, provided, yes, you knew what the words meant.
The author is communicating with other people who know about the space of programming languages, and describing Haskell in a particular way to show its surface area.
What that quote means is that you can take a Haskell program and compile it into lambda calculus and this is what GHC is more or less doing.
This has important implications. From a theoretical perspective, it's easier to prove that the language remains sound when you add new features. But also from a more practical point of view, it's easier to work on compiler backends for a more minimal language, to target new CPUs or for applying optimizations.
These issues are very well known to language designers. E.g. one of the big changes in Scala 3 / Dotty is that it's supposedly based on "DOT Calculus". Having the ability to "desugar" the language into a simpler language that is provably type safe is pretty awesome.
What makes Haskell interesting is that the developers using Haskell also become acquainted with such issues. Haskell is a language and ecosystem that raises the knowledge ceiling for its users. And there aren't many languages around that do that ;-)
The choir already understands all that. You lost everyone else at the words "lambda calculus".
Go into a random PHP shop, and I would be surprised if a single person would know what lambda calculus is.
I'm not complaining about the message, I'm complaining about the language you are using. If you want to evangelize for Haskell, you need to use words that someone who failed out of differential calculus will recognize and understand.
I was almost 100% certain it was a joke until I read the paragraph that quote is from.
I want to reassure you that most Haskell evangelists (myself included) that say stuff like that usually mean it as a joke. Most people who seek to evangelize haskell do not lose sight of the fact that it's pretty daunting at first and has a relatively steep learning curve.
That said, Haskell is simple, but it's simple in an unintuitive way (as most other languages obscure the ideas). For example I'd argue that when people when people first hear "enum", what they really want is a sum type (i.e. `data Something = OneThing {...} | TheOther {...}`) and not what you get in most languages which is enums-that-are-just-named-numbers or enums-that-are-just-named-strings.
Most languages are coming around to the way haskell/other ML languages view the world however:
- non-nullable + option types
- function composition (a bunch of languages get stuck in the filter/map phase but never get to the)
- typeclasses + data types over classes + interfaces/abstract classes
- pattern matching
- Monads
- The Free(R) Monad and attempts to make programs more like state machines and encode it at the type level
I'm probably preaching to the choir in this thread but Haskell's type system is like the mercedes of production-ready languages these days -- eventually the features trickle down to other languages. There are more advanced options out there like Idris (which already has good dependent type support) but it's going to take a while for any of them to get the support and ecosystem haskell fought hard for over all these years.
One highlight of Haskell's malleability and flexibility is the work around linear types in Haskell[0] -- they basically give you rust-like semantics (reference tracking for compile-time "automatic" memory management/etc) without having to rewrite haskell from scratch. Turns out you can classify rust's main feature under the super generic problem of "ascrib[ing] more precise types". Turns out with a good enough type system, and lots of patience/determination, you can solve a lot of common software issues at the type level.
As the famous saying goes, the future is here, it's just not evenly distributed.
I think the large amount of effort the Rust community puts into explaining what they're doing with their type system, making it a first-class feature that's included in standard tutorials and having a lot of ergonomic effort put into error messages, is actually essential to making it work for ordinary users. (And even then, just barely; fighting the borrow checker is a thing.)
A language that allows someone to build this as a library is much more scary. What other incomprehensible type hackery could someone do? Haskell can be fun but it's always going to look like a somewhat more practical research language to me.
> I think the large amount of effort the Rust community puts into explaining what they're doing with their type system, making it a first-class feature that's included in standard tutorials and having a lot of ergonomic effort put into error messages, is actually essential to making it work for ordinary users. (And even then, just barely; fighting the borrow checker is a thing.)
100% agree -- they've learned a lot from other languages and have padded their steep learning curve (due to the ownership/borrowing scheme and advanced type system), and it's done wonders for them. I spend a lot of my time these days trying to decide between Haskell and Rust for new projects, there are seemingly a lot of people in both camps that are freely moving between these two languages because of their similarities.
> A language that allows someone to build this as a library is much more scary. What other incomprehensible type hackery could someone do? Haskell can be fun but it's always going to look like a somewhat more practical research language to me.
I think it's a bit more than a library (many of the things in the original post and in linear types require deeper changes), and a ton of these features require extensions to GHC (via language extension pragmas in the source file), but I do agree, the type trickery involved is intense.
In my opinion type-level hackery in haskell is not the same as when you do crazy class hierarchies/patterns in other languages (let's say Java) -- for a few reasons:
- Haskell is pretty darn legible, for example, servant[0] is a library that lets you express an API as a type. It does a lot at the type level with advanced techniques, but here's an example of an API:
Despite the fancy type level trickery that servant is doing under the covers this is impressively readable. In many instances the advanced type stuff (like `Partial t`, `WithUUID t`, `Capture "uuid" UUID`) actually helps the code be easier to understand, but doesn't detract from readability.
- You can step up the levels of expressiveness on your own terms -- the simpler way to write things is always right next to the more complicated way, and you can choose to push more into the type level when you choose. Example:
data Task = Task { tName :: TaskName
, tDesc :: TaskDesc
, tState :: TaskStateValue
} deriving (Eq, Show, Read, Generic)
-- the "f" below can be swapped for a polymoprhic type like "Maybe" or "Identity" (which is equal to itself)
-- You can think about this by literally replacing the f with the word "Maybe" everywhere you see it in the below definition, it even makes sense in the semantic english sense.
data TaskF f = TaskF { tfName :: f TaskName
, tfDesc :: f TaskDesc
, tfState :: f TaskStateValue
}
data TaskFInState (state :: TaskState) f where
FinishedT :: f TaskName -> f TaskDesc -> TaskFInState 'Finished f
InProgressT :: f TaskName -> f TaskDesc -> TaskFInState 'InProgress f
NotStartedT :: f TaskName -> f TaskDesc -> TaskFInState 'NotStarted f
-- | The case where we don't know what the state actually is
-- Ex. when we pull a value from the DB, we can't be polymorphic over state with the other constructors
-- but the database *has* to know what was stored forthe state.
-- Once we have an UnknownStateT we can write functions that try to translate to what we expect/require and fail otherwise.
UnknownStateT :: f TaskName -> f TaskDesc -> f TaskStateValue -> TaskFInState state f
-- | Similar case, but for when we need to fix the state type variable to *something*
SomeStateT :: f TaskName -> f TaskDesc -> f TaskStateValue -> TaskFInState 'Some f
This code isn't the greatest but it's what I've been working with in a recent blog series with an in-depth guide to writing a simple rest-ish API. You can go from `Task` to `TaskF` to `TaskFInState` as you graduate, and even let these types go between each other and use the level that is required.
Want to write a function that only works on fully-specified Tasks that are in a very specific state? specialize the types! fore example: `cancelTask :: TaskFInState 'InProgress Identity -> TaskFInState 'NotStarted Identity`. Just reading this signature tells you important information about the function.
More on-topic, the "hello world" program for a dependently typed language is usually length-typed vectors (i.e. `Vector Int 5` to represent a list of ints with 5 elements) -- from my experience people start trying to get more sophisticated with types when they see cool advanced type trickery that they think would be useful, and start doing the reading/trudging uphill to figure it out. This probably is a bit difficult for new developers thrust into a codebase with tricks they don't understand, but again the legibility of haskell code and the clarity provided by type signatures and the syntax helps.
Finding Haskell difficult is nothing to be ashamed of. However it's going to appear more difficult than it ought to be if you're approaching it as an experienced programmer with strong opinions. It can be humbling to realize that there's a whole branch of programming you're completely new to and know little about. It's going to be difficult to climb that mountain and you will feel like a beginner again and that's okay.
> Finding Haskell difficult is nothing to be ashamed of
Agreed.
> It can be humbling to realize that there's a whole branch of programming you're completely new to and know little about.
Agreed.
> It's worth the effort!
To learn it? Sure. To use it? I disagree. I was more unproductive with Haskell than I've ever been with C, which is usually the language I love to bash on. I can look up opcodes and write assembly faster. "Ah, but with experience!" - I don't see why I'd bother.
I write mostly functional code in any language I'm working in as it is. The functional parts of Haskell don't really have anything for me, at least not to compensate the pain of not getting anything done.
Take lens, for instance. It's an incredibly complicated solution to a problem that AFAIK only plagues Haskell! I'd love to know of any exceptions.
Writing networking code was an exercise in frustration where I had to try multiple libraries and faff about with changing types from eager to lazy bytestrings..
I'm glad I bothered to try and learn Haskell. I just don't see me ever using it in production, let alone try to hire anyone who knows it. It's hard enough finding Python programmers who know what generator expressions are.
If we're only talking experiences here then I can say that I've written plenty of networking code in C. I grew up on C. I have 15+ years' experiencein C-like languages across the gamut; more if you count the years when I was a youth and hacking together games and homework assignments for fun.
I've definitely felt the pain you're describing and have even thought of lens in the way you ascribe. How can anyone be productive in a language where logging is so difficult to add? I can add logging to a Python application in 3 lines. And as you say... converting from lazy to strict from text to bytestring to string depending on the library. So annoying! Nothing like those clean examples they show you in the tutorials!
Every time I went down that rabbit hole was because I was getting frustrated with feeling like a beginner again. What was I getting from Haskell for all of this hassle? Why were these simple things in other languages so hard? What's the benefit?
Peace of mind.
It's easier to get started with a C or Python or Javascript program. Partly because of experience. Partly because those languages do nothing to isolate side effects, constrain mutation, or check my code in any effective way. I stick to a particular style (usually functional), I write tests first, and I usually end up paying for that easy start later on in the project when, despite our intentions and efforts; side effects, mutation, and plain old type errors creep in. What I gain in efficiency early on in the project I pay for later with interest. The interest rate is only compounded when we start adding team members.
My experience with Haskell has been that it is frustrating and sometimes slower to get started with, especially when I was first starting out, but that it has been worth the effort in the long run. Down the road when my project started to grow I was better equipped to manage the complexity because I had a type system that kept me honest and guided me towards strong designs. I had a tool that would ensure that only the parts I was really sure about could perform IO actions or use shared mutable state. And best of all I could not touch a module for months and when I came back to it there's a good chance I could understand what it was doing, make the change I needed to make, refactor it, and push it to production without any worries.
I think the human side of software development was the nicest feature of working with Haskell. As I added new team members I didn't have to worry about junior developers breaking the build as much. Training was much more straight forward. The documentation was much easier to write as we could focus on the higher-level designs and let the type system document the details. Testing was more effective as we could focus on problems and tests that brought more value to the business problems.
I still choose other languages for various reasons but Haskell has been worth it in my experience. Painful but worth it.
> Brainfuck is simple, but nobody would choose to write a real project in it.
Sure. But it's worth knowing whether a language is simple or not (and what tradeoffs have been made to get there).
> Most programmers struggle trying to understand what a monad is. That's not easy.
It's easier than achieving Haskell-like defect rates in languages that have ad-hoc built in solutions to the same problems, IME.
> The free monad is not easy.
Disagree. Certainly it's a lot easier than solving the same problem by hand.
> Monad transformers are not easy.
Agreed, but again, easier than achieving the same defect rates without them.
> Understanding foldable/traversable/arrows/applicate is not east.
Easier than understanding dozens of ad-hoc informally specified implementations of half of them, which is what working in an ecosystem without them boils down to.
> Lens is/are not easy.
Perhaps not, but easier than achieving the same defect rate without them.
> It's easier than achieving Haskell-like defect rates in languages that have ad-hoc built in solutions to the same problems, IME.
My first Haskell program type-checked and passed all tests. It was incredibly broken. As in it didn't work at all. I understood monads and it didn't help one jot.
Monads in other languages _can_ be helpful. It pays off to know what one is. But in Haskell, more often than not they're being used to solve problems other languages don't even have in the first place.
> Disagree. Certainly it's a lot easier than solving the same problem by hand.
How? Anyone knows how to write a test double by hand. Most people can use a mocking framework. The visitor pattern is in the GoF book. These are well known and don't involve completely changing the type signature of the code you're writing just so you can interpret it. And let's not even mention Lisp.
> Agreed, but again, easier than achieving the same defect rates without them.
Not really. Write pure code, test it, have a thin layer of side-effects around it. The transformer stack is solving, again, problems only Haskell has. I don't need the state monad anywhere else, so I don't need to layer it on top of anything. In a language with exceptions, ditto. And so on.
> Easier than understanding dozens of ad-hoc informally specified implementations of half of them, which is what working in an ecosystem without them boils down to.
I would bet good money that in my old team I wouldn't be able to explain what an applicative functor is to 90% of them if I had one month of full time training.
> Perhaps not, but easier than achieving the same defect rate without them.
> Monads in other languages _can_ be helpful. It pays off to know what one is. But in Haskell, more often than not they're being used to solve problems other languages don't even have in the first place.
Every language faces the same problems; your only options are to not solve the problem at all, solve it in an ad-hoc way, or solve it with a general feature.
E.g. every language faces the problem that error handling can be quite boilerplatey. Bad languages don't solve this at all. Somewhat better languages offer an ad-hoc language feature like exceptions, which are superficially nice (indeed superficially nicer than monadic error handling). But every ad-hoc language feature is one more thing to keep in mind when working or debugging, so they all come at a penalty to your defect rate: exceptions lead to "magic" control flow which can lead to resources not getting closed on error paths, seemingly-innocuous refactors changing behavior, and so on.
> Anyone knows how to write a test double by hand. Most people can use a mocking framework.
Until you ask them to test code that relies on something async, and then they'll write flaky tests, or no tests at all. And I don't think I've ever seen a decent test double for something like a database (most people give up and use an in-memory one). Even those who write tests tend to end up with tests that are much more boilerplatey than main code and not kept up to date, because mocking frameworks rely on magic reflection that means you can't refactor code that uses them the normal way.
> Write pure code, test it, have a thin layer of side-effects around it.
And when the business logic you're implementing is inherently coupled to effectful questions and effect actions, what then? Distort your code, invent some ad-hoc datastructure to represent a half-complete business decision that needs to rely on the answer from some other service?
> I don't need the state monad anywhere else, so I don't need to layer it on top of anything. In a language with exceptions, ditto. And so on.
Well, you need state, you need error-handling; either you do these things manually and directly (painfully verbose and unmaintainable, leading to high defect rates), you do them in a "magical" unmanaged way (high defect rates because you can no longer know what code interferes with what other code), or you manage them explicitly, at which point you need a way to interleave managed effects.
> I would bet good money that in my old team I wouldn't be able to explain what an applicative functor is to 90% of them if I had one month of full time training.
Bet you could. I simply don't believe that anyone who can understand the "visitor pattern" or "observables" or "factories" or whatever the OO pattern of the week is could struggle with applicative functors. It's an interface consisting of two functions of at most two arguments. It's really not that hard.
> Solves, yet again, a problem only Haskell has.
Not so; every substantial system I've seen has ended up needing some way to pass a "patch" or "change" around between different bits of code. The only choice is whether you do it in an ad-hoc way or a standard one.
And that would prove what, exactly? That no language is perfect we already know. My assertion is that, for the vast majority of programmers, Haskell is fundamentally harder than the languages they already know or could learn instead.
Comparing Haskell to brainfuck is a little hyperbolic -- you do not have fully understand Monads and their underpinnings to be productive in Haskell. Just like when new programmers write "public static void main" and have no idea what it does, or how JAR files work, or how cout works, newbies can type `do` and get off and running. In Haskell most of your time is spent writing non-monadic code -- writing pure functions that don't care about the outside world.
Another important distinction I want to draw is that while you're that Haskell isn't easy, the difficulty contained within is fundamental to computation itself.
Haskell uses it's type system to buddy-up with category theory which is considered a dual to typed lambda calculus[0]. There are spooky (to me at least, less so to actual mathematicians) natural equivalencies here in that there are certain things you can talk about at the level of Haskell types (category theory) that are universal, and since we're talking about computation, they start becoming universal truths about computations. This is a powerful concept because it changes the way you think about problems. Regardless of whether it's useful in your day job (which might be plumbing two RESTful APIs together) -- I'm not trying to convince anyone to use haskell for everything (you should use the right tool for the job given the constraints), I'm trying to encourage people to try it at least once to see the difference.
Haskell in my mind offers a step stool to understand the deeper theory/mathematics underpinning of computation as a whole, by providing a language that can essentially do both -- express complex concepts and actually do useful things -- it's somewhere on the opposite end of the spectrum from assembly, but not as far as a pen and paper/chalkboard/your mind.
To follow on the point above, all the concepts you're discussing as hard are what we're building in other languages -- the other languages are just giving us versions of the power/expressiveness with corners cut for ergonomics sake, or in the worst cases, drastically reduced power. There is a tradeoff, and it obviously does not always make sense to use Haskell's version of some abstraction, if you do not understand it or it takes you 5x as long to code up. That said, knowing the underlying concepts that underpin these things is the kind of knowledge you can take from project to project -- concepts like traversable show up in file/folder walking, graph traversal, all these problems that you might think were not generically solvable if you only ever dealt with libraries that worked at the lower level (as in one library for walking graphs and the other for walking the filesystem).
You're right that understanding the concepts isn't easy, but this is the best kind of understanding to struggle and overcome -- it's fundamental to the field itself. No one is going to come up with a new Monad/Foldable/Traversable tomorrow, they can generally at best discover new concepts.
> I have personally worked with dozens of programmers that would never be able to write "proper" Haskell.
As long as these programmers learn the paradigms I don't care, use another language that's easier to write. The problem is that you can happily write language x for years and never scratch the surface of these deeper truths/paradigms/approaches, but that doesn't mean it's a good idea for your own personal development as a developer/computer scientist/whatever else. If you don't see value in exploring different, likely fundamental ways of thinking about computing then you do you.
Maybe it's just me, but I see value in languages that expand the way I think -- just like that aha moment when I figured out how to use map/filter/reduce instead of writing for loops. I learned to think in transformations, one step abstracted from the imperative reality.
Haskell may not be for everyone, but the paradigms it exposes are for all computer scientists (as far as I can tell anyway), and thus software developers/engineers who want to work smarter and not harder.
> you do not have fully understand Monads and their underpinnings to be productive in Haskell
I don't think that's true. Most programming is done in a team, and someone will have written a transformer stack. I was told to use the free monad to solve my testing problem in my first Haskell program. "Hello world" doesn't count.
> the difficulty contained within is fundamental to computation itself.
Not always. The examples I gave are all of what I consider to be "unforced errors". I don't need monad transformers in any other language I've written code in. Or lens. Or arrows. Or free monads. Or...
> I'm trying to encourage people to try it at least once to see the difference.
I did. Hence me even knowing what lens is.
> concepts like traversable show up in file/folder walking, graph traversal, all these problems that you might think were not generically solvable if you only ever dealt with libraries that worked at the lower level (as in one library for walking graphs and the other for walking the filesystem).
Honest question: how is knowing Haskell's traversables (which are hard) going to add to one's knowledge if one has already worked with any of the following:
* C++ iterators
* Python iterables
* D ranges
* C++20 ranges
* (I think) Clojure's transducers?
Sure, Python and Clojure are less applicable due to being dynamic, but D and C++? Generic. Same goes for foldable.
> As long as these programmers learn the paradigms
They wouldn't be able to. I say this as someone who somehow managed to take a student who didn't know how to add fractions together and tutor him to the point of (just) passing a university Linear Algebra class.
> Maybe it's just me, but I see value in languages that expand the way I think
So do I. Trying to learn Haskell was enlightening. I can't see me picking it as the tool of choice for pretty much any project though.
> software developers/engineers who want to work smarter and not harder.
When I wrote Haskell I found myself working harder, writing bugs anyway and wondering what the point was. It's intellectually interesting, and worth looking into. I just don't want to write in it.
> I don't think that's true. Most programming is done in a team, and someone will have written a transformer stack. I was told to use the free monad to solve my testing problem in my first Haskell program. "Hello world" doesn't count.
Right but there isn't any other language where a production application will be obvious to newcomers anyway. There is always some cruft/enterprise design pattern/whatever else that will need to be learned or at least hand-waved for early productivity, and will be deeply understood later. My point was that you don't have to understand what "do" does. If you get some simple feature let's say update the user wiggle count when any friend wiggles), the chance you're going to be editing legible, clear haskell (given you understand how to read haskell) is high. Something like:
-- | do a user wiggle and return the wiggle count
doWiggle :: User -> IO WiggleCount
doWiggle user = do
_ <- saveWiggleToDB user
wiggle <- updateWiggleCount user
-- here's where the newbie would probably start thinking to add some code
return wiggle
While this code is just a fake example, it's concise, and very legible -- you don't need to understand the complexities of the IO monad or any other stack that would be there, haskell can mimic the simplicity of a completely imperative monad-less environment, down to the `return`.
> Not always. The examples I gave are all of what I consider to be "unforced errors". I don't need monad transformers in any other language I've written code in. Or lens. Or arrows. Or free monads. Or...
But see this is the the whole point of the discussion of the relationship between lambda calculus and category theory. You're using most of these concepts already, you're just calling them something different, and wrapping them in some unnecessary ceremony/enterprise design pattern. Or even worse, you're using weaker, partial, worse approximations of these concepts and don't know it. Ignorance is not bliss in our line of work -- whether or not you use the concepts I (at least) expect good programmers to know the underpinnings.
> I did. Hence me even knowing what lens is.
I can't argue with your personal experience -- if you don't think learning that stuff was beneficial then there's nothing I could say to change your mind. My argument hinges on the fact that those concepts are beneficial and haskell shows them to you without much adulteration faster than other languages.
> Honest question: how is knowing Haskell's traversables (which are hard) going to add to one's knowledge if one has already worked with any of the following:
It adds to one's knowledge the same way knowing the Iterator/Iterable pattern exists instead of having used for loops in any of those patterns. It adds to one's knowledge the same way reading the gang of four book does, or any theoretical computer science does. Traversable is roughly identical to the iterator patterns but it is the purified form of the concept -- you don't get bogged down with how python iterates or some other language and how they built their iterator implementation.
> They wouldn't be able to. I say this as someone who somehow managed to take a student who didn't know how to add fractions together and tutor him to the point of (just) passing a university Linear Algebra class.
I don't consider myself an optimist, but I think you're wrong. If you were right, growth would be impossible for humankind. A more useful statement IMO might be that the amount of effort and focus one would have to put in is beyond what they could exert in the amount of time they have to devote (or their lifetime) -- but even then that's a hard statement to prove.
> So do I. Trying to learn Haskell was enlightening. I can't see me picking it as the tool of choice for pretty much any project though.
I mean that's OK though -- hopefully you picked up some things that were useful to you. Haskell ergonomics or practicality (basically, language features) is something that the Haskell community has to work on and make better.
> When I wrote Haskell I found myself working harder, writing bugs anyway and wondering what the point was. It's intellectually interesting, and worth looking into. I just don't want to write in it.
Again, I can't argue with your personal experience, but I can tell you that if you're using haskell's type system at all correctly what you're saying just can't be true. It's just not how it works -- for example, you probably have never gotten an NPE in Haskell -- it's a class of errors that doesn't exist for the most part. The errors you were getting (or maybe compiler feedback?) isn't the same as in other languages.
> For example I'd argue that when people when people first hear "enum", what they really want is a sum type
I'll be honest, I'm pretty sure the first time I header "enum" I had exactly 0 idea of what it would be, so it can be whatever the language designer wants, it will always work out for someone.
Well, both System Fc and Haskell Core are quite simple and consistent. It's much more concise than any imperative language with dozens of corner cases, yet quite powerful.
> Really, I feel like everyone who is going to read that article will either already know that, or will have no idea what that sentence means.
Yeah, that seems to explain the reaction to it here. But I'm not sure writing things you expect your audience to understand is such a bad thing. This is probably just the wrong audience for the post.
Every discussion or article I have read on dependent types assumes that the reader is a mathematician. I usually make it only a few paragraphs in before I am completely lost.
Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not theoretical) benefits but they do not come through clearly. All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity. There must be more, that I'm just not seeing.
Is there a "Dependent types for non-mathematicians" article out there somewhere, where I can learn about patterns and practical applications?
> Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly.
I'd say that's backwards: rather a dependently typed language relaxes a huge restriction that most programming languages have, that only certain things can be used as types. Any program that's valid in language X is also valid in a dependently typed version of language X (e.g. most Haskell functions translate directly into Idris as long as they don't rely on laziness).
Dependent types make it easier to encode properties that you care about into the type system, i.e. rather than the programmer having to get them right, the compiler can check them for you. Far from burdening the programmer, it lightens your mental load.
> All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity.
Most code is in terms of domain-specific things, and so the types you use are also domain-specific. In my experience every code bug (as distinct from "behaving as specified but not as intended" bugs) boils down to "we thought x, but actually y" and can be avoided by making more precise use of a type system. If you have bugs that hit production, you can probably avoid them with better types. If you avoid production bugs by using tests, you can probably replace most of those tests with types and they'll become more concise and easier to maintain. But of course the specifics of what types to use will be specific to your domain; examples like list indices are common because they're one of those rare types that virtually everyone uses.
Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly
It's basically the opposite of this.
If a language has dependent types, you can continue to use it in the same way as a language with does not have dependent types.
BUT, there's a lot of programming patterns that previously couldn't be implemented in a type-safe way, that now can be. This also gives a ton of opportunities for libraries to implement abstractions that weren't expressible before.
Dependent types are not that complicated, actually, and they don't add any burden to programs that don't use them.
Actual article title: "Why Dependent Haskell is the Future of Software Development" - which the author spends a few handwavey paragraphs unconvincingly trying to show. After that, though, the article moves on to why to get there, and how to do so, both of which are more interesting than the attempt to justify the claim in the title.
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1.
Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive.
When I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.
The key difference with C++ templates is that in C++ you can't have a type parameterised by a value that's only know at runtime, e.g. a std::array<N> where N is read from stdin. In a dependently typed language, you can. Object orientation is a different matter entirely; in the sense it implies Java-style class-based inheritance, it's almost in the opposite spirit to dependent types, as such late-binding (virtual methods) means it's possible to call methods such that the compiler has no idea which method will be called at compile time, making it hard to reason about the code at compile time.
Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side.
Now allow arbitrary programs to be types. We'll call these type programs.
Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing.
For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself.
Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis.
In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true.
You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here.
I find the whole thing fascinating myself, but haven't gone too deeply into it.
(BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)
In a very abstract way, it is a way to encode relationships between types on the type system.
You can express things like how are you allowed to consume elements from a data structure, how many elements a specific data structure is allowed/expected to have, how their form looks like and so forth, all at compile time.
Thus working as kind of profs that certain functions can only be called if the conditions are met.
Most typed programming languages will allow you to form a pair of type (Integer, Integer), and reject programs which try to return something like (Integer, Float).
Dependently typed languages might allow you to declare a type (n, m) where n and m are integers, and n < m, and will reject programs which attempt to return pairs with n > m.
The key step here is that this rejection is done during compilation, and so while your program is running you can be absolutely sure that n < m.
Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class.
As an example this is Haskell's core language:
data Expr b
= Var Id
| Lit Literal
| App (Expr b) (Arg b)
| Lam b (Expr b)
| Let (Bind b) (Expr b)
| Case (Expr b) b Type [Alt b]
| Tick (Tickish Id) (Expr b)
| Type Type
| Cast (Expr b) Coercion
| Coercion Coercion
data Type
= TyVarTy Var
| LitTy TyLit
| AppTy Type Type
| ForAllTy !TyCoVarBinder Type
| FunTy Type Type
| TyConApp TyCon [KindOrType]
| CastTy Type KindCoercion
| CoercionTy Coercion
If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax.
And this is Lean core language (a dependently type language):
inductive expr
| var : nat → expr
| sort : level → expr
| const : name → list level → expr
| mvar : name → name → expr → expr
| local_const : name → name → binder_info → expr → expr
| app : expr → expr → expr
| lam : name → binder_info → expr → expr → expr
| pi : name → binder_info → expr → expr → expr
| elet : name → expr → expr → expr → expr
| macro : macro_def → list expr → expr
Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types.
So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time.
In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages.
That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.
When the type of a function mentions its parameter, it’s a dependent type (just like a normal function that mentions it’s parameter is a “dependent value”, so to speak.
Usually though one speaks of dependent types only when the parameter can range over not just types.
[1] https://ucsd-progsys.github.io/liquidhaskell-blog/
[2] https://rise4fun.com/Dafny/tutorial/guide
[3] https://fstar-lang.org/tutorial - see e.g. section 3 "First proofs about functions on integers"
[4] https://github.com/Z3Prover/z3