[HN Gopher] Compile-Time Checked Truth Tables
___________________________________________________________________
Compile-Time Checked Truth Tables
Author : chriskrycho
Score : 42 points
Date : 2023-08-22 02:07 UTC (20 hours ago)
(HTM) web link (blog.ploeh.dk)
(TXT) w3m dump (blog.ploeh.dk)
| [deleted]
| emmanueloga_ wrote:
| 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-t...
|
| 2: https://www.subtext-lang.org/
|
| 3: https://vimeo.com/140738254
|
| 4:
| https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algori...
|
| 5:
| https://en.wikipedia.org/wiki/Espresso_heuristic_logic_minim...
|
| 6: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
| tczMUFlmoNk wrote:
| 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 wrote:
| > 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.
| mananaysiempre wrote:
| > wildcard pattern matches are error prone.
|
| True.
|
| Unfortunately, they can also be _asymptotically_ shorter than
| writing the whole thing out: for example, try writing a
| lexicographic comparison function for an AST type of your
| choosing and making it linear in the number of constructors.
|
| If the language is lazy, it can be more severe than that: in
| Haskell, andL False _ = False andL _
| rhs = rhs
|
| is the short-circuiting AND, while andS False
| False = False andS False True = False andS True
| False = False andS True True = True
|
| is the naive one.
| zogrodea wrote:
| I have a related anecdote. I generated a pattern matching
| system for Unicode grapheme cluster breaks once (using
| OCaml which is similar to F#), and it turned out to be very
| slow due to the branch mispredictions introduced by pattern
| matching.
|
| Later, I borrowed a trick learned from someone else and
| used a hashtable to store the relevant data (written to
| only once when the program starts) instead. At this point,
| the performance cost was so small that I couldn't tell any
| difference compared to before I introduced pattern
| matching.
|
| For what it's worth, there are about 18000 characters
| specified by Unicode for special handling with grapheme
| breaks[0] so I don't know how noticeable the difference
| would be with the pattern matching tables you're likely to
| encounter in real life.
|
| [0] https://www.unicode.org/Public/UCD/latest/ucd/auxiliary
| /Grap...
| mananaysiempre wrote:
| Yeah, the usual way to compile pattern matching is a
| decision tree, because once you decide to check one of
| the arguments it can completely change which of the
| remaining arguments is a better candidate to look at
| next. (Of course, in a lazy language, it's even more
| subtle, but ML is strict.) It's a bit like compiling
| switch statements, only more so, and I expect compilers
| for functional languages have less tuning for crazy
| corner cases like a 18k-entry table than, say, Clang,
| simply because they have less tuning crazy corner cases
| overall. (I once had Clang compile a switch into a lookup
| table and _stuff the table into a 64-bit constant_ , for
| crying out loud.)
|
| For Unicode tables, the usual approach is of course a
| radix trie, even if the traditional two-level trie from
| the Unicode 2.0 days is starting to look a bit bloated
| now and a three-level tree is quite a bit slower. A hash
| might be a good approach for some things. One potential
| downside is that it completely destroys memory locality,
| while normal Unicode data will usually use a fairly small
| subset of the characters; I'm not sure how important this
| would turn out to be. People (e.g. libutf and IIRC
| duktape) have also used a sorted table of alternating
| start- and endpoints of ranges.
|
| [The 18k figure sounds scarier than it is: 11k of those
| are precomposed Korean syllables encoded in a well-known
| systematic way, so for 0xAC00 <= codepoint < 0xAC00 + 19
| * 21 * 28 the table just says (if (codepoint - 0xAC00)
| mod 28 = 0 then LV else LVT).]
| iraqmtpizza wrote:
| >wildcard pattern matches are error prone
|
| That's my problem with var in Java
| Quekid5 wrote:
| 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!
| munificent wrote:
| 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.
| lemper wrote:
| 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 wrote:
| 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-
| equival...
| jsmith45 wrote:
| 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 wrote:
| Can you match to (i % 3, i % 5) instead?
| Philpax wrote:
| You can, yes: https://play.rust-
| lang.org/?version=stable&mode=debug&editio...
| Smaug123 wrote:
| 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!
___________________________________________________________________
(page generated 2023-08-22 23:01 UTC)