Is encountering impossible state symptomatic of a bad model?

Learn
1

Hello,

I’m implementing the 7 GUIs “Flight Booker” challenge in Elm.

With a slight variation in that I chose not to show the second input when selecting a one-way flight (I find that wouldn’t make sens).

Anyhow, there are a few spots in my update function that bother me, related to encountering impossible conditions, on lines 144, 155, 169 and 173 below :

On each line, I’ve explained why encountering the condition is incoherent.
To satisfy the compiler, I return a “bogus” (unchanged) model, “bogus” in the sens that this condition “should never happen” so returning the model as-is doesn’t make much sens.

I have some vague ideas how I could remove some of those but possibly at the cost of quite a lot of duplication.

I’d like to know what are your thoughts on this? I have encountered “catch-all” case expressions in learning material so I’m not sure if removing all impossible states is even possible, or if it’s just something to strive to?

In server programming, I usually decide to panic so that I can be made aware of a code path triggering, and that should never have triggered (sometimes that’s years later and depending on external factors).

I’m wondering how I should handle this in Elm, since by using some form of “catch-all” or returning a “bogus” as-is model, I’ll make later refactoring potentially less effective by masking away stuff that should light up when the code and requirements change. But also it’ll make being made aware of triggering an “impossible” branch more challenging in production because of no runtime error.

Thanks for your input

2

Personally, I think it’s great to Make Impossible States Impossible™.

I also think that, in some cases, instead of creating complex code to show the compiler that you’re right, it’s much more pragmatic and efficient to just use a catch-all and say “this should not be possible”.

Of course, then, when things change and the previously impossible condition becomes possible, you have a potential bug on your hands. That’s a trade-off =)

3

For sure :slight_smile:

I should maybe have mentioned that I’m quite interested in learning about how far I can push things on the software correctness spectrum (as a general idea, not strictly related to Elm).

Worrying about correctness obviously has a cost though, I do realize that.

4

When I come in a situation like you describe, where you need to cover state that should be impossible, I take a step back and redo the modelling.

I remember doing the 7 guis challenge years ago, but I didn’t finish it.

Feel free to check out my WIP.

5

Regarding how to “panic” in the case of impossible states, it can be done in the same way as any other thing in Elm. If you want to make the user of the software aware, set some value on the model and check that in order to show some UI. If you want to make yourself aware of this condition being encountered for any user, use a command to send a request to an http endpoint.

6

Re http endpoint, I have been considering using elm-sentry to capture these assumed impossible states

7 
        ( _, _ ) ->
            model

This is totally fine, because in this instance your case statement is over the event and the state:

update : Msg -> Model -> Model
update msg model =
    case ( msg, model ) of

Your Model is a custom type, which attempts to enumerate the possible states of the application. Think of it as a state machine. The events may trigger a transition of state in the state machine.

If you consider a state machine, with states S1…Sn, and events triggereing state transitions E1…Em. Not every event is possible in every state. That is to say that when you draw out a state machine on a piece of paper, you do not have lines coming out of each of S1…Sn, for each E1…Em, yielding a total number of transitions of size n times m. Instead, when you draw a state machine you only have some of E1…Em shown on each of the states. Formally, we say the transitions form a subset of the cross product of the states and the events, and in practice usually far less than n times m.

I highly recommend drawing the state machine on a piece of paper. Then translating that into code. It is fine to have a catch all for all the transitions that should not be allowed.

Here is an example of when an event would correctly be ignored:

You open a dialog box, and at the same time send a network request to fetch the data to populate the dialog with. The state is WaitingForData. Now the DataFetched event may come back and transition to DialogReady state. Or the user might hit the cancel button triggering the Cancel event and returning to the MainScreen state. If DataFetched arrives when already back in the MainScreen state, it just gets ignored by (_, _) -> model.

The DataFetched and Cancel events really do run in parallel in the real world, one on the network and the other within the user. This is generally true of most user interfaces since they interface with the real and parallel world outside of the machine. The purpose of the state machine is to marshal these events sequentially; an Elm program is an entirely sequential and deterministic thing. Sometimes events get ignored if they arrive at the wrong state.

1 Like
8

Thanks @perty

I checked out your code, but I’m not sure about your model.

If I tweak your init function, I can book a flight like this:

init : Model
init =
    { validModel = ValidModel
    , option = Return
    , departureDateString = "2023-03-01"
    , returnDateString = "2023-02-01"
    ...
    }

It seems to me that this is undesirable, I would prefer to find a model that does not allow the expression of an incoherent state. But maybe I’m wrong about that :slight_smile:

Yes that could be a strategy. But then you would have to create new code paths for paths that should never be take in the first place. That’d feel a bit weird.

Thanks for your lengthy explanation!! It makes a lot of sens!

I was only vaguely aware of FSM, turned off by overly simple examples or the recommended usage of libraries.

But I understand better now how this concept maps quite closely to the update function.

I found this great intro on the subject, on Youtube: https://youtu.be/2OiWs-h_M3A?t=572

And implemented this float parser example as an exercise (it’s a bit odd, the user drives the state machine forwards by clicking on buttons)

module Main exposing (..)

import Browser
import Html exposing (..)
import Html.Events exposing (onClick)



-- MODEL


type Model
    = Start (List Char)
    | AfterMinus (List Char)
    | SecondDigitOnwards (List Char)
    | AfterDot (List Char)
    | Mantissa (List Char)
    | ParseError
    | End


init : Model
init =
    -- Start (String.toList "1")
    -- Start (String.toList "1.")
    -- Start (String.toList "1.2")
    -- Start (String.toList "1.2x")
    -- Start (String.toList "1.23456")
    -- Start (String.toList "1.23456x")
    -- Start (String.toList "1.23456.1")
    Start (String.toList "x1.23456.1")



-- UPDATE


type Msg
    = Minus
    | Digit
    | Dot
    | Complete
    | Fail


transition : (List Char -> Model) -> List Char -> Model
transition onMore lst =
    case lst of
        [] ->
            ParseError

        _ :: t ->
            onMore t


update : Msg -> Model -> Model
update msg model =
    case ( msg, model ) of
        ( Minus, Start lst ) ->
            transition AfterMinus lst

        ( Digit, Start lst ) ->
            transition SecondDigitOnwards lst

        ( Digit, AfterMinus lst ) ->
            transition SecondDigitOnwards lst

        ( Digit, SecondDigitOnwards lst ) ->
            transition SecondDigitOnwards lst

        ( Dot, SecondDigitOnwards lst ) ->
            transition AfterDot lst

        ( Digit, AfterDot lst ) ->
            transition Mantissa lst

        ( Digit, Mantissa lst ) ->
            transition Mantissa lst

        ( Complete, Mantissa [] ) ->
            End

        ( Complete, SecondDigitOnwards [] ) ->
            End

        _ ->
            ParseError



-- VIEW


isHeadDigit : List Char -> Bool
isHeadDigit lst =
    case List.head lst of
        Nothing ->
            False

        Just h ->
            List.member h [ '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' ]


isHeadMinus : List Char -> Bool
isHeadMinus lst =
    List.head lst == Just '-'


isHeadDot : List Char -> Bool
isHeadDot lst =
    List.head lst == Just '.'


minusButton : Model -> Html Msg
minusButton model =
    case model of
        Start lst ->
            if isHeadMinus lst then
                button [ onClick Minus ] [ text "Minus" ]

            else
                text ""

        _ ->
            text ""


digitButton : Model -> Html Msg
digitButton model =
    let
        digitBtn lst =
            if isHeadDigit lst then
                button [ onClick Digit ] [ text "Digit" ]

            else
                text ""
    in
    case model of
        Start lst ->
            digitBtn lst

        AfterMinus lst ->
            digitBtn lst

        SecondDigitOnwards lst ->
            digitBtn lst

        AfterDot lst ->
            digitBtn lst

        Mantissa lst ->
            digitBtn lst

        _ ->
            text ""


dotButton : Model -> Html Msg
dotButton model =
    case model of
        SecondDigitOnwards (h :: _) ->
            if h == '.' then
                button [ onClick Dot ] [ text "Dot" ]

            else
                text ""

        _ ->
            text ""


completeButton : Model -> Html Msg
completeButton model =
    case model of
        SecondDigitOnwards [] ->
            button [ onClick Complete ] [ text "Complete" ]

        Mantissa [] ->
            button [ onClick Complete ] [ text "Complete" ]

        _ ->
            text ""


view : Model -> Html Msg
view model =
    let
        btnLst =
            [ minusButton model
            , digitButton model
            , dotButton model
            , completeButton model
            ]
    in
    div []
        [ h1 [] [ text "Parsing floats via state machine" ]
        , case model of
            End ->
                text "Finished!"

            ParseError ->
                text "Errored!"

            _ ->
                div []
                    (btnLst
                        ++ [ if btnLst == [ text "", text "", text "", text "" ] then
                                button [ onClick Fail ] [ text "Fail" ]

                             else
                                text ""

                           --    , hr [] []
                           --    , button [ onClick Minus ] [ text "MINUS" ]
                           --    , button [ onClick Digit ] [ text "DIGIT" ]
                           --    , button [ onClick Dot ] [ text "DOT" ]
                           --    , button [ onClick Complete ] [ text "COMPLETE" ]
                           --    , button [ onClick Complete ] [ text "FAIL" ]
                           ]
                    )
        , p [] [ text (Debug.toString model) ]
        ]



-- BOOTSTRAP


main : Program () Model Msg
main =
    Browser.sandbox { init = init, update = update, view = view }

I can see clearly now how, by designing the update function, Msg and Model types, one can constraint the state transitions quite nicely.

I’d be interested to learn more if anybody knows any good resources and exercises on the matter.

Thanks!

9

Note, in my mind case ( msg, model ) of is always an anti-pattern. To me, it’s better to do case msg of with a case model of in every branch. Sure, that’s more verbose, but then you can’t forget to handle some message.

2 Likes
10

Two rules that I’ve come up with for forms:

  1. Write everything twice.
  2. Make impossible states possible.

You need two models for a form: An “ugly” one that models the different inputs of the form, and a “nice” one that models valid outputs of the form.

For the nice output type, you might want to go with some variation of:

type Flight
  = OneWay Date
  | Return Date Date

In other words, it only makes sense having two dates for Return.

But for the ugly form input type, you might want to have:

type alias Form =
  { flightType : FlightType
  , departureDate : String
  , returnDate : String
  }

type FlightType
  = OneWay_
  | Return_

That model allows for two dates even for OneWay_. That’s useful so that the return date field isn’t cleared if you switch back and forth between OneWay_ and Return_. (I don’t think the 7GUIs description said anything about that, but it’s nice UX in my opinion.)

The dates are strings so that they can represent any user input (including invalid things).

Finally, you can create a validation function like so:

validate : Form -> Result Error Flight

type Error = ...
7 Likes
11

I second this advice. It’s the approach I tend to use as well.

12

You can find another interesting use of FSMs here as well. I used them to control input to this calculator, which also made it easy to test user input scenarios.

As for recommendations for FSMs. I learned about them through Michael Sipser’s “Introduction to the Theory of Computation” but that might be too heavy on the math. If it is then try the Wikipedia article on the topic and see where that takes you.

13

For the toy float state machine, it’s interesting thinking about the equivalent regex and the state machine that it builds internally which might match your states.

-?[0-9]+(.[0-9]+) . If you simplify to only one digit value, it gets down to -?0+(.0+). That can be expanded out to (-|)00*(.00*|).

14

I went through my code again and tried to make it more readable. I also updated the Readme.

Pretty much as @lydell is saying, the mindset is that there are two models, one that represents the input the user has made so far and one that is the result of validating that input.

The user’s input is of course not always correct but we still need to represent it.

In my example, the validated model is not stored, it is only reachable as a result of a function that operates on the input model: validateModel : Model -> ValidatedModel

At first I stored the validation result but that is like having a cache since it is a function of the input. However, it is easier to debug the validation if it is stored. But who needs debugging, anyway. :slight_smile:

To answer the question of this thread, yes, impossible states should always be impossible but user input can look like anything. :stuck_out_tongue_winking_eye:

1 Like
15

Always really? I found @rupert’s reference to FSMs quite enlightening in this regard, I don’t really see how that could work given my latest version (which I’m quite happy with) having the following model:

type Model
    = UserEdit Form
    | ConfirmBooking Flight

I have to account for “normal” impossible states on line 165 (with a catch-all), but doing otherwise would “spread” the same problem over the update function, in multiple places.

Maybe I’m missing something?

That was great advice, many thanks! Storing the raw user inputs did cross my mind but I hadn’t that clear of an idea so your suggestions really helped.

The validate function was the last missing piece, which I chose to use mostly at the view layer, which worked great.

That was a good point

Thanks I’ll dig into it, I like it! Your code is very clean.

Thanks for the heads up, I did notice that :slight_smile:

I just found it really interesting that I could implement the equivalent functionality in such an easy way.

3/4 of what I’ve found on the subject of state machines feels rather dull, I haven’t found a great resource on the matter yet.

Thanks @perty, I’ll look at your code again.

16

I think lydell is meaning to transform this:

    case (msg, model) of 
        ...

        ( DepartureChanged s, UserEdit form ) ->
            UserEdit <|
                { form | departureDate = s }

Into this:

    case msg of 
        ...

        ( DepartureChanged s) -> 
           case model of 
               UserEdit form ->
                  UserEdit <| { form | departureDate = s }

               _ -> model

Same thing, just you have to write many more individual cases for unmatched models _ -> model, rather than catch many with a single (_, _) -> model. But it has the advantage of making the top-level case msg complete over all the Msg constructors, so you cannot miss one.

Generally, I have not found using (_, _) -> model to be too much of a problem. Except I do admit that occasionally as code evolves there have been some unused and harmless Msg constructors lingering. elm-review has a rule to clean them up: NoUnused.CustomTypeConstructors - elm-review-unused 1.1.29

17

The basic state machine material is fairly quick to learn. I think some people have taken the idea further like some react library that I can’t recall.

If you want to get deep into it, tla+ could be used to reason about orderings of messages and their effects on a state machine. You could use it to try to prove certain UI bugs can never happen with a given set of msg update handlers and model. I have never done this, but if you are looking for more challenge, just pointing that area out.

18

Is encountering impossible state symptomatic of a bad model?

In general, I would say yes.

I’ve recently picked up Elm again and I find it is such a different model of programming. For example, I spend a ton of time getting my model right.

It sounds like the problem you are working on may be a workflow. One pattern I found useful is using a phantom types, for example:

type Step step
    = Step Order

It’s kind of a brain twister, but with this type declared, you can now do things like:

type OrderInputs =
  OrderInputs

type ValidOrder =
    ValidOrder

validate : Step OrderInputs -> Step ValidOrder
validate x =
     ...

To your original question, I had a recent experience where I thought I had the right model, but found I had a possible state I couldn’t represent! :slight_smile: By sticking to a model that could not represent invalid states, Elm helped me discover my mental model was not correct.

See

1 Like
19

Thanks for the feedback @rupert. I think I would prefer having a catch-all in one place rather than many places. Elm-review looks handy in that regard.

Interesting! This looks like an great suggestion, I’ll look into this, many thanks.

I suspect this is key, and pretty subtle at times. Thanks for the phantom type suggestion, I’ll read up on it to see if it helps :slight_smile:

20

That’s because state machines are hard to create in an idiomatic [1] way in most languages. But if you implement something “almost” like state machine it looks trivial.

Elm TEA with messages, model and implicit update function sounds almost like state machine. But you miss connection between events and states. Yes, you have update function but most of it is runtime assertion. You don’t enforce in type system state transitions - it’s hard to create invariant that after AddToCart message you will always be in the state HasProductInCart. Also it’s almost impossible to ensure that user can only emit subset of messages in specific state - it should be impossible to get RemoveFromCart message when in state EmptyCart.

There’s nice article about more robust state machines for versed in Haskell: https://wickstrom.tech/finite-state-machines/2017/11/19/finite-state-machines-part-2.html
Sadly, it mixes handling effects, so it is more complex that it need to be.

[1] I mean implementation that feel native to language. In Clojure you could implement state machine as a data structure but after literal translation to Elm it won’t be idiomatic because you find yourself without type safety (or very weak type safety).

1 Like