Compile-Time Checked Truth Tables | Hacker News Reader

Compile-Time Checked Truth Tables

blog.ploeh.dk

72 pointschriskrycho19 comments

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?

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

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!

>wildcard pattern matches are error prone

That's my problem with var in Java

> 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 naïve one.

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

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

You can write it pretty compactly in Rust without introducing wildcards over non-boolean arguments. If you're extra paranoid you can write `true | false` instead of _ for those patterns in the below example

    match (requires_approval, can_user_approve, item_status) {
        (true, true, Available) => ReadWrite,
        (true, false, Available) => ReadOnly,
        (true, _, Inuse) => ReadOnly,
        (true, _, NotAvailable) => Hidden,
        (false, _, NotAvailable | Available | InUse) => Hidden,
    }

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.

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.

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

Can you match to (i % 3, i % 5) instead?

You can, yes: https://play.rust-lang.org/?version=stable&mode=debug&editio...

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.

It gets a bit nicer still.

    (i%3,i%5) switch {
        (0, 0) => "FizzBuzz",
        (0, _) => "Fizz",
        (_, 0) => "Buzz",
        (_, _) => i
    }

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!

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

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

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 https://julesjacobs.com/notes/patternmatching/patternmatchin...

Reply on news.ycombinator.com