-
Notifications
You must be signed in to change notification settings - Fork 11
/
Overview.idr
123 lines (106 loc) · 5.95 KB
/
Overview.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
module BoundedContext.OrderTaking.Workflow.PlaceOrder.Overview
import Rango.BoundedContext.Workflow
%default total
-- Overview of the Place Order workflow:
--
-- The incoming order form gets validated
-- - if valid it is registered
-- - if not it is rejected
-- More precisely this can be represented as the following state transition:
--
-- ┌────────────────────────────┐
-- │ OrderForm │
-- └────────────────────────────┘
-- │
-- │ Validate Order
-- ▼
-- ┌─────────────┐ Create valid ┌============================┐
-- │ ValidOrder │ ◀────────────────────────── I Order I
-- └─────────────┘ └============================┘
-- │ │
-- │ Price │ Create invalid
-- ▼ ▼
-- ┌─────────────┐ ┌────────────────────────────┐
-- │ PricedOrder │ │ InvalidOrder │
-- └─────────────┘ └────────────────────────────┘
-- │ │
-- │ │ Queue
-- │ ▼
-- │ ┌────────────────────────────┐
-- │ │ InvalidOrderQueued │
-- │ └────────────────────────────┘
-- │ │
-- │ │ Create invalid order info
-- │ ▼
-- │ Create priced order info ┌────────────────────────────┐
-- └─────────────────────────────────────────▶ │ OrderInfo │
-- └────────────────────────────┘
--
-- Nodes represent the information we have, and edges represent the commands
-- that transforms information in this workflow.
-- Commands that have the same starting node are checks/decisions, one possible
-- path is selected during the interpretation of this process.
--
-- As in the order taking example, when we have an Order, it can be valid or invalid.
-- Next step is to represent this state transition in Idris as indexed datatypes.
||| States of the Order-Taking
public export
data State
= OrderForm
| Order
| ValidOrder
| PricedOrder
| InvalidOrder
| InvalidOrderQueued
| OrderInfo
-- The State is a simple ADT with some constructors.
||| Check of the OrderTaking transition;
|||
||| Decide if an order is valid or invalid.
public export
data Check : State -> State -> State -> Type where
CheckInvalidOrder : Check Order InvalidOrder ValidOrder
-- The Check is an indexed datatype with three indices, all the three indices are type of State.
||| State transition of the OrderTaking workflow.
public export
data Step : State -> State -> Type where
ValidateOrder : Step OrderForm Order
AddInvalidOrder : Step InvalidOrder InvalidOrderQueued
PriceOrder : Step ValidOrder PricedOrder
SendAckToCustomer : Step PricedOrder OrderInfo
SendInvalidOrder : Step InvalidOrderQueued OrderInfo
-- The Step is another indexed datatype, with two indices of State values.
||| Workflow definiton of the state transition system.
|||
||| See the graph above. This workflow represents an order-taking
||| process, which accepts or rejects an order, if the order
||| is accepted than prices it, if the order is invalid
||| registers it as an invalid order. In both cases it sends
||| information about that state of the order to the customer
public export
workflow : Workflow Step Check OrderForm OrderInfo
workflow = do
Do ValidateOrder
Branch CheckInvalidOrder
(do Do AddInvalidOrder
Do SendInvalidOrder)
(do Do PriceOrder
Do SendAckToCustomer)
-- In Idris the 'do' notation is tied to the the (>>) and the (>>=) bind operatiors, any type
-- that implements those operators is able to use the 'do' notation. This is a sintactical sugar
-- and helps us to write code which can be read naturally, in sequence and in branching.
-- This approach fits well to the sequential nature of the workflows.
---------------------------------------------------------------------------------------------------
-- Graph Source:
--
-- digraph {
-- OrderForm -> Order [label="Validate Order"];
-- InvalidOrder -> InvalidOrderQueued [label="Queue"];
-- ValidOrder -> PricedOrder [label="Price"];
-- PricedOrder -> OrderInfo [label="Create priced order info"];
-- InvalidOrderQueued -> OrderInfo [label="Create invalid order info"];
--
-- Order -> ValidOrder [label="Create valid"];
-- Order -> InvalidOrder [label="Create invalid"];
-- }
--