alloy-1.2.0: Generic programming library

Safe HaskellSafe-Inferred



A slightly experimental add-on for Alloy involving the idea of routes to a particular part of a tree.



data Route inner outer Source

A Route is a way of navigating to a particular node in a tree structure.

Let's say that you have some binary tree structure:

 data BinTree a = Leaf a | Branch (BinTree a) (BinTree a)

Suppose you then have a big binary tree of integers, potentially with duplicate values, and you want to be able to modify a particular integer. You can't modify in-place, because this is a functional language. So you instead want to be able to apply a modify function to the whole tree that really just modifies the particular integer, deep within the tree.

To do this you can use a route:

 myRoute :: Route Int (BinTree Int)

You apply it as follows (for example, to increment the integer):

 routeModify myRoute (+1) myTree

This will only work if the route is valid on the given tree.

The usual way that you get routes is via the traversal functions in the module.

Another useful aspect is composition. If your tree was in a tree of trees:

 routeToInnerTree :: Route (BinTree Int) (BinTree (BinTree Int))

You could compose this with the earlier route:

 routeToInnerTree @-> myRoute :: Route Int (BinTree (BinTree Int))

These routes are a little like zippers, but rather than building a new data type to contain the zipped version and the re-use aspect, this is just a simple add-on to apply a modification function in a particular part of the tree. Multiple routes can be used to modify the same tree, which is also useful.

Routes support Eq, Show and Ord. All these instances represent a route as a list of integers: a route-map. [0,2,1] means first child (zero-based), then third child, then second child of the given data-type. Routes are ordered using the standard list ordering (lexicographic) over this representation.


Eq (Route inner outer) 
Ord (Route inner outer) 
Show (Route inner outer) 

routeModify :: Route inner outer -> (inner -> inner) -> outer -> outerSource

Applies a pure modification function using the given route.

routeModifyM :: Monad m => Route inner outer -> (inner -> m inner) -> outer -> m outerSource

Applies a monadic modification function using the given route.

routeGet :: Route inner outer -> outer -> innerSource

Given a route, gets the value in the large data structure that is pointed to by that route.

routeSet :: Route inner outer -> inner -> outer -> outerSource

Given a route, sets the value in the large data structure that is pointed to by that route.

(@->) :: Route mid outer -> Route inner mid -> Route inner outerSource

Composes two routes together. The outer-to-mid route goes on the left hand side, and the mid-to-inner goes on the right hand side to form an outer-to-inner route.

identityRoute :: Route a aSource

The identity route. This has various obvious properties:

 routeGet identityRoute == id
 routeSet identityRoute == const
 routeModify identityRoute == id
 identityRoute @-> route == route
 route @-> identityRoute == route

routeId :: Route inner outer -> [Int]Source

Gets the integer-list version of a route. See the documentation of Route.

routeList :: Int -> Route a [a]Source

Given an index (zero is the first item), forms a route to that index item in the list. So for example:

 routeModify (routeList 3) (*10) [0,1,2,3,4,5] == [0,1,2,30,4,5]

makeRoute :: [Int] -> (forall m. Monad m => (inner -> m inner) -> outer -> m outer) -> Route inner outerSource

Given the integer list of identifiers and the modification function, forms a Route. It is up to you to make sure that the integer list is valid as described in the documentation of Route, otherwise routes constructed this way and via the Alloy functions may exhibit strange behaviours when compared.

routeDataMap :: Ord k => Int -> Route (k, v) (Map k v)Source

Constructs a Route to the key-value pair at the given index (zero-based) in the ordered map. Routes involving maps are difficult because Map hides its internal representation. This route secretly boxes the Map into a list of pairs and back again when used. The identifiers for map entries (as used in the integer list) are simply the index into the map as passed to this function.

routeDataSet :: Ord k => Int -> Route k (Set k)Source

Constructs a Route to the value at the given index (zero-based) in the ordered set. See the documentation for routeDataMap, which is nearly identical to this function.

class AlloyARoute t o o' whereSource

An extension to AlloyA that adds in Routes. The opsets are now parameterised over both the monad/functor, and the outer-type of the route.


transformMRoute :: Monad m => o m outer -> o' m outer -> (t, Route t outer) -> m tSource

transformARoute :: Applicative f => o f outer -> o' f outer -> (t, Route t outer) -> f tSource

data BaseOpARoute m outer Source

The terminator for opsets with AlloyARoute.



baseOpARoute :: BaseOpARoute m outerSource

Like baseOpA but for AlloyARoute.

data (t :-@ opT) m outer Source

The type that extends an applicative/monadic opset (opT) in the given functor/monad (m) to be applied to the given type (t) with routes to the outer type (outer). This is for use with the AlloyARoute class.


((t, Route t outer) -> m t) :-@ (opT m outer) 

type OneOpARoute t = t :-@ BaseOpARouteSource

A handy synonym for a monadic/applicative opset with only one item, to use with AlloyARoute.

type TwoOpARoute s t = s :-@ (t :-@ BaseOpARoute)Source

A handy synonym for a monadic/applicative opset with only two items, to use with AlloyARoute.