7 ms·

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 stati

by acchow 4y ago

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).

satvikpendem 4y ago
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.
- iddan 4y ago
  Well now you can write full types in both of them
  - shpongled 4y ago
    You can write them, but without most of the benefits of static types
    - mejutoco 4y ago
      You can typecheck them with mypy or pyright or at runtime with typeguard. It is not ideal, but pretty good in terms of benefits.
      - ok_dad 4y ago
        That’s great, but sometimes those tools fail to spot an error silently, where a compiler plus runtime checks usually won’t.
        miohtama 4y ago
        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?
        ok_dad 4y ago
        Yea, at work mypy fails quite often on the old code there.
        v0idzer0 4y ago
        Never once happened to me in years of typescript, though I agree it’s obviously possible
        still_grokking 4y ago
        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.
        Throwaway234590 4y ago
        Was this blow up due to a dependency with an 'any' type somewhere, and your code fed the dependency library some garbage? That's what bit me, even with the strictest ts settings, this can't be picked up by tsc.
        still_grokking 4y ago
        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).
      - shpongled 4y ago
        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.
        mejutoco 4y ago
        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.
      - still_grokking 4y ago
        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.
        mejutoco 4y ago
        Typeguard checks at runtime. Mypy and pyright check at "lint time". They do static analysis of the code without running it.
- Barrin92 4y ago
  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.
  - still_grokking 4y ago
    > 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.
    - ykonstant 4y ago
      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
deleted 4y ago
[deleted]
yazzku 4y ago
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/ https://hoogle.haskell.org/
henrydark 4y ago
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.
- bsaul 4y ago
  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..
  - henrydark 4y ago
    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-Radio-Episode-296-Type-Driven-Development-with-Edwin-Brady.mp3 http://feedproxy.google.com/~r/se-radio/~5/Kg1Py4rd2i0/SE-Ra...

by acchow 4y ago

satvikpendem 4y ago

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.

iddan 4y ago
Well now you can write full types in both of them
- shpongled 4y ago
  You can write them, but without most of the benefits of static types
  - mejutoco 4y ago
    You can typecheck them with mypy or pyright or at runtime with typeguard. It is not ideal, but pretty good in terms of benefits.
    - ok_dad 4y ago
      That’s great, but sometimes those tools fail to spot an error silently, where a compiler plus runtime checks usually won’t.
      - miohtama 4y ago
        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?
        ok_dad 4y ago
        Yea, at work mypy fails quite often on the old code there.
        v0idzer0 4y ago
        Never once happened to me in years of typescript, though I agree it’s obviously possible
        still_grokking 4y ago
        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.
        Throwaway234590 4y ago
        Was this blow up due to a dependency with an 'any' type somewhere, and your code fed the dependency library some garbage? That's what bit me, even with the strictest ts settings, this can't be picked up by tsc.
        still_grokking 4y ago
        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).
    - shpongled 4y ago
      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.
      - mejutoco 4y ago
        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.
    - still_grokking 4y ago
      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.
      - mejutoco 4y ago
        Typeguard checks at runtime. Mypy and pyright check at "lint time". They do static analysis of the code without running it.
Barrin92 4y ago
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.
- still_grokking 4y ago
  > 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.
  - ykonstant 4y ago
    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

deleted 4y ago

[deleted]

yazzku 4y ago

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/ https://hoogle.haskell.org/

henrydark 4y ago

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.

bsaul 4y ago
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..
- henrydark 4y ago
  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-Radio-Episode-296-Type-Driven-Development-with-Edwin-Brady.mp3 http://feedproxy.google.com/~r/se-radio/~5/Kg1Py4rd2i0/SE-Ra...