I had never heard of this book before, now I definitely want to give it a try.

As an aside, isn't type driven development how everyone codes naturally in statically typed languages? Whether it's Ocaml or Java, I feel like I try to get the types defined, then put on music and turn my brain off and just line the types up (much moreso in Ocaml than in Java).

Indeed, and this is precisely why I hate writing in dynamically typed languages like Ruby or Python; they hinder me from thinking about the shape of the program clearly.

Well now you can write full types in both of them

You can write them, but without most of the benefits of static types

You can typecheck them with mypy or pyright or at runtime with typeguard.

It is not ideal, but pretty good in terms of benefits.

That’s great, but sometimes those tools fail to spot an error silently, where a compiler plus runtime checks usually won’t.

As an extensive user and a fan of these Python type checking tools, I do not remember this happening for some years now. Do you have a particular example where it should be improved?

Yea, at work mypy fails quite often on the old code there.

Never once happened to me in years of typescript, though I agree it’s obviously possible

Such a major failure was my first (and last) experience with TS about two years ago. Had all the "strict" options set, was quite happy finally using a "type safe JS", and boom, it exploded at runtime with some nasty bug which was discovered not before having the code run in production. Than I learned that TS' "type system" isn't sound, and you're required to write tests even for the parts that should be actually covered by the "types". That's not helpful at all. That's not what I expect from type safety.

Was this blow up due to a dependency with an 'any' type somewhere, and your code the dependency library some garbage? That's what bit me, even with the strictest ts settings, this can't be picked up by tsc.

I don't know anymore what it was concretely. That was two years ago on some project that wasn't even part of my usual duties. We lost some team members and I had to look after some extra projects. As I have quite some experience with JS I was given a TS task.

At this point I was even quite eager to update my JS skills with TS knowledge. All in all it was fun to write this project. But my error was to trust the types like I would when programming on my main project in Scala. Big error…

Since than I think TS is much oversold.

You can do fun things with the types (even some things that I miss in Scala, and there is not much to miss in Scala in general!), but you just can't trust the TS types. So this makes them superfluous in some sense. (Yes, some types are better than no types; especially when it comes to the IDE experience; but as long as any lib call (due to trivial bugs in "typing-files"), or some "impossible" input can break things this is not as helpful as one would like; especially when coming form really strongly typed languages).

Same. As long as you sanitize dynamic serialized input like json while parsing this is not a problem.

Later versions are very strict even about dynamic types, treating them as Union[] rather than Any, forcing you to check the type before using it. Likewise with strict non nullable.

I still use python type hints (and TypeScript) - and while they have benefits, I find that they fall short of something like Rust, Haskell, etc (because they are just that - hints). I don't have the surety that the types as annotated are the same as the types at runtime.

Just to make it clear. If you use typeguard @typechecked annotations snd the type hint does not match reality at runtime it will blow up with an error telling you.

The same, but at "lint time" (not runtime) will happen with mypy or pyright, although I am sure there are rough edges.

Checking types at runtime is dynamic typing. It's equal to writing something like `if (typeOf(someValue) == "someRuntimeType") {…}`.

This misses all the advantages of static types.

Typeguard checks at runtime. Mypy and pyright check at "lint time". They do static analysis of the code without running it.

this is putting the cart before the horse given that in any real-world facing application it's not the language that determines the shape of the program but the data and rest of the world that interfaces with your program.

Dynamic languages are in many ways simply a recognition of that fact, namely that data is sparse, incremental, changes and accretes and so on. There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.

> There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.

Scala developers would disagree.

Especially in business applications strong static types are extremely helpful to prevent bugs and model the domains of interest in a proper way.

I agree; I would expect to see such languages feature much more prominently there, especially in the subtle and convoluted business/legal complex.

One may argue that the proof-strength formality can be a hindrance: in such domains, inconsistencies and contradictions abound, and some of them cannot be predicted in advance. But I believe that languages like Idris can accommodate this. Maybe I am wrong, or maybe they can, but not more efficiently than more free-form languages.

...but ok, I am failing to see what I can do with COBOL that I cannot do with Idris, business-logic-wise. lol

It's a bit more than that in Haskell (and I guess Idris, but never tried). In Haskell you can write 'undefined' in any definition. 'undefined' is of any type, so the code will type-check. Then you can write a high-level sketch of your program, including functions, purely based on types and 'undefined'. When you are satisfied playing the types puzzle, you proceed to write implementations. This is referred to as "hole-driven programming" or "type hole-driven programming".

Also, like the other guy mentioned, the types lend themselves very well to auto-completion. It's no coincidence than in Hoogle, you can often find a function by its type. E.g., what could "[a] -> [b] -> [(a,b)]" possibly do?

https://hoogle.haskell.org/

In my experience it's not at all how everyone codes, or even almost anyone, in statically typed languages. Here's an example to elucidate a (potential) difference between the common and the commitment to types:

You're coding a card game, say poker. Games should only start with a shuffled deck.

1. A reasonable, common solution would be to have a type like Deck, and a function shuffle, taking a Deck and returning a Deck (where taking can mean it's an instance's member function, and returning can mean inplace mutation)

2. A type driven approach can be having two distinct types: Deck and ShuffledDeck, and a function that takes a Deck and returns a ShuffledDeck, and all procedures henceforth in the game's logic require ShuffledDeck - _not_ Deck.

In the type driven approach the possibility of playing with an unshuffled deck has been removed solely through the usage of types, and successful compilation is a proof no cheaters can sneak in a bad deck.

But it's not just that. There's exactly one function that takes Deck and returns ShuffledDeck, so a language like idris knows this has to fill a hole somewhere, in the one place that starts with Deck and then need ShuffledDeck. So in some sense part of the code has been written automatically.

I rarely see the second approach used, though I see analogies of this example all the time.

good example. i thought i used type-driven design, but your example made me realize i'm clearly not.

In your example, how would you qualify using an enum "State" with the case "shuffled" and "ordered" ? I feel like this would help me check all cases in places where it's needed, sometimes with the help of the compiler. But does that qualify as "type-driven" ?

In particular, do languages like idriss require encoding all possible states of a state machine as a unique type to leverage the full power of the checking mechanisms ? This would seem a bit unmanageable in practice..

I'm not an expert, I don't know how the community would treat such enums. I think the bottom line is if you can't fail to shuffle the cards, whether through an interesting enums and matching mechanism or through some other part of the type system, then you're good.

I've never used idris, but as far as I understand it encoding state machines in the type system is exactly the kind of thing type-dependent languages in general and idris in particular shine at. This is the prototypical example given, and it's the one Mathew Farwell himself gives in a podcast interview [1]

[1] software engineering radio, episode 296, http://feedproxy.google.com/~r/se-radio/~5/Kg1Py4rd2i0/SE-Ra...

There is at least one language that does this as a form of its core mechanism of execution- Mercury Language, a declarative/logic programming language.

Its type system is fairly complex. To accomplish the goal you describe, functions must be declared as deterministic, non-deterministic, or multi-deterministic. Meaning, they always have a solution, sometimes have a solution, or multiple solutions for the same input.

Armed with that information, the compiler will throw an error if you haven't thought of all possibilities in your logic flow. The fact that the type system required you to be very descriptive in many different ways compounded the number of bugs that the compiler would catch before your program ever runs... I think someone said "if you can get your code past the compiler, it will work on the first try."

I wish Mercury were more popular, it's an awesome project!

Another example, let's say you're parsing a subscriber name for an email list, and you have a few checks such as whether it's too long, has whitespace, orcontains forbidden characters:

    pub fn parse(s: String) -> SubscriberName {
        let is_empty_or_whitespace = s.trim().is_empty();

        let is_too_long = s.graphemes(true).count() > 256;

        let forbidden_characters = ['/', '(', ')', '"', '<', '>', '\\', '{', '}'];

        let contains_forbidden_characters = s
            .chars()
            .any(|g| forbidden_characters.contains(&g));

        if is_empty_or_whitespace || is_too_long || contains_forbidden_characters {
            panic!("{} is not a valid subscriber name.", s)
        } else {
            Self(s)
        }
    }

And let's say your code to add a new subscriber to the email list only accepts a SubscriberName, not a String:

    pub struct NewSubscriber {
        pub email: SubscriberEmail,
        pub name: SubscriberName,
    }

Because `parse` gives back a SubscriberName if and only if all of the parse checks pass, you simply cannot add a new subscriber without all checks passing; the function will simply fail otherwise.

This example comes from the excellent book Zero To Production In Rust, which has a chapter on type-driven development [0].

[0] https://zero2prod.com

"Funny" code.

I'm quite sure nobody would do something like that "in production"…

The problem starts with the signature of this function: There is—of course—no function which could take an arbitrary String and return a SubscriberName.

You need to return at least an Option, or better a Result.

But at this point the fun starts. You need to thread this wrapped value throughout your whole program.

Crashing your program (by a panic in the above function, or by a unwrap somewhere later) because someone sent you an invalid String is not an option in real life.

That's a simplified example that I grabbed in the middle of the book before the author refactors it, of course you shouldn't `panic` if you don't need to.

I've pointed this out as I think the follow-up problem is more difficult actually.

It's easy to validate something "and just throw an exception".

The fun starts when you can't do that (or don't want to do it like that).

Don't forget that "type derived code" also happens with any language that has implicit arguments, e.g. type classes in Haskell and implicits in Scala. For example, in Haskell, if I compare two lists-of-maps-of-tuples for equality, there are many nested equality functions involved, but the type class machinery generates this code, at compile time for me. In a language without this, e.g. OCaml, many generic operations like equality, to_string, serialisation, etc become very painful.

Even "implicits" (especially the explicit ones called `given`s in Scala) are extremely useful I don't think you need them for type-class derivation. Rust does not use "implicits" for that, I think.

How does Rust do it? Is it possible to derive using custom logic?

If I would need to guess I would say it's done through Rust's macros.

But I would need to look this up also myself. I'm not 100% sure. (But I've never heard of any implicits implemented in Rust; they discussed this feature here and there, but it's not part of anything in the language or the compiler, afik).

OT: I've never seen you on the Heise forums ever since. But I guess there isn't much to miss anyway by now…

Hahaha, which name do you go by in Heise forums? I wonder if I remember you too.

I prefer not to link accounts, but we've talked not only once. :-)

I've recognized your handle as I remember you as being one of the few people there who actually know what they're talking about when it comes to software engineering.

But I've also moved on. The overall level has dropped to a bottomless pit by now. It's no fun anymore.

> I prefer not to link accounts, but we've talked not only once. :-)

Fair enough and thank you for the kind words. :)

> the compiler can guess the implementation of the function [...] guaranteed to be correct on a type level

I'm curious about this. Can you provide some examples, please? Which languages can do this?

The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube:

https://www.youtube.com/watch?v=DRq2NgeFcO0

The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.

off the top of my head, coq agda idris.

you can sort of do this with ghci and :hoogle.

the simplest example is

foo : A -> A

since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.

another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.

All of the environments are pretty interactive, and you pick and choose. but from time to time there is exactly one possible implementation that meets all the constraints, so the compiler can fill that in.

Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.)

When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from.

In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.)

Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.)

On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.

in agda, I think ctrl-c ctrl-a is the "I feel lucky" button. Plfa is definitely good, Connor Mcbride is pretty good too https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37ox...

and yes programming with holes is almost magical. I really like "run as much as you can" then complain when you get stuck. kind of a mind blowing change for me.

> In your `bar` case, `bar xs = 42` is also a solution.

Not if you add the condition that the type must be as general as possible.

> foo : A -> A

> since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.

> another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.

Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.

Maybe a better example would be `z: [A] -> [B] -> [(A, B)]`.

While the concept is neat, I struggle a bit to see how it can be useful in practice. Do you have an example for the sufficiently constrained case? That sounds like the most interesting case by far.

You had a look at Hoogle?

https://hoogle.haskell.org/

For some type signatures there is (are) only one (or only a few) meaningful implementation(s).

> the logic itself can be produced automatically via the filling of type holes

Does that work in anything but boilerplate code? Like, hole filling won't be able to decide between then and else clauses in a conditional, for instance, because both clauses return the same type. And conditionals are one of the most basic data flow structures.

For Boolean conditionals, you're right. But there are richer conditionals that make certain variables available in only one clause of them, e.g., matching on whether an Either in Haskell is Left or Right, or whether a Result in Rust is an Err or an Ok.

> Does that work in anything but boilerplate code?

It depends on the problem and the language.

The most impressive I've ever seen was implementing "call with current continuation" as a monad, given nothing but the type signature.

Generally, it works best in strongly-typed, functional languages.

> The most impressive I've ever seen was implementing "call with current continuation" as a monad, given nothing but the type signature.

That sounds cool. Where to find this? I get only irrelevant search results.

To be honest, boilerplate is where I think I'd appreciate code generation the most.

That makes sense, but it also seems like a “the cause of, and solution to, all of life’s problems” sort of situation.

Today I learned that there's a name for the kind of development I do naturally. Modeling my input and output types first is so much more effective at helping me to develop my mental model of the program. I often catch "bugs" before I've started writing code just by thinking about how the data flow will work.

The hopi is out of days though. It covers Idris 1 and isn't, I believe, being updated. Edwin intimated to me a while ago he'd rather have his bollocks cut off than write another book, and I assume he included updates in that. Idris 2 has significant differences to 1.

Would you also recommend that book to someone who's not using Haskell/Idris/Scala?

Sure, it's the methodology that's important, of making invalid states unrepresentable.