Introduction¶

Machines as implemented in Freya (internally using the Hephaestus library) are ways to program based on decisions.

Many problems (particularly problems like how to respond to an HTTP request) can be modelled in this way – as a series of decisions (boolean – true/false – decisions) to be made on the way to eventually arriving at a result. You can imagine the process of responding to an HTTP request as a series of suitable decisions – for example:

Is the server in a state to respond?
    true: continue
    false: return "503 Service Unavailable"

Is the version of HTTP being requested supported?
    true: continue
    false: return "505 HTTP Version Not Supported"

etc. until a suitable response is determined and returned.

As you can see, this is effectively a tree of decisions – a binary tree. The machine model requires that the logic that needs to be expressed is encoded in this form – as a tree of decisions, where the leaves represent the action that should result upon reaching the leaf.

In the case of an HTTP machine, handling an HTTP request, the endpoints would represent response handlers to be invoked, sending the chosen HTTP response back to the client.

Exemplar¶

The HTTP problem will continue to be used in the machine design topic as the common example case. This provides concrete examples, as well as tying the topic directly to the implementation of one of the most powerful parts of the Freya stack, a full-featured HTTP machine implementation.

The next section will cover Decisions in more detail, and begin to introduce some of the approaches taken to machines in the implementation.

Configuration¶

When defining a machine, Hephaestus does not expect to be given a ready-made decision, it expects to receive a function which will return a decision. This function takes an instance of a configuration type and returns a decision, enabling for runtime configuration of each decision. In Hephaestus terms, the decision tree initially is a prototype, and will only become a tree of actual decisions once it has been configured with appropriate data.

In effect, a decision is effectively defined as the following type (this is a simplification):

type Decision<'configuration> =
    'configuration -> DecisionValue

It may not be immediately obvious why this is useful, but it begins to become clearer when a decision value is explored.

Values¶

The act of configuring a decision, resulting in a decision value, allows for some significant optimisations to be made if a decision value is defined in a certain way.

Returning to the example of handling an HTTP request, consider a case with the following decision:

Is the URI too long?
    true: return "414 URI Too Long"
    false: continue

If the implementation of that decision is to compare the length of the request URI against a maximum length given in the configuration, it’s possible that the result of the decision is already known. For example, if the maximum allowed length of a URI configured was “infinite” then the result of the decision will always be false. If the maximum allowed length was zero, then the result will always be true!

This applies widely – many decisions are based on information provided as part of configuration, and a significant subset can be known ahead of running the machine.

For this reason, a decision value is effectively defined as the following type: (again, a simplification):

type DecisionValue =
    | Function of // ...function returning bool
    | Literal of bool

In this way, after configuration the decision tree is a tree of decision values, where the decision value is either a function to be evaluated at runtime to give a result, or a known result. This property will be extremely useful later in Optimisation.

State¶

In the Overview, you saw the example decision:

Is the version of HTTP being requested supported?
    true: continue
    false: return "505 HTTP Version Not Supported"

It’s clear that to implement that decision, the decision will need access to the request. This is accomplished in machines by passing the state to a machine to run it. So in the HTTP example, the request state might be passed to the first decision, so that it can return a result.

In fact, in Hephaestus, the decision actually returns a result – and a new state, which will be passed to the next decision. This allows decisions to both read relevant data, and potentially change the state for the following decisions. This is not commonly used, but can allow for more complex logic to be expressed.

This gives a slighly more realistic definition for the decision value type (again, simplified):

type DecisionValue<'state> =
    | Function of ('state -> bool * 'state)
    | Literal of bool

In this way, it is also possible to more accurately define the original decision type:

type Decision<'configuration,'state> =
    'configuration -> DecisionValue<'state>

This is now close enough to the actual implementation to understand the basic machine decision model, and the fundamental approach to configuring decisions.

In the next section on Terminals, the computational model will take shape further.

Configuration¶

In Decisions, the configuration process of decisions – from an unconfigured decision to a decision value once supplied with configuration data – was outlined. Terminals go through a similar process, being configured with the same configuration value before being “ready”.

As with decisions, they can be thought of as a simple type (simplified):

type Terminal<'configuration> =
    'configuration -> TerminalValue

In the case of terminals, the logic is somewhat simpler than with decisions in one sense – the terminal is only meaningful when run, so there is no consideration of a terminal being known ahead of time.

State¶

Also as with decisions, terminals need to act upon the input data, the state, to produce the result required. There is no need for them to produce a boolean result to determine what action to take next however – they are by definition the last part of a machine computation.

The terminal value can be seen then approximately as being (again, simplified):

type TerminalValue<'state> =
    | Terminal of 'state -> 'state

As you can see, the state is returned so that machines may fit in to broader computations, be composed, etc.

Results¶

There is one addition – the result of a machine computation. Although the computation as described may have modified (or returned a new instance) of the state provided, it currently has no responsibility to return a value. This is the responsibility of the terminal, and leads to this definition, expanded to encompass a result type (as ever, simplified):

type TerminalValue<'result,'state> =
    | Terminal of 'state -> 'result * 'state

This now allows for a more complete definition of the terminal type also:

type Terminal<'configuration,'result,'state> =
    'configuration -> TerminalValue<'result,'state>

This is again close enough to the meaning of the actual implementation to see the shape of a machine computation – and to note that it can be parameterized by the types of the configuration data, the result, and the state passed through the computation.

This gives a very flexible model, and in the following sections on Optimisation and Application within Freya, you will see how this model allows for an efficient execution approach, and the concrete implementation of the machine model in Freya.

Reachability¶

The simple but effective approach taken is based on the premise that where a decision is a literal, it is already possible to tell which subsequent branch of the tree is reachable, and which is not. Wherever a decision is a literal, it is possible to prune the decision tree, effectively removing the decision entirely, and creating a new tree where the execution path will go directly to the appropriate sub-tree.

Hephaestus trees are not defined to be pure trees (branches can join, so two paths can lead to the same decision). This requires a slightly more complex algorithm to safely prune the tree structure, but once it is pruned the tree becomes a tree where all remaining decisions are functions and not literals.

This can have significant impact on performance and complexity of the eventual decision tree. The Freya HTTP machine in the default pre-configured, pre-optimisation stage, has several hundred decisions, forming a large and complex tree. If given minimal configuration (which will result in many of these decisions assuming default, literal values) this number goes down to around five decisions in total!

As configuration becomes more complex, this number begins to rise, but the resulting tree is always significantly simpler than the potential maximal tree.

Implications¶

The implications of optimising the decision tree in this way on program design are worth noting.

First, in the overall design of the tree, wholesale duplication of logic can be permitted, as any unneeded logical paths will be removed before runtime use by the configuration and optimisation process.

Second, the expectation of what will be run becomes less important – as sections of logic may be optimised away, the expectation shifts to only running what is relevant, leading to thinking more declaratively about the overall logic. Interactions between logical elements are reduced in importance, and the importance of simple logical decisions comes to the fore, emphasising the decision based nature of the machine approach further.

The next section on Application gives some detail on the adoption of the machine model within Freya.

Syntax¶

The URI Template Router defines a custom computation expression (simpler and more limited than the freya computation expression. The computation expression uses a custom operation to let you define routes in a simple, expressive and typed way. The computation expression is named freyaUriTemplateRouter but is also aliased to freyaRouter for convenience!

Definitions¶

Routes are defined by specifying a requirement for the HTTP method (or verb), a requirement for the path, and the Pipeline function to call if the route is matched. Route matching effectively happens in definition order precedence, although the router internally converts the route definitions to an optimised trie for performance reasons.

Strongly typed values are used for the requirements, using types taken from the Types libraries, in this case Freya.Types.Http and Freya.Types.Uri.Template, as well as types from Freya.Routers.Uri.Template. Here’s an annotated example of setting up a router, including opening appropriate modules/namespace:

open Freya.Core
open Freya.Routers.Uri.Template
open Freya.Types.Http
open Freya.Types.Uri.Template

// Handlers

let handlerA =
    freya {
        return Next }

let handlerB =
    freya {
        return Next }

// Routing

let routeA =
    UriTemplate.parse "/a/{id}"

let routeB =
    UriTemplate.parse "/b/{name}"

let routes =
    freyaRouter {
        route Any routeA handlerA
        route (Methods [ GET; OPTIONS ]) routeB handlerB }

Breaking this down, the first thing you will notice is the definition of two handlers, which are simple Pipeline functions:

let handlerA : Pipeline =
    freya {
        return Next }

let handlerB : Pipeline =
    freya {
        return Next }

Next in the code you will see two simple URI Templates defined. URI Templates can be used to generate URIs given a template and suitable data – Freya also allows to match on URI Templates, extracting the data to then be used. There are some caveats to matching URI Templates, but in general it is a good fit for many applications.

Two URI Templates are defined which will match the paths shown. The syntax for a match in this case is likely familiar – a simple match, capturing the braced terms (e.g. {id}).

let routeA : UriTemplate =
    UriTemplate.parse "/a/{id}"

let routeB : UriTemplate =
    UriTemplate.parse "/b/{name}"

Finally the router itself with the routes defined. The routes are defined using the route keyword in the computation expression. This takes three arguments:

• A UriTemplateRouteMethod, which may be All – matching any method, or Methods which takes a list of Method values which are allowed. In the example, the first route will match any method, the second only GET or OPTIONS requests.
• A UriTemplate which will be matched against the request path and query.
• A Pipeline which will be called if the method, and the path and query are matched.

let routes =
    freyaRouter {
        route Any routeA handlerA
        route (Methods [ GET; OPTIONS ]) routeB handlerB }

The router will call the Pipeline function of the first matched route. If no route matches, no pipeline will be called.

Type Inference¶

Freya 3.0 introduced a more extensive use of statically resolved type parameters (don’t worry if these are not familiar) to give more concise and flexible APIs. One of the places where this is used is in this computation expression. Rather than only taking a literal UriTemplateRouteMethod as the first parameter, the route function can actually take any value which has a static UriTemplateRouteMethod member. By default, this is defined for a few different types, all of which can be used interchangeably. That means that the folloing are all valid routes:

let routes =
    freyaRouter {
        route Any routeA handlerA // Any
        route (Methods [ GET; POST ]) routeA handlerA // Methods
        route [ GET; POST ] routeA handlerA // Method list, inferred
        route GET routeA handlerA } // Method, inferred

You will see that this potentially makes things clearer and more readable, allowing for simpler expressions of the same concepts. In addition to the Methods, both the template and the handler are also inferred - anything which has UriTemplate and anything which has Pipeline can be used. By default, this means that you can just use strings and they will be statically inferred as templates, and any Freya<_> function can be inferred as a Pipeline. This can mean that a previously more complex configuration can be made much simpler:

let routes1 =
    freyaRouter {
        route (Methods [ GET ]) (UriTemplate.parse "/hello") handlerA }

// is the same as...

let routes2 =
    freyaRouter {
        route GET "/hello" handlerA }

Pipeline¶

In earlier versions of Freya, it was neccessary to call an explicit toPipeline function to use a router as a pipeline. This is no longer needed in 3.0+ – the router implements Pipeline and thus anything which expects to be able to infer a pipeline can accept a router.

URI Templates¶

in this example the URI Templates have been defined separately from the router. This could be done inline, saving space. However, it is often useful for multiple parts of a program to be able to refer to the URI Template as a first class item, so they are commonly defined outside of the router itself.

This becomes especially useful when you wish to return the URI of a resource as part of a response. You can use the same URI Template for routing and generating linking URIs, which prevents the two ever becoming unsynchronised, using the typed approach to prevent a class of error.

Optics¶

As with accessing data from the request or response, accessing data from the route requires the use of a suitable set of optics. These are provided under the Route module. Here’s a function which will return the {id} value from the example:

let readId =
    freya {
        return! Freya.Optic.get (Route.atom_ "id") }

There are several things to note here. The first is that route optics are prisms. You can’t statically be sure that a value will be present (even though intuitively you can know that it will be in certain contexts), so the optics must be prisms. Additionally, route optics are parameterised – as shown, it is passed the name of the value sought, in this case “id”).

Another key point to note is that there are three prisms available (all within the Route module). In this case, Route.atom_ is used, but Route.list_ and Route.keys_ are also available. Briefly, this is due to the nature of data within the URI Template specification. It is possible to render and match more complex data structures with URI Templates (see the URI Template RFC for a sense of how URI Templates can be used in more advanced ways). Simple values will only usually require the use of the Route.atom_ optic, but much more is possible – see the relevant recipes for more information.

Summary¶

Techniques for accessing matched values using optics have been shown.

open Freya.Routers.Uri.Template

// Optic for extracting string values from a matched route
Route.atom_ : string -> Prism<State, string>

// Optic for extracting string list values from a matched route
Route.list_ : string -> Prism<State, string list>

// Optic for extracting string pair values from a matched route
Route.keys_ : string -> Prism<State, (string * string) list>

Recipes¶

See also:

• Routing – as well as the library reference, a growing collection of routing recipes covering various techniques is maintained.

Syntax¶

The first thing to note is that as with the Freya URI Template Router, the configuration of the HTTP machine is done using a moderately declarative computation expression syntax. This allows for configuration to be readable while also taking advantage of some features of the F# type system to allow for concision where possible.

To create a simple HTTP machine, which models and HTTP resource, you can use the computation expression, freyaHttpMachine – also aliased as freyaMachine for convenience:

open Freya.Machine.Http

let resource =
    freyaMachine {
       handleOk handler }

Here you can see a very simple resource with almost minimal configuration.

The computation expression makes extensive use of custom operations, giving a declarative syntax which allows for a very clean description of the functionality of the machine as defined by configuration.

Terminology¶

In the topic on Machines, the application of the general machine model to specific problems, in this case HTTP was discussed, stating that general machine terminology is sometimes overridden for specific problem domains. The HTTP machine is one such example.

Next¶

To understand how the HTTP machine works, it is useful to be able to view the design of the decision tree which has been modelled, and which the configuration provided using the computation expression will configure. The next section on the HTTP Model gives information on the model, followed by a further section on individual Configuration specifications.

Diagrams¶

Clickable diagrams are available (these are generated from the Omnigraffle design documents for the HTTP machine and extensions, maintained as part of the Freya Machines repository):

• Freya HTTP Machine Reference Diagrams.

Visualisation¶

In the Overview, the terminology of Decisions and Handlers was defined, and these are visualised in the clickable diagram of the HTTP model. The composition elements are informative in terms of grouping and structure, but the decisions and handlers are the key elements of the model. The naming of these elements is identical to the configuration syntax that may be used in the computation expression, allowing the diagrams to be used as a direct reference along with the detailed reference on each configuration option.