Implementation using Transit

State and message types

The state machine represents the four land areas as states (uppercase letters A, B, C, and D) and the seven bridges as messages (lowercase letters a through g). Each message represents crossing a specific bridge, which transitions between the corresponding land areas.

type State = Variant
  ( "A" :: {}
  , "B" :: {}
  , "C" :: {}
  , "D" :: {}
  )

type Msg = Variant
  ( "a" :: {}
  , "b" :: {}
  , "c" :: {}
  , "d" :: {}
  , "e" :: {}
  , "f" :: {}
  , "g" :: {}
  )

^{🗎 test/Examples/BridgesKoenigsberg.purs L25-L40}

Type-level specification

Since bridges can be crossed in both directions, each bridge creates a bidirectional connection between two land areas. In the type-level specification, we define transitions using the syntax "State1" |< "Message" >| "State2", which effectively defines two transitions: one from State1 to State2 and one from State2 to State1.

type BridgesTransit =
  Transit
    :* ("A" |< "a" >| "B")
    :* ("A" |< "b" >| "B")
    :* ("A" |< "c" >| "C")
    :* ("A" |< "d" >| "C")
    :* ("A" |< "e" >| "D")
    :* ("B" |< "f" >| "D")
    :* ("C" |< "g" >| "D")

^{🗎 test/Examples/BridgesKoenigsberg.purs L42-L50}

The Update Function

However, in the update function we need to explicitly handle both directions of each bridge as shown below.

update :: State -> Msg -> State
update = mkUpdate @BridgesTransit
  (match @"A" @"a" \_ _ -> return @"B")
  (match @"B" @"a" \_ _ -> return @"A")

  (match @"A" @"b" \_ _ -> return @"B")
  (match @"B" @"b" \_ _ -> return @"A")

  (match @"A" @"c" \_ _ -> return @"C")
  (match @"C" @"c" \_ _ -> return @"A")

-- And so on ... (13 lines omitted)

^{🗎 test/Examples/BridgesKoenigsberg.purs L52-L73}