DEV Community: 1hko

Finding Truth with Elm

1hko — Sat, 21 Jul 2018 00:20:05 +0000

When working with propositional logic one needs to create truth tables such as the one below —

P	Q	¬P	¬P ∨ Q	P ⇒ Q
T	T	F	T	T
T	F	F	F	F
F	T	T	T	T
F	F	T	T	T

Table 1

P ⇒ Q is logically equivalent to ¬P ∨ Q

It's important to do the exercise, but it's also easy to make mistakes. If we had a program generate the truth table for us, we could be more certain of the results. And it enables laziness so of course we want to do this.

Goal

The program should be intuitive and simply take a list of propositional expressions. Analysis of the expressions will determine which True/False permutations to construct. For example, the following set of expressions contains 3 unique variables P, Q and R —

P	Q	R	(P ⇒ Q) ⇒ R	P ⇒ (Q ⇒ R)	(P ⇒ R) ∨ (Q ⇒ R)
T	T	T	T	T	T
T	T	F	F	F	F
T	F	T	T	T	T
T	F	F	T	T	T
F	T	T	T	T	T
F	T	F	F	T	T
F	F	T	T	T	T
F	F	F	F	T	T

Table 2

⇒ is not commutative

(P ⇒ Q) ⇒ R is not equivalent to P ⇒ (Q ⇒ R)

P ⇒ (Q ⇒ R) is logically equivalent to (P ⇒ R) ∨ (Q ⇒ R)

Now available as a package

This program now exists in the Elm package repository, 1hko/elm-truth-table. The code you see in this post is mostly the same with a few things renamed.

Possible API

I wasn't looking for anything fancy. Propositions should be easy to specify allowing the user to specify any amount of variables in a set of expressions —

type Expr =
    -- ...


truthTable : List Expr -> Html msg
truthTable exprs =
    -- ...


-- table 1
truthTable
    [ Not (Var "P")                  -- ¬P
    , Or (Not (Var "P")) (Var "Q")   -- ¬P ∨ Q
    , Implies (Var "P")  (Var "Q")   -- P ⇒ Q
    ]


-- table 2
truthTable
    -- (P => Q) => R
    [ Implies (Implies (Var "P")  (Var "Q")) (Var "R")

    -- P => (Q => R)
    , Implies (Var "P") (Implies (Var "Q")  (Var "R"))

    -- (P ⇒ R) ∨ (Q ⇒ R)
    , Or (Implies (Var "P") (Var "R")) (Implies (Var "Q") (Var "R"))
    ]

Later we can make a String -> Expr function later that parses "Q => P" : String to Implies (Var "Q") (Var "P") : Expr. But for now, this is all we need to get started.

Implementation

A single union type Expr is sufficient for our program's needs. I'll show the complete type here but know that I completely implemented one variant before moving onto the next

type Expr
    = Or Expr Expr
    | And Expr Expr
    | Xor Expr Expr
    | Implies Expr Expr
    | Equiv Expr Expr
    | Not Expr
    | Var String

Table Header

Every table starts with a <thead>. Our program needs to analyze and create column headers based on the input expressions. In Table 1 we saw —

P	Q	¬P	¬P ∨ Q	P ⇒ Q
…	…	…	…	…

Table 1

One column header for each variable appearing in the set of expressions; P and Q

One column for each expression – ¬P, ¬P ∨ Q, P ⇒ Q

To compute the columns for each variable, we create vars —

vars : Expr -> Set String
vars expr =
    case expr of
        Or a b ->
            Set.union (vars a) (vars b)

        Xor a b ->
            Set.union (vars a) (vars b)

        And a b ->
            Set.union (vars a) (vars b)

        Implies a b ->
            Set.union (vars a) (vars b)

        Equiv a b ->
            Set.union (vars a) (vars b)

        Not a ->
            vars a

        Var a ->
            Set.singleton a


And (Var "P") (Var "Q") |> vars
-- [ "P", "Q" ] : Set String

We can convert each expression to a string to be used in the remaining column headers —

exprToString : Expr -> String
exprToString expr =
    case expr of
        And a b ->
            exprToString a ++ " ∧  " ++ exprToString b

        Or a b ->
            exprToString a ++ " ∨ " ++ exprToString b

        Xor a b ->
            exprToString a ++ " ⊕ " ++ exprToString b

        Implies a b ->
            exprToString a ++ " ⇒ " ++ exprToString b

        Equiv a b ->
            exprToString a ++ " ⇔ " ++ exprToString b

        Not a ->
            "¬" ++ exprToString a

        Var a ->
            a


Implies (Var "P") (Var "Q") |> exprToString
-- "P ⇒ Q" : String

We can start filling in some of the implementation for truthTable now —

truthTable : List Expr -> Html msg
truthTable exprs =
    let
        ids =
            exprs
                |> List.map vars
                |> List.foldl Set.union Set.empty
                |> Set.toList

        columns =
            ids ++ List.map exprToString exprs

        -- ...
    in
    Html.table [ Attributes.style [ ( "width", "100%" ) ] ]
        [ Html.thead [] [ tableHeader columns ]
        , -- ...
        ]


tableHeader : List String -> Html msg
tableHeader labels =
    labels
        |> List.map (tableCell [ ( "font-weight", "bold" ) ])
        |> Html.tr []


tableCell : List ( String, String ) -> String -> Html msg
tableCell style text =
    Html.td [ Attributes.style style ] [ Html.text text ]

Table Rows

Moving along, we get to <tbody>. In Table 1 we see that True/False values need to be generated for each possible scenario of P and Q —

P	Q	¬P	¬P ∨ Q	P ⇒ Q
T	T	…	…	…
T	F	…	…	…
F	T	…	…	…
F	F	…	…	…

Table 1
all possible True/False permutations for 2 variables, P and Q

When the set of expressions expanded to include a third variable, R, in Table 2, another column was added, and more True/False values permutations too —

P	Q	R	(P ⇒ Q) ⇒ R	P ⇒ (Q ⇒ R)	(P ⇒ R) ∨ (Q ⇒ R)
T	T	T	…	…	…
T	T	F	…	…	…
T	F	T	…	…	…
T	F	F	…	…	…
F	T	T	…	…	…
F	T	F	…	…	…
F	F	T	…	…	…
F	F	F	…	…	…

Table 2
all possible True/False permutations for 3 variables, P and Q and R

We implement permute to generate the values needed fill in each row —

permute : Int -> List a -> List (List a)
permute n list =
    let
        loop acc n xs =
            if n == 0 then
                [ acc ]
            else
                list
                    |> List.concatMap (\x -> loop (acc ++ [ x ]) (n - 1) xs)
    in
    loop [] n list 


permute 2 [ "A", "B" ]
-- [ [ "A", "A" ]
-- , [ "A", "B" ]
-- , [ "B", "A" ]
-- , [ "B", "B" ]
-- ] : List (List String)

Given a list of variables and a list of values, we make it possible to evaluate an expression —

makeEnv : List String -> List Bool -> Env
makeEnv ids values =
    values
        |> List.map2 (,) ids
        |> Dict.fromList


eval : Env -> Expr -> Result String Bool
eval env expr =
    case expr of
        And a b ->
            Result.map2 (&&) (eval env a) (eval env b)

        Or a b ->
            Result.map2 (||) (eval env a) (eval env b)

        Xor a b ->
            Result.map2 xor (eval env a) (eval env b)

        Implies a b ->
            Result.map2 implies (eval env a) (eval env b)

        Equiv a b ->
            Result.map2 equiv (eval env a) (eval env b)

        Not a ->
            Result.map not (eval env a)

        Var a ->
            Dict.get a env
                |> Result.fromMaybe ("unbound identifier: " ++ toString a)


And (Var "P") (Var "Q")
    |> eval (makeEnv [ "P", "Q" ], [ True, False ])
    -- Ok False : Result String Bool

To finish truthTable, we first generate the True/False value permutations and then evaluate them for each expression —

truthTable : List Expr -> Html msg
truthTable exprs =
    let
        ids =
            -- ...

        columns =
            -- ...

        count =
            List.length ids

        rows =
            permute count [ True, False ]
                |> List.map (tableRows (makeEnv ids) exprs)
    in
    Html.table [ Attributes.style [ ( "width", "100%" ) ] ]
        [ Html.thead [] [ tableHeader columns ]
        , Html.tbody [] rows
        ]

Finally we write tableRows to glue all the pieces together —

tableRows : (List Bool -> Env) -> List Expr -> List Bool -> Html msg
tableRows makeEnv exprs values =
    let
        env =
            makeEnv values

        results =
            exprs
                |> List.map (eval env)
                |> List.foldr (Result.map2 (::)) (Ok [])
                |> Result.map ((++) values)
                |> Result.withDefault []

        viewCell truth =
            if truth then
                tableCell [ ( "color", "#19A974" ) ] "T"
            else
                tableCell [ ( "color", "#E7040F" ) ] "F"
    in
    results
        |> List.map viewCell
        |> Html.tr []

Practical Application

"If user is logged in, and token is not invalid, and user belongs to editors, and post is editable, and post is not locked then ..." – Writing programs that are easy to read is difficult. Sometimes complex logical propositions can be replaced with a simplified equivalent expression. Truth tables help us identify these equivalences

P	Q	(¬P) ∧ (¬Q)	¬(P ∨ Q)
T	T	F	F
T	F	F	F
F	T	F	F
F	F	T	T

Table 3
  truthTable
      [ And (Not (Var "P")) (Not (Var "Q"))
      , Not (Or (Var "P") (Var "Q"))
      ]
De Morgan's Law: ¬(P ∨ Q) is equivalent to (¬P) ∧ (¬Q)

ie, "not cloudy or raining" is equivalent to "not cloudy and not raining"

Truth Table Generator

Find truth for yourself with the full source code provided on ellie-app.

To write this post, I used this online utility to convert HTML tables to GHF Markdown

To-do

I will continue to make improvements on this as time permits

exprToString should include parentheses () disambiguate expressions like P ⇒ Q ⇒ R
Expr union type can probably be simplified to type Expr = Unary ... | Binary ...
a String -> Expr parser
Your ideas here 🔥

Retrying failed requests in Elm... without the headache

1hko — Fri, 29 Jun 2018 23:06:39 +0000

I needed a generic way to retry requests that fail. I did not want to litter my model with extra state or clutter my update function by having to handle additional cases for each request's code paths.

I found panosoft/elm-cmd-retry but it depends on native code and meets neither of the requirements set above.

Wishful Thinking

It should be intuitive to use —

decoder
    |> Http.get url
    |> Retry.send DataReceived

It should allow us to retry with configuration —

decoder
    |> Http.get url
    |> Retry.sendWith { retries = 3, interval = 10 * Time.second } DataReceived

Implementation

Here's my best attempt at the Retry module. I tweaked the API thanks to some comments I received on the Elm discourse. The revised implementation also makes it possible to retry any Task using retry or retryWith. It compiles and works as intended in my program.

At a glance —

default : Config
retry : Task x a -> Task x a
retryWith : Config -> Task x a -> Task x a
send : (Result Http.Error a -> msg) -> Http.Request a -> Cmd msg
sendWith : Config -> (Result Http.Error a -> msg) -> Http.Request a -> Cmd msg

Complete implementation —

module Retry exposing (Config, default, retry, retryWith, send, sendWith)

import Http
import Process
import Task exposing (Task)
import Time exposing (Time)


type alias Config =
    { retries : Int
    , interval : Time
    }


default : Config
default =
    { retries = 5
    , interval = 1 * Time.second
    }


retry : Task x a -> Task x a
retry =
    retryWith default


retryWith : Config -> Task x a -> Task x a
retryWith config task =
    task |> Task.onError (onError config task)


send : (Result Http.Error a -> msg) -> Http.Request a -> Cmd msg
send =
    sendWith default


sendWith : Config -> (Result Http.Error a -> msg) -> Http.Request a -> Cmd msg
sendWith config resultToMessage req =
    let
        task =
            Http.toTask req
    in
        task
            |> Task.onError (onError config task)
            |> Task.attempt resultToMessage


onError : Config -> Task x a -> x -> Task x a
onError config task error =
    if config.retries == 0 then
        let
            _ =
                Debug.log "failed retrying" error
        in
            Task.fail error
    else
        let
            _ =
                Debug.log ("retrying " ++ (toString config.retries)) error

            next =
                task
                    |> Task.onError (onError { config | retries = config.retries - 1 } task)
        in
            Process.sleep config.interval
                |> Task.andThen (always next)

How to use it

As demonstrated in the example below we meet our goals. Our model is not required to keep track of extra state and it's easy to convert any single-attempt request into a request that retries itself.

module SomeModule exposing (..)

import Retry
import User exposing (User)
...


type alias Model =
    { users : List User }


type Msg
    = UsersReceived (Result Http.Error (List User))


init : ( Model, Cmd Msg )
init =
    ( { users = [] }, getUsers )


getUsers : Cmd Msg
getUsers =
    (Decode.list User.decode)
        |> Http.get "/users.json"
        |> Retry.send UsersReceived


update : Msg -> Model -> ( Model, Cmd Msg )
update msg model =
    case msg of
        UsersReceived (Ok users) ->
            { model | users = users }
                ! []

        UsersReceived (Err e) ->
            let
                _ =
                    Debug.log "request failed" e
            in
                ( model, Cmd.none )

Feedback

I'm new to Elm and I'm asking the community for general feedback on this module.

Can you see problems I may encounter with it?
Can you see ways in which it can be improved?
Am I breaking any Elm conventions?

Original API

Originally I had written the Retry module with retry and retryWith functions that returned a Task. This required the programmer to use Task.attempt to create the necessary Cmd. If possible, it's best to keep this implementation detail out of the programmer's mind entirely. The Retry.send and Retry.sendWith API remedies this problem

-- original API leaks Task abstraction
decoder
    |> Http.get url
    |> Retry.retry
    |> Task.attempt DataReceived

-- proposal
decoder
    |> Http.get url
    |> Retry.retry DataReceived

-- proposal with configuration
decoder
    |> Http.get url
    |> Retry.retryWith { ... } DataReceived

-- new API
decoder
    |> Http.get url
    |> Retry.send DataReceived

-- new API with configuration
decoder
    |> Http.get url
    |> Retry.sendWith { retries = 3, interval = 10 * Time.second } DataReceived

P	Q	R	(P ⇒ Q) ⇒ R	P ⇒ (Q ⇒ R)	(P ⇒ R) ∨ (Q ⇒ R)
T	T	T	…	…	…
T	T	F	…	…	…
T	F	T	…	…	…
T	F	F	…	…	…
F	T	T	…	…	…
F	T	F	…	…	…
F	F	T	…	…	…
F	F	F	…	…	…

P	Q	R	(P ⇒ Q) ⇒ R	P ⇒ (Q ⇒ R)	(P ⇒ R) ∨ (Q ⇒ R)
T	T	T	…	…	…
T	T	F	…	…	…
T	F	T	…	…	…
T	F	F	…	…	…
F	T	T	…	…	…
F	T	F	…	…	…
F	F	T	…	…	…
F	F	F	…	…	…

P	Q	R	(P ⇒ Q) ⇒ R	P ⇒ (Q ⇒ R)	(P ⇒ R) ∨ (Q ⇒ R)
T	T	T	…	…	…
T	T	F	…	…	…
T	F	T	…	…	…
T	F	F	…	…	…
F	T	T	…	…	…
F	T	F	…	…	…
F	F	T	…	…	…
F	F	F	…	…	…