Dynamics are still under heavy development. It is therefore important to note that dynamics are released for experiments only. Please re-read the last sentence.
At least the following restrictions apply:
Algebraic, record and function typed objects without the above mentioned restrictions can be packed and/or unpacked.
The main goal of this text is to provide a basic understanding of dynamics by presenting its design and only a little bit of its implementation. The current implementation limitations and on-going research are also pointed out.
A dynamic (of static type Dynamic) consists of:
Basic operations on dynamics:
In addition there are type dependent functions i.e. the context determines the type of the packed object.
Please see the ‘Examples’-folder for concrete syntax and examples.
In addition to the normal procedure to create a new Clean project:
A dynamic is created using the following syntax:
dynamic <an arbitrarily Clean object> :: <external type>
Eventually most typed Clean objects can be injected into a dynamic. Only for some objects e.g. World, File, … natural restrictions will apply.
The external type of a dynamic is the static type of the object injected into the dynamic. The internal type of a dynamic are the types of all objects which help to create an object of the external type.
An example (Clean fragment):
dynamic (length [‘a’,’b’,’c’]) :: Int
The current implementation need not perform the rather costly internal type check because it is done at compile-time and the use of code repositories preserves the validity of the compile-time check.
After a dynamic project has been compiled and linked without errors, the static linker has created:
Only the batch-file is visible for the user and it replaces the executable that would normally be generated by the linker.
The code and type repositories for the dynamic project have been stored in the ‘libraries’-subfolder of the dynamic linker folder which has been set in the Clean IDE.
There are two ways to start a dynamic project:
The batch-file starts the dynamic linker by giving it the code repository for the dynamic application. The dynamic linker then starts the application at its normal entry point.
Each object in Clean conceptually is a graph rewriting system. The graph at run-time consists of:
In order to encode a dynamic e.g. write it to disk the above components of the run-time graph need to be encoded:
In addition lazy dynamics are supported. A lazy dynamic is referenced at least once from a dynamic other than itself. The need for laziness is motivated by the requirements:
An example illustrating the requirements presented above follows. Suppose two writer applications communicate with a single reader application by a record containing a dynamically typed field for each writer. The writer applications cannot/do not use the field of another writer.
If a writer wants to fill its field in the common data structure, then the data structure must first partially be decoded, the field of the writer must be filled and it finally must be partially encoded again. It is clear that the second requirement is essential here.
The example clearly shows that constructing the entire encoded graph is undesirable and in general impossible. Furthermore the type of a dynamic must always be constructible regardless of the value it describes. Lazy dynamics satisfy these requirements.
Because only parts of a dynamic will be encoded at once and sharing within a dynamic must be preserved, its data graph must be partitioned into small pieces according to some well-chosen condition satisfying the above requirements. These partitions can also be called the unit of laziness.
Currently the unit of laziness i.e. a partition is a set of equally coloured data graph nodes. The value and type component of each dynamic occurring in the data graph is assigned an unique colour. The set of colours associated with each node contains the colour of each component of a dynamic from which it is reachable.
The descriptors referenced by the data graph nodes in a partition are also stored which permits the dynamic linker to selectively load and link code into the running application when a particular partition is required.
As consequence of the lazy encoding of the data graph, a dynamic may still contain references to other dynamics.
The provided encoding-routine implements the above. The ‘dumpDynamic’-tool can be used to create a human readable representation of a dynamic.
The partitions that constitute a dynamic are decoded lazily: only if a partition is needed by evaluation, its data graph is built when it has not already been built before.
The decode-phase is preceded by a read-phase that is medium dependent. Currently the read-phase is not lazy because it is unknown which references to not yet built partitions of a dynamic, are still reachable from the root of entire graph. To implement this, the run-time system has to be extended.
In a more advanced implementation, the programmer should be able to specify a medium specific callback-function that reads a partition from that medium.
It should be noted that the encode-phase is a lot more complicated than the decode-phase both from the design as the implementation perspective.
A dynamic pattern is transformed into the following actions that are performed in the order of enumeration:
Two type constructors are considered equal if their implementations are syntactically exactly the same modulo alpha-conversion. In case of an algebraic data-type the constructor order is insignificant.
The above definition is very rigid because in practice there may exist a conversion translating the offered type by a dynamic to the required type demanded by a pattern match. The notion of conversion-functions is being investigated. The programmer would specify them using generics.
From an operational perspective, the type variables in grouped dynamic patterns e.g. in a single rule alternative permit communication among dynamics regardless of the expression surrounding the dynamic patterns. Type constructor names in dynamic patterns establish a potential connection between a dynamic and its surrounding expression.
For example if a dynamic pattern succeeds which contains a type constructor name and the dynamic matched against it also offers an equally named type constructor and its type definitions are equivalent, then there are two implementations of the same type constructor i.e. one in the surrounding expression of the pattern and one in the dynamic.
But the current Clean implementation assumes a single definition for a type constructor. As a consequence a function from the surrounding expression would not correctly work on objects from the dynamic it matched against and vice versa.
Therefore the dynamics implementation guarantees that if the type component of a dynamic is successfully matched against at least one type pattern, then the surrounding expressions of these type patterns must share a single implementation for each type constructor name contained in these patterns. In other words, a dynamic can be correctly evaluated in another surrounding expression provided its dynamic patterns match.
Currently the following restriction to be lifted apply:
Example (Clean fragment):
:: Tree a = …
apply (f :: a -> b) d_v=:(v :: b)
= case d_v of
(t :: Tree Int)
->
If in the above example, the dynamic pattern of ‘d_v’-dynamic succeeds, then injected object ‘t’ cannot be evaluated within the apply function because the Tree-implementation of dynamics f and v is not yet shared with the implementation used by the apply-function.
Example (Clean fragment):
dynamic (dynamic Empty :: Tree Int) :: Dynamic
If an application evaluates at least one dynamic, then these dynamic are permitted to recursively evaluated other dynamics provided that the required type patterns succeed which gives rise to a tree that relates the evaluation of one dynamic with another.
The top-level node in the tree is the application. All other nodes are dynamic nodes. The children of a particular node, are the nodes decoded by that node. The edge between a parent node and a child node is labelled with the external type of the child node i.e. a dynamic.
The problem here is that the inner dynamic can potentially be unpacked at different nodes as long as it can be propagated upwards in the dynamic tree and all these sites must share a single implementation. Propagation stops when an edge from child to parent does not contain a Dynamic-type.
This problem is still being investigated.
If the unification algorithm encounters two equally named types, then their names are passed to the dynamic linker that performs a type definition check according to the notion of type equivalence discussed earlier. If the type definitions are equivalent, they are entered into their type equivalent class.
When evaluation later triggers the decoding of a partition which requires a type implementation from a certain type equivalent class, an arbitrarily type implementation from that type equivalent class must be linked in when it has not yet been linked in.
At the moment there only two public accessible papers about dynamics. Other papers describing both the design of dynamics and its implementation will probably appear next year.
This paper describes type dependent functions. A type dependent function can be use to enforce the static type context of the function upon a dynamic.
This paper introduces the notion of a dynamic and its two basic operations for the lazy functional programming language Clean.