5 ms·

Compile-Time Checked Truth Tables

72 points by chriskrycho 3y ago

lemper 3y ago
good thing c# supports pattern match too. just this morning, I wrote something like this var thing = (enumA, enumB) switch { (EnumA.A,EnumB.A) => DoStuff(), _ => throw new Exception(), } suffice to say, c# is pretty ok, coming from ml family.
- KineticLensman 3y ago
  Rust's match is pretty cool as well. Here's Fizzbuzz, lifted from [0] match (i % 3 == 0, i % 5 == 0) { (false, false) => { }, (true, true) => { FizzBuzz }, (true, false) => { Fizz }, (false, true) => { Buzz } } I'm moving from C# to Rust at the moment and really enjoying it, especially now that I (almost) understand the borrow checker [0] https://stackoverflow.com/questions/43896431/c-sharp-equivalent-of-rusts-match https://stackoverflow.com/questions/43896431/c-sharp-equival...
  - recursive 3y ago
    Can you match to (i % 3, i % 5) instead?
    - Philpax 3y ago
      You can, yes: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0c8baf63af6af6fed10a62b9d0e9a6dc https://play.rust-lang.org/?version=stable&mode=debug&editio...
  - jsmith45 3y ago
    As you hopefully know, the modern C# equivalent is not bad either, especially with top level statements and implicit global usings (The following is the whole program): foreach (var i in Enumerable.Range(1,100)) { Console.WriteLine( (i%3==0,i%5==0) switch { (true, true) => "FizzBuzz", (true, _) => "Fizz", (_, true) => "Buzz", (_, _) => $"{i}" } ); } This is so much nicer than what was possible back when the linked question was asked.
    - recursive 3y ago
      It gets a bit nicer still. (i%3,i%5) switch { (0, 0) => "FizzBuzz", (0, _) => "Fizz", (_, 0) => "Buzz", (_, _) => i }
- Smaug123 3y ago
  Enums are a bit leaky, though, because C# enums can just have any old `int` chucked into them, so you really do need the final arm of the `match`. `(EnumA)100` will compile just fine!
deleted 3y ago
[deleted]
tczMUFlmoNk 3y ago
Somewhat surprised that the author doesn't go on to show how to reduce the truth table... let decide requiresApproval canUserApprove itemStatus = match requiresApproval, canUserApprove, itemStatus with | true, true, NotAvailable -> Hidden | false, true, NotAvailable -> Hidden | true, false, NotAvailable -> Hidden | false, false, NotAvailable -> Hidden | true, true, Available -> ReadWrite | false, true, Available -> Hidden | true, false, Available -> ReadOnly | false, false, Available -> Hidden | true, true, InUse -> ReadOnly | false, true, InUse -> Hidden | true, false, InUse -> ReadOnly | false, false, InUse -> Hidden ...to something like this: let decide requiresApproval canUserApprove itemStatus = match requiresApproval, canUserApprove, itemStatus with | _, _, NotAvailable -> Hidden | false, _, _ -> Hidden | true, true, Available -> ReadWrite | true, _, _ -> ReadOnly I would think that being able to see and effect this reduction is part of the benefit of writing out the whole table. It might not always be the right call to actually reduce it, but in this case (based on the parameter names) each of the branches seems to makes sense from a domain perspective, so why not do it?
- yakshaving_jgt 3y ago
  > so why not do it? Because wildcard pattern matches are error prone. When you add a new constructor, the compiler will remain satisfied that the pattern match is exhaustive and won't prompt you to verify the behaviour.
  - Quekid5 3y ago
    I understand your point, but it's unlikely that there's going to be new constructors added to Boolean :) EDIT: Oh, actually, nevermind. After reading more closely, I do agree that it might be reduced a bit too much!
  - iraqmtpizza 3y ago
    >wildcard pattern matches are error prone That's my problem with var in Java
munificent 3y ago
Just for kicks, here's a Dart version: enum ItemStatus { notAvailable, available, inUse } enum FieldState { hidden, readOnly, readWrite } FieldState decide(bool requiresApproval, bool canUserApprove, ItemStatus itemStatus) => switch ((requiresApproval, canUserApprove, itemStatus)) { (true, true, ItemStatus.notAvailable) => FieldState.hidden, (false, true, ItemStatus.notAvailable) => FieldState.hidden, (true, false, ItemStatus.notAvailable) => FieldState.hidden, (false, false, ItemStatus.notAvailable) => FieldState.hidden, (true, true, ItemStatus.available ) => FieldState.readWrite, (false, true, ItemStatus.available ) => FieldState.hidden, (true, false, ItemStatus.available ) => FieldState.readOnly, (false, false, ItemStatus.available ) => FieldState.hidden, (true, true, ItemStatus.inUse ) => FieldState.readOnly, (false, true, ItemStatus.inUse ) => FieldState.hidden, (true, false, ItemStatus.inUse ) => FieldState.readOnly, (false, false, ItemStatus.inUse ) => FieldState.hidden, }; As with F# and Haskell, the compiler will tell you if you didn't cover one of the combinations. In the case of Dart, we go ahead and make it a full compile-time error, not just a warning. The cool thing about pattern matching over tuples with compile-time exhaustiveness checking is that you can start simplifying and collapsing rows and the compiler will let you know if you made a mistake. I believe you can simplify the example here to: FieldState decide(bool requiresApproval, bool canUserApprove, ItemStatus itemStatus) => switch ((requiresApproval, canUserApprove, itemStatus)) { (_, _, ItemStatus.notAvailable) => FieldState.hidden, (false, _, ItemStatus.available ) => FieldState.hidden, (false, _, ItemStatus.inUse ) => FieldState.hidden, (true, false, ItemStatus.available ) => FieldState.readOnly, (true, _, ItemStatus.inUse ) => FieldState.readOnly, (true, true, ItemStatus.available ) => FieldState.readWrite, }; Doing that simplification is a useful exercise to then determine how to express the rules you're modeling in a succinct way.
emmanueloga_ 3y ago
I've built this sort of truth table in "plain code" and was always jealous of environments like embeddr, where things are a lot more readable and no manual alignment is required :-) [1]. Subtext [2] included a feature called "schematic tables" that is related to decision tables (demo [3], 8yr old video). When I saw Subtext's schematic tables I started to think of minimizing expressions, finding the complement, etc, to aid in writing correct boolean expressions. I think an algorithm like Quine–McCluskey [4] or espresso [5] could have applications to programming for refactoring boolean logic (normally these are used in electronics design). I don't know of any programming environment that could tell you if a boolean expression is a tautology or a contradiction... (I imagine a linter with SAT solver [6] powers could do this). In table form this would be obvious: a result column that is always true or always false. But then again you don't want to write a truth table for EVERY boolean expression on a program. Would be nice to be able to go back and forth from table to expression, minimize the expression, check satisfiability, etc. -- 1: https://markusvoelter.medium.com/the-evolution-of-decision-tables-80ce77bf984c https://markusvoelter.medium.com/the-evolution-of-decision-t... 2: https://www.subtext-lang.org/ https://www.subtext-lang.org/ 3: https://vimeo.com/140738254 https://vimeo.com/140738254 4: https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algori... 5: https://en.wikipedia.org/wiki/Espresso_heuristic_logic_minimizer https://en.wikipedia.org/wiki/Espresso_heuristic_logic_minim... 6: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
perryizgr8 3y ago
Just out of college and in my first job as a software engineer, I was excited to reduce the conditions in a piece of code using the K map reduction technique and then implement the resulting truth table with a switch case block. It was shot down pretty quickly by the reviewer because it was inscrutable and unverifiable to anyone without significant effort. Since then I've realised that such optimizations are the compiler's job :)
- blueberry87 3y ago
  Yeah, in any modern language with pattern matching stuff like this is absolutely the compiler's job, and can be done pretty well[1] - of course, there are plenty of legacy languages that don't have pattern matching, but seeing as it can be compiled straight to switches and whatnot, even the lowest level languages don't have /that/ much of an excuse. refs: [1]: http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf https://julesjacobs.com/notes/patternmatching/patternmatching.pdf https://julesjacobs.com/notes/patternmatching/patternmatchin...

72 points by chriskrycho 3y ago

good thing c# supports pattern match too. just this morning, I wrote something like this var thing = (enumA, enumB) switch { (EnumA.A,EnumB.A) => DoStuff(), _ => throw new Exception(), } suffice to say, c# is pretty ok, coming from ml family.

KineticLensman 3y ago
Rust's match is pretty cool as well. Here's Fizzbuzz, lifted from [0] match (i % 3 == 0, i % 5 == 0) { (false, false) => { }, (true, true) => { FizzBuzz }, (true, false) => { Fizz }, (false, true) => { Buzz } } I'm moving from C# to Rust at the moment and really enjoying it, especially now that I (almost) understand the borrow checker [0] https://stackoverflow.com/questions/43896431/c-sharp-equivalent-of-rusts-match https://stackoverflow.com/questions/43896431/c-sharp-equival...
- recursive 3y ago
  Can you match to (i % 3, i % 5) instead?
  - Philpax 3y ago
    You can, yes: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0c8baf63af6af6fed10a62b9d0e9a6dc https://play.rust-lang.org/?version=stable&mode=debug&editio...
- jsmith45 3y ago
  As you hopefully know, the modern C# equivalent is not bad either, especially with top level statements and implicit global usings (The following is the whole program): foreach (var i in Enumerable.Range(1,100)) { Console.WriteLine( (i%3==0,i%5==0) switch { (true, true) => "FizzBuzz", (true, _) => "Fizz", (_, true) => "Buzz", (_, _) => $"{i}" } ); } This is so much nicer than what was possible back when the linked question was asked.
  - recursive 3y ago
    It gets a bit nicer still. (i%3,i%5) switch { (0, 0) => "FizzBuzz", (0, _) => "Fizz", (_, 0) => "Buzz", (_, _) => i }
Smaug123 3y ago
Enums are a bit leaky, though, because C# enums can just have any old `int` chucked into them, so you really do need the final arm of the `match`. `(EnumA)100` will compile just fine!

deleted 3y ago

[deleted]

tczMUFlmoNk 3y ago

Somewhat surprised that the author doesn't go on to show how to reduce the truth table... let decide requiresApproval canUserApprove itemStatus = match requiresApproval, canUserApprove, itemStatus with | true, true, NotAvailable -> Hidden | false, true, NotAvailable -> Hidden | true, false, NotAvailable -> Hidden | false, false, NotAvailable -> Hidden | true, true, Available -> ReadWrite | false, true, Available -> Hidden | true, false, Available -> ReadOnly | false, false, Available -> Hidden | true, true, InUse -> ReadOnly | false, true, InUse -> Hidden | true, false, InUse -> ReadOnly | false, false, InUse -> Hidden ...to something like this: let decide requiresApproval canUserApprove itemStatus = match requiresApproval, canUserApprove, itemStatus with | _, _, NotAvailable -> Hidden | false, _, _ -> Hidden | true, true, Available -> ReadWrite | true, _, _ -> ReadOnly I would think that being able to see and effect this reduction is part of the benefit of writing out the whole table. It might not always be the right call to actually reduce it, but in this case (based on the parameter names) each of the branches seems to makes sense from a domain perspective, so why not do it?

yakshaving_jgt 3y ago
> so why not do it? Because wildcard pattern matches are error prone. When you add a new constructor, the compiler will remain satisfied that the pattern match is exhaustive and won't prompt you to verify the behaviour.
- Quekid5 3y ago
  I understand your point, but it's unlikely that there's going to be new constructors added to Boolean :) EDIT: Oh, actually, nevermind. After reading more closely, I do agree that it might be reduced a bit too much!
- iraqmtpizza 3y ago
  >wildcard pattern matches are error prone That's my problem with var in Java

munificent 3y ago

Just for kicks, here's a Dart version: enum ItemStatus { notAvailable, available, inUse } enum FieldState { hidden, readOnly, readWrite } FieldState decide(bool requiresApproval, bool canUserApprove, ItemStatus itemStatus) => switch ((requiresApproval, canUserApprove, itemStatus)) { (true, true, ItemStatus.notAvailable) => FieldState.hidden, (false, true, ItemStatus.notAvailable) => FieldState.hidden, (true, false, ItemStatus.notAvailable) => FieldState.hidden, (false, false, ItemStatus.notAvailable) => FieldState.hidden, (true, true, ItemStatus.available ) => FieldState.readWrite, (false, true, ItemStatus.available ) => FieldState.hidden, (true, false, ItemStatus.available ) => FieldState.readOnly, (false, false, ItemStatus.available ) => FieldState.hidden, (true, true, ItemStatus.inUse ) => FieldState.readOnly, (false, true, ItemStatus.inUse ) => FieldState.hidden, (true, false, ItemStatus.inUse ) => FieldState.readOnly, (false, false, ItemStatus.inUse ) => FieldState.hidden, }; As with F# and Haskell, the compiler will tell you if you didn't cover one of the combinations. In the case of Dart, we go ahead and make it a full compile-time error, not just a warning. The cool thing about pattern matching over tuples with compile-time exhaustiveness checking is that you can start simplifying and collapsing rows and the compiler will let you know if you made a mistake. I believe you can simplify the example here to: FieldState decide(bool requiresApproval, bool canUserApprove, ItemStatus itemStatus) => switch ((requiresApproval, canUserApprove, itemStatus)) { (_, _, ItemStatus.notAvailable) => FieldState.hidden, (false, _, ItemStatus.available ) => FieldState.hidden, (false, _, ItemStatus.inUse ) => FieldState.hidden, (true, false, ItemStatus.available ) => FieldState.readOnly, (true, _, ItemStatus.inUse ) => FieldState.readOnly, (true, true, ItemStatus.available ) => FieldState.readWrite, }; Doing that simplification is a useful exercise to then determine how to express the rules you're modeling in a succinct way.

emmanueloga_ 3y ago

I've built this sort of truth table in "plain code" and was always jealous of environments like embeddr, where things are a lot more readable and no manual alignment is required :-) [1]. Subtext [2] included a feature called "schematic tables" that is related to decision tables (demo [3], 8yr old video). When I saw Subtext's schematic tables I started to think of minimizing expressions, finding the complement, etc, to aid in writing correct boolean expressions. I think an algorithm like Quine–McCluskey [4] or espresso [5] could have applications to programming for refactoring boolean logic (normally these are used in electronics design). I don't know of any programming environment that could tell you if a boolean expression is a tautology or a contradiction... (I imagine a linter with SAT solver [6] powers could do this). In table form this would be obvious: a result column that is always true or always false. But then again you don't want to write a truth table for EVERY boolean expression on a program. Would be nice to be able to go back and forth from table to expression, minimize the expression, check satisfiability, etc. -- 1: https://markusvoelter.medium.com/the-evolution-of-decision-tables-80ce77bf984c https://markusvoelter.medium.com/the-evolution-of-decision-t... 2: https://www.subtext-lang.org/ https://www.subtext-lang.org/ 3: https://vimeo.com/140738254 https://vimeo.com/140738254 4: https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algori... 5: https://en.wikipedia.org/wiki/Espresso_heuristic_logic_minimizer https://en.wikipedia.org/wiki/Espresso_heuristic_logic_minim... 6: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

perryizgr8 3y ago

Just out of college and in my first job as a software engineer, I was excited to reduce the conditions in a piece of code using the K map reduction technique and then implement the resulting truth table with a switch case block. It was shot down pretty quickly by the reviewer because it was inscrutable and unverifiable to anyone without significant effort. Since then I've realised that such optimizations are the compiler's job :)

blueberry87 3y ago
Yeah, in any modern language with pattern matching stuff like this is absolutely the compiler's job, and can be done pretty well[1] - of course, there are plenty of legacy languages that don't have pattern matching, but seeing as it can be compiled straight to switches and whatnot, even the lowest level languages don't have /that/ much of an excuse. refs: [1]: http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf https://julesjacobs.com/notes/patternmatching/patternmatching.pdf https://julesjacobs.com/notes/patternmatching/patternmatchin...