28 ms·

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

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...
- chrisworden 4y ago
  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!
- satvikpendem 4y ago
  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 https://zero2prod.com
  - still_grokking 4y ago
    "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.
    - satvikpendem 4y ago
      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.
      - 4y ago

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...
chrisworden 4y ago
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!
satvikpendem 4y ago
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 https://zero2prod.com
- still_grokking 4y ago
  "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.
  - satvikpendem 4y ago
    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.
    - 4y ago