|
|
Dynamics are a new experimental feature of Clean. The concept is easy to understand, but the implementation is not so straightforward (see Vervoort and Plasmeijer, 2002). So, it will take some time before all bits and pieces are implemented and the system will work flawlessly. Please be patient.
What can you do with "Dynamics"? With "Dynamics" it is possible to store and exchange a Clean expression between (different) Clean applications in an easy and type-safe way. The expression may contain (unevaluated!) data and (unevaluated!) function applications. Here are some examples of its use.
Almost all applications store and fetch information to and from
disk (settings and the like). Traditionally, information written to file
first has to be converted by the programmer to some (String) format. When the file is read
in again a parser has to be constructed to parse the input and to convert the String back to the
appropriate data structure. With Dynamics one can store and retrieve (almost) any Clean data structure in a
type-safe way with just one (!) function call. Not only
data can be saved, but also code (unevaluated functions, higher order
functions), which is part of the data structure being stored. Dynamics make it
easier to write a persistent application: an application that stores the
settings in such a way that the next time the user will see everything in the
same way as the last time the application was used.
Different independently programmed Clean
applications, even applications distributed across a network, can easily
communicate arbitrary expressions that can contain data as well as code
(unevaluated functions) in a type-safe way. Dynamics can be communicated via
files or via message passing primitives offered by the Clean libraries. The fact that Clean applications can
communicate code means that a running Clean
application can be extended with additional functionality. So, plug-ins
and mobile code can be realized very easily and everything is
type-safe.
To make all this possible we need some special facilities in the Clean language. But, in the Clean run-time system special support is needed as well. This includes dynamic type checking, dynamic type unification, dynamic encoding and decoding of arbitrary Clean expressions and types, dynamic linking, garbage collection of dynamics objects on disk, and just-in-time code generation.
In Clean 2.0 we have added a dynamic type system such that Clean now offers a hybrid type system with both static as well as dynamic typing. An object (expression) of static type can be packed into an object of dynamic type (a “Dynamic”) and backwards. The type of a Dynamic can only be checked at run-time. An application can also check whether types of several Dynamics can be unified with each other, without a need to know what types are exactly stored into a Dynamic. In this way Clean applications can be used as control language to manage processes and plug-ins (see Van Weelden and Plasmeijer, 2002).
In this Chapter we first explain how a Dynamic can be constructed (see 8.1). In Section 8.2 we explain how the type of a Dynamic can be inspected via a pattern match, and how one can ensure that Dynamics fit together by using run-time type unification.
We explain in Section 8.3 how dynamics can be used to realize type safe communication of expressions between independently executing applications. In Section 8.4 we explain the basic architecture of the Clean run-time system that makes this all possible. Semantic restrictions and restrictions of the current implementation are summarized in Section 8.5.
8.1 Packing Expressions into a Dynamic
Since Clean is a strongly typed language (see Chapter 5), every expression in Clean has a static type determined at compile time. The Clean compiler is in general able to infer the static type of any expression or any function.
Example of Clean expressions and their static type:
3::Int
map::(a -> b) [a] -> [b]
map ((+) 1)::[Int] ->[Int]
MoveColorPoint Green::(Real,Real) -> ColorPoint
By using the keyword dynamic one can (in principle) change any expression of static type :: t into a dynamically typed object of static type ::Dynamic. Such a "dynamic" is an object (a record to be precise) that contains the original expression as well as an encoding of the original static type of the expression. Both the expression as well as the encoding of its static type, are packed into a dynamic. At run-time, the contents of a dynamic (the value of the expression as well the encoded type) can be inspected via a dynamic pattern match (see 8.2).
|
DynamicExpression |
= |
dynamic GraphExpr [:: Type] |
Example showing how one can pack an expression into a Dynamic. Optionally, the static type of the expression one wants to pack into a Dynamic can be specified.
dynamic 3
dynamic 3::Int
dynamic map::A.a b:(a->b) [a] -> [b]
dynamic map::(Int -> Real) [Int] -> [Real]
dynamic map ((+) 1)
dynamic MoveColorPoint Green
Example of a (constant) function creating a dynamic containing an expression of type Tree Int.
:: Tree a = Node a (Tree a) (Tree a) | Leaf
MyTree::Dynamic
MyTree = dynamic (DoubleTree 1 mytree)
where
Doubletree rootvalue tree = Node rootvalue tree tree
mytree = (Node 2 (Node 3 Leaf Leaf) Leaf)
Only the compiler is able to combine an expression with its type into a dynamic, such that it is guaranteed that the encoded type is indeed the type of the corresponding packed expression. However, as usual it is allowed to specify a more specific type than the one the compiler would infer. The compiler will check the correctness of such a (restricted) type specification. Polymorphic types can be stored as well.
If an expression of polymorphic type is packed into a dynamic one
needs to explicitly specify the universal quantifiers as well (see the example
above).
In principle (there are a few exceptions), any algebraic data type can be packed into a dynamic, including basic types, function types, user defined types, polymorphic types, record types, all types of arrays, all types of lists, and existentially quantified types. The system can deal with synonym types as well. Restrictions hold for packing abstract data types, uniqueness types and overloaded functions, see the sub-sections below.
The static type of the object created with the keyword "dynamic" is the predefined type Dynamic. Since all objects created in this way are of type Dynamic, the compiler is in general not able anymore to determine the static type hidden in the Dynamic and it cannot check its type consistency anymore. The type stored into a Dynamic has to be checked at run-time (see 8.2 and 8.3).
8.1.1 Packing Abstract Data Types
Certain types simply cannot be packed into a Dynamic for fundamental reasons. Examples are objects of abstract predefined type that have a special meaning in the real world, such as objects of type World and of type File. It is not sound to pack objects of these types into a Dynamic, because their real world counterpart cannot be packed and stored.
Abstract data types that have a meaning in the real world (such as World, File) cannot be
packed into Dynamic.
A compile time error message will be given in those cases were the compiler refuses to pack an expression into a Dynamic.
In the current implementation there are additional restrictions on the kind of types that can be packed into a Dynamic. Currently it is not possible to pack any abstract data type into a dynamic at all. The reason is that the test on equality of abstract types is not easy: it does not seem to be enough to test the equality of the definitions of the types involved. We should also test whether the operations defined on these abstract data types are exactly the same. The most straightforward way to do this would be to require that abstract data types are coming from the same module (repository).
Expressions containing objects of abstract data type cannot be
packed into a Dynamic. We are working on this. Check the latest version of the Clean system.
8.1.2 Packing Overloaded Functions
Not yet implemented: Overloaded functions can also be packed into a Dynamic. In that case the corresponding type classes (see 6.1) are packed as additional dictionary argument of the function into the Dynamic. When the Dynamic is unpacked in a pattern match, the same type classes have to be defined in the receiving function, otherwise the pattern match will fail (see 8.2.2).
Example: storing an overloaded function into a Dynamic.
OverloadedDynamic:: Dynamic
OverloadedDynamic = dynamic plus :: A.a:a a -> a | + a
where
plus:: a a -> a | + a
plus x y = x + y
Currently, when an overloaded function is packed into a dynamic, one
explicitly has to specify the type, including the forall quantifier and the
class context.
8.1.3 Packing Expressions of Unique Type
Not yet implemented: Expressions of unique type (see Chapter 9) can also be packed into a Dynamic. However, the run-time system cannot deal with uniqueness type variables or with coercion statements (attribute variable inequalities). One can only use the type attribute "*". Furthermore, one has to explicitly define the desired unicity in the type of the expression to be packed into a Dynamic. Otherwise the unicity properties of the packed expression will not be stored. As usual, the compiler will check whether the specified type (including the uniqueness type attributes) of the packed expression is correct.
Example: packing a function into a Dynamic that can write a character to a unique file.
MyDynamic:: Dynamic
MyDynamic = dynamic fwritec :: Char *File -> *File
Uniqueness type variables and coercion statements cannot be part of
a type packed into a Dynamic.
Uniqueness type attributes are only taken into account if they are
explicitly specified in the type of the packed dynamic.
Counter Example: Dynamics cannot deal with uniqueness type variables or with attribute variable inequalities.
MyDynamic:: Dynamic
MyDynamic = dynamic append :: [.a] u:[.a] -> v:[.a] , [u<=v]
8.1.4 Packing Arguments of Unknown Type
The compiler is not in all cases capable to infer the concrete type to be assigned to a Dynamic. For instance, when a polymorphic function is defined it is in general unknown what the type of the actual argument will be. If it is polymorphic, it can be of any type.
An argument of polymorphic type cannot be packed into a Dynamic.
Counter Example of a function creating a Dynamic. Arguments of polymorphic type cannot be packed into a Dynamic.
WrongCreateDynamic:: t -> Dynamic
WrongCreateDynamic any = dynamic any
If one wants to define a function that can wrap an arbitrary argument into a Dynamic, not only the value, but also the concrete static type of that argument has to be passed to the function. For efficiency reasons, we of course do not want to pass the types of all arguments to all functions. Therefore, we have to know which of the arguments might be packed into a Dynamic. A special class context restriction is used to express this. So, instead of a polymorphic function one has to define an overloaded function (see Chapter 6). The class TC (for Type Code) is predefined and an instance of this class is required whenever an argument of unknown type is packed into a dynamic. The compiler will automatically generate an appropriate instance of the TC when needed.
Example of an overloaded function that can wrap an argument of arbitrary type into a Dynamic.
CreateDynamic:: t -> Dynamic | TC t
CreateDynamic any = dynamic any
MyTree:: Dynamic
MyTree = CreateDynamic (Node 2 (Node 3 Leaf Leaf) Leaf)
8.1.5 Using Dynamic Typing to Defeat the Static Type System
Dynamic typing can also be used to do things the static type system would forbid. For instance, lists require that all lists elements are of the same type. Since all dynamic expressions are of type Dynamic, one can combine objects of static different type into a list by turning them into a Dynamic.
Example: three ways to pack objects of different type into a list. The first method is to define a new type in which all types one likes to pack into a list are summarized with an appropriate constructor to distinguish them. For unpacking one can make a case distinction on the different constructors in a pattern match. Everything is nice statically typed but one can only pack and unpack the types that are mentioned in the wrapper type.
:: WrapperType = I Int | R Real | C Char
MyWrapperList = [I 1, R 3.14, C 'a']
The next way to pack objects of different types is by defining a list structure using an existential type (see 5.1.3). Any type can be packed now but the disadvantage is that there is no simple way to distinguish the elements and unpack them once they are packed.
:: ExstList = E.a: Cons a ExstList | Nil
MyExstList = Cons 1 (Cons 3.14 (Cons 'a' Nil)
The third way is to wrap the values into a Dynamic. Any type can be packed and via a pattern match one can unwrap them as well. It is very inefficient though and one can only unwrap a value by explicitly naming the type in the pattern match (see 8.2).
MyDynamicList = [dynamic 1, dynamic 3.14, dynamic 'a']
It is possible to write Clean programs in which all arguments are dynamically typed. You can do it, but it is not a good thing to do: programs with dynamics are less reliable (run-time type errors might occur) and much more inefficient. Dynamics should be used for the purpose they are designed for: type-safe storage, retrieval, and communication of arbitrary expressions between (independent) applications.
8.2 Unpacking Dynamics Using a Dynamic Pattern Match
When a Dynamic is created (see above), its static type is the type Dynamic. The compiler is in general not able anymore to determine what the original type was of the expression that is packed into a Dynamic. The only way to figure that out is at run-time (that why it is called a Dynamic), by inspecting the dynamic via a pattern match (see 3.2) or a case construct (see 3.4.2). With a pattern match on a Dynamic one cannot only inspect the value of the expression that was packed into a Dynamic, but also its original type. So, with Dynamics run-time type checking and dynamic type unification is possible in Clean with all the advantages (more expressions can be typed) and disadvantages (type checking may fail at run-time) of a dynamic type system. The programmer has to take care of handling the case in which the pattern match fails due to a non-matching dynamic type.
|
DynamicPattern |
= |
(GraphPattern :: DynamicType) |
|
DynamicType |
| |
{ DynPatternType}+ |
|
DynPatternType |
= |
Type |
|
|
| |
TypePatternVariable |
|
|
| |
OverloadedTypePatternVariable |
|
TypePatternVariable |
= |
Variable |
|
OverloadedTypeVariable |
= |
Variable^ |
Any expression that can be packed into a dynamic can also be unpacked using a dynamic pattern match. With a pattern match on Dynamics a case distinction can be made on the contents of the Dynamic. If the actual Dynamic matches the type and the value specified in the pattern, the corresponding function alternative is chosen. Since it is known in that case that the Dynamic matches the specified type, this knowledge is used by the static type system: dynamics of known type can be handled as ordinary expressions in the body of the function. In this way dynamics can be converted back to ordinary statically typed expressions again. The static type checker will use the knowledge to check the type consistency in the body of the corresponding function alternative.
Example: Use of a dynamic pattern match to check whether a Dynamic is of a specific predefined type. The first alternative of the function transform matches if the Dynamic contains the Integer of value 0. The second alternative is chosen if the Dynamic contains any Integer (other than 0). The third alternative demands a function from [Int] to [Int]. The next alternative is chosen if the Dynamic is a pair of two [Int]. If none of the alternatives match, the last alternative is chosen. The program will yield an empty list in that case.
transform :: Dynamic -> [Int]
transform (0 :: Int) = []
transform (n :: Int) = [n]
transform (f :: [Int]->[Int]) = f [1..100]
transform ((x,y) :: ([Int],[Int])) = x ++ y
transform other = []
Warning: when defining a pattern match on Dynamics, one should always be aware that the pattern match might fail. So, we advise you to always include an alternative that can handle non-matching dynamics. The application will otherwise abort with an error message that none of the function alternatives matched.
Example: use of a dynamic pattern match to check whether a Dynamic is of a specific user defined algebraic data type. If the Dynamic contains a Tree of Int, the function CountDynamicLeafs will count the number of leafs in this tree. Otherwise CountDynamicLeafs will return 0.
:: Tree a = Node a (Tree a) (Tree a) | Leaf
CountDynamicLeafs :: Dynamic -> Int
CountDynamicLeafs (tree :: Tree Int) = countleafs tree
CountDynamicLeafs other = 0
where
countleafs :: (Tree Int) -> Int
countleafs tree = count tree 0
where
count:: (Tree a) Int -> Int
count Leaf nleafs = nleafs + 1
count (Node left right) nleafs = count left (count right nleafs)
MyTree :: Dynamic
MyTree = dynamic (Node 1 (Node 2 (Node 3 Leaf Leaf) Leaf) (Node 4 Leaf Leaf))
Start :: Int
Start = CountDynamicLeafs MyTree
Example: use of a dynamic pattern match to check whether a Dynamic is a polymorphic function (the identity function in this case).
TestId :: Dynamic a -> a
TestId (id :: A.b: b -> b) x = id x
TestId else x = x
To avoid confusion with type pattern variables (see 8.2.4 and 8.2.5), polymorphic type variables have to be explicitly introduced with
the forall quantifier (A.).
Quantifiers are only allowed on the outermost level (Rank 1).
Dynamics can be created by functions in other modules or even come from other (totally different) Clean applications (see 8.3). It is therefore possible that in a Dynamic a type with a certain name is stored, yet this type might have a type definition which is (slightly or totally) different from the type known in the matching function. So, the context in which a dynamic is packed might be totally different from the context in which the dynamic is unpacked via a pattern match. Hence, it is not enough that matching type constructors have identical names; they should also have exactly the same type definition. If not, the match will fail.
Two types are considered to be equal if and only if all the type definitions (type constructors, data constructors, class definitions) are syntactically identical modulo the names of type variables (alpha conversion is allowed). Type equivalence of type constructors is automatically checked by the Clean run-time system, even if these types are defined in totally different Clean applications. To make this possible, we had to change the architecture of the Clean run-time system (see 8.4).
So, when a pattern match on a dynamic takes place, the following things are checked in the indicated order (case constructs are handled in a similar way):
1) All the type constructors (either of basic type, predefined or user defined) specified in a dynamic pattern will be compared with the name of the corresponding actual type constructors stored in the dynamics. If corresponding type constructors have different names, the pattern match fails and the next alternative is tried.
2) If in the pattern match, corresponding type’s constructors have the same name, the run-time system will check whether their type definitions (their type might have been defined in different Clean applications or different Clean modules) are the same as well. The system knows where to find these type definitions (see 8.3 and 8.4). If the definitions are not the same, the types are considered to be different. The pattern match fails and the next alternative is tried.
3) If the types are the same, the actual data constructors (constant values) are compared with the data constructors specified in the patterns, as usual in a standard pattern match (see 3.2) without dynamics. If all the specified constants match the actual values, the match is successful and the corresponding function alternative is chosen. Otherwise, the pattern match fails and the next alternative is tried.
In the current implementation there are additional restrictions on the kind of types that can be packed into a Dynamic and therefore also be unpacked from a Dynamic (see 8.2.1, 8.2.2, and 8.2.3).
In a dynamic pattern match one can explicitly specify to match on a certain type constructors (e.g. Tree Int). One can also use a type pattern variable (see 8.2.4) to specify a type scheme with which the actual type has to be unified. By using overloaded variables (see 8.2.5) defined in the type of the function, the static context in which a function is used can have influence on the kind of dynamic that is accepted. So, there are two special types of variables that can occur in a type pattern: type pattern variables and overloaded type pattern variables.
8.2.1 Unpacking Abstract Data Types
It is not yet possible to pack or unpack an abstract data type. We
are working on this. Check the latest version of the Clean
system. See also 8.1.1.
8.2.2 Unpacking of Overloaded Functions
Not yet implemented: One can specify a class restriction in the type in a dynamic pattern match. The system will check whether the actual dynamic contains a function that is indeed overloaded with exactly the same class context restriction as specified in the pattern. Two class definitions are regarded to be equal if all involved class definitions are syntactically equal, modulo alpha conversion of the type variables.
One is obligated for overloaded type variables to introduce them via
the forall quantifier in the pattern, to avoid confusion with type pattern
variables (see 8.2.4 and 8.2.5).
Quantifiers are only allowed on the outermost level.
Example: Unpacking of an overloaded function. The pattern match will only be successful if the dynamic contains a function overloaded in +. The corresponding class definitions will be checked: the definition of the class + has to be the same as the class + known in the context where the dynamic has been created. Due to the application of plus 2 3, the type checker will require an instance for + on integer values.
CheckDynamic:: Dynamic -> Int
CheckDynamic (plus :: A.a : a a -> a | + a) = plus 2 3
CheckDynamic else = 0
8.2.3 Unpacking Expressions of Unique Type
Not yet implemented: Expressions of unique type (see Chapter 9) can also be unpacked via a dynamic pattern match. However, the run-time system cannot deal with uniqueness type variables or with coercion statements (attribute variable inequalities). One can only use the type attribute "*". The match will only be successful if the specified types match and all type attributes also match. No coercion from unique to non-unique or the other way around will take place.
Example: Unpacking a function that can write a character to a unique file.
WriteCharDynamic:: Dynamic Char *File -> *File
WriteCharDynamic (fwc :: Char *File -> *File) char myfile = fwc char myfile
WriteCharDynamic else char myfile = myfile
Uniqueness type variables and coercion statements cannot be used in
a dynamic pattern match.
The
type attributes of the formal argument and the actual argument have to be
exactly the same. No coercion from unique to non-unique or the other way around
will take place.
8.2.4 Checking and Unifying Types Schemes using Type Pattern Variables
In an ordinary pattern match one can use data constructors (to test whether an argument is of a specific value) and variables (which match on any concrete value in the domain). Similarly, in a pattern match on a dynamic type one can use type constructors (to test whether a dynamic contains an expression of a specific type) and type pattern variables (which match on any type). However, there are differences between ordinary variables and type pattern variables as well. All ordinary variable symbols introduced at the left-hand side of a function definition must have different names (see 3.2). But, the same type variable symbol can be used several times in the left-hand side (and, of course, also in the right-hand side) of a function definition. Type pattern variables have the function alternative as scope and can appear in a pattern as well as in the right-hand side of a function in the context of a dynamic type.
|
TypePatternVariable |
= |
Variable |
Each time the same type variable is used in the left-hand side, the pattern matching mechanism will try to unify the type variable with the concrete type stored in the dynamic. If the same type variable is used several times on the left hand-side, the most general unifier is determined that matches on all corresponding types in the dynamics. If no general unifier can be found, the match will fail. As usual, of all corresponding type constructors it will be checked whether they are indeed the same: the corresponding type definitions have to be equivalent (see 8.2). Type equivalence of matching type constructors is automatically checked by the Clean run-time system, even if these types are defined in different Clean applications.
Type pattern variables are very handy. They can be used to check for certain type schemes or to check the internal type consistency between different Dynamics, while the checking function does not exactly has to know which concrete types are actually stored in a dynamic. One can make use of type pattern variables to manage and control plug-ins in a flexible way (see 8.3).
The function dynApply has two arguments of type Dynamic and yields a value of type Dynamic as well. The first Dynamic has to contain a function unifiable with type (a -> b), the second argument has to be unifiable with the argument type a the function is expecting. In this way we can ensure that it is type technically safe to apply the function to the argument, without exactly knowing what the actual types are. The result will have the statically unknown type b, but, by packing this result into a Dynamic again, the static type system is happy: it is a Dynamic. If the dynamics types cannot be unified, it is not type safe to apply the function to the argument, and the next alternative of dynApply is chosen. It yields an error message stored into a dynamic.
dynApply :: Dynamic Dynamic -> Dynamic
dynApply (f :: a -> b) (x :: a) = dynamic (f x :: b)
dynApply df dx = dynamic ("cannot apply ",df," to ",dx)
Start = dynApply (dynamic (map ((+) 1)) (dynamic [1..10])
Type pattern variables behave similar as existentially quantified type variables (see 5.1.3). It is statically impossible to determine what the actual type of a type pattern variable is. So, in the static type system one cannot define an expression which type is depending on the value of a type pattern variable. The static type system cannot deal with it, since it does no know its value. However, an expression which type is depending on the type assigned to a type pattern variable can be packed into a dynamic again, because this is done at run-time. See the dynAppy example above.
It is not allowed to create an expression which static type is
depending on the value of a type pattern variable.
Counter Example: It is not possible to let a static type depend on the value of a type pattern variable. The actual value of the type b in WrongDynApply is unknown at run-time. This example will result into a type error. See 8.2.5 for a legal variant of this function.
WrongDynApply :: Dynamic Dynamic -> ???
WrongDynApply (f :: a -> b) (x :: a) = f x
WrongDynApply df dx = abort "cannot perform the dyanmic application"
Start = WrongDynApply (dynamic (map ((+) 1)) (dynamic [1..10]) ++ [11..99]
Note: don't confuse type pattern variables with the other variables that can appear in a dynamic type to indicate polymorphic or overloaded functions or constructors. The latter are introduced via a quantifier in the type. See also 8.2.5.
8.2.5 Checking and Unifying Unknown Types using Overloaded Type Variables
In a dynamic pattern match one can explicitly state what type of a Dynamic is demanded. But it is also possible to let the static context in which a function is used impose restrictions on the Dynamic to be accepted. This can be realized by using overloaded type variables in a dynamic pattern. Such an overloaded type variable has to be introduced in the type of the function itself and the variable should have the predefined type class TC (see 8.1.1) as context restriction. This makes it possible to let the overloading mechanism determine what the demanded type of a Dynamic has to be (the "type dependent functions" as introduced by Marco Pil, 1999). By using such an overloaded type variable in a dynamic pattern, the type assigned by the static overloading mechanism to this variable is used as specification of the required type in the dynamic pattern match. The carrot symbol (^) is used as suffix of a type pattern variable in a dynamic pattern match to indicate that an overloaded type variable is used, instead of a type pattern variable. Overloaded type variables have the whole function definition as scope, including the type of the function itself.
|
OverloadedTypeVariable |
= |
Variable^ |
An overloaded type pattern variable has to be introduced in the type
definition of the function.
The predefined type class TC (see 8.1.1) has to be specified as context restriction on the global type
pattern variable.
As is usual with overloading (see 6.6), in some cases the compiler is not able to resolve overloading,
e.g. due to internally ambiguously overloading.
Example: The function Start appends [11..99] to the result of FlexDynApply. So, it is clear that FlexDynApply will have to deliver a [Int] to the function Start. The additional context restriction TC b turns FlexDynApply into an overloaded function in b. The function FlexDynApply will not deliver some dynamic type b, but the static type b that is demanded by the context applying FlexDynApply. The overloading mechanism will automatically pass as additional parameter information about the static type b that is required by the context. This type is then used to check the actual type of the dynamic in the dynamic pattern match
FlexDynApply :: Dynamic Dynamic -> b | TC b
FlexDynApply (f :: a -> b^) (x :: a) = f x
FlexDynApply df dx = abort "cannot perform the dyanmic application"
Start = FlexDynApply (dynamic (map ((+) 1)) (dynamic [1..10]) ++ [11..99]
Example: The function lookup will look up a value of a certain type a in its lists of Dynamics. The type it will search for depends on the context in which the function lookup is used. In Start the lookup function is used twice. In the first case an integer value is demanded (due to + 5), in the second case a real value (due to + 2.5) is required. The program will be aborted if a value of the required type cannot be found in the list.
lookup :: [Dynamic] -> a | TC a
lookup [(x :: a^):xs] = x
lookup [x:xs] = lookup xs
lookup [] = abort ”dynamic type error”
Start = (lookup DynamicList + 5, lookup DynamicList + 2.5) // result will be (6,5.64)
DynamicList = [dynamic 1, dynamic 3.14, dynamic 'a']
Note: don't confuse overloaded type variables with type pattern variables or the other variables that can appear in a dynamic type to indicate polymorphic or overloaded functions or constructors. The latter are introduced via a quantifier in the type.
Example: the following artificial example the kinds of type variables that can be used in a dynamic pattern are shown. In the first alternative a type variable a is used (introduced by the forall quantifier). This alternative only matches on a polymorphic function. In the second alternative an overloaded type variable is used (indicated by a^) referring to the overloaded type variable a | TC a introduced in the function body. It will match on a function of the same type as the actual type of the second argument of AllSortsOfVariables. The last alternative uses type pattern variables a and b. It matches on any function type, although this function is not used.
AllSortsOfVariables :: Dynamic a -> a | TC a
AllSortsOfVariables (id::A.a : (a -> a)) x = id x
AllSortsOfVariables (f::a^ -> a^) x = f x
AllSortsOfVariables (f::a -> b) x = x
8.3 Type Safe Communication using Dynamics
As explained in the introduction of this Chapter, the most important practical use of Dynamics is enabling type safe communication of data and code between different (distributed) Clean applications. When a Dynamic is stored or communicated it will be encoded (serialized) to a string. So, in principle almost any communication media can be used to communicate Dynamics. In this section we only explain how to store and retrieve a Dynamic from a File. It is also possible to communicate a Dynamic directly via a channel or via send / receive communication primitives. The actual possibilities are depending on the facilities offered by Clean libraries. This is outside the scope of this Clean language report.
If a Clean application stores a Dynamic into a File any other (totally different) Clean application can read the Dynamic from it. Since a Dynamic can contain data as well as code (unevaluated function applications), this means that any part of one Clean program can be plugged into another. Since Clean is using compiled code, this has a high impact on the run-time system (see 8.4).
One can read and write a Dynamic with just one function call. In the Clean library StdDynamic the functions readDynamic and writeDynamic are predefined. As usual in Clean, uniqueness typing is used for performing I/O (see 9.1). When a Dynamic is written, the whole expression (the graph expression and its static type) is encoded symbolically to a String and stored on disk. When a Dynamic is read, it is read in lazily. Only when the evaluation of the Dynamic is demanded (which can only happen after a successful pattern match), the String is decoded back to a Dynamic. If new function definitions have to be plugged in, this will be done automatically (see 8.4). This lazy reading is also done for Dynamics stored into a Dynamic. So, a Dynamic can only be plugged in if its type is approved in a Dynamic pattern match.
Standard functions for reading and writing of a Dynamic.
definition module StdDynamic
...
writeDynamic :: Dynamic String *World -> *(Bool,*World)
readDynamic :: String *World -> *(Bool, Dynamic, *World)
The use of Dynamics is shown in the examples below. Each example is a complete Clean application.
Example of a Clean application writing a Dynamic containing a value of type Tree Int to a File named DynTreeValue. This example shows that data can be stored to disk using the Clean function writeDynamic.
module TreeValue
import StdDynamic, StdEnv
:: Tree a = Node a (Tree a) (Tree a) | Leaf
Start world
# (ok,world) = writeDynamic "DynTreeValue" MyTree world
| not ok = abort "could not write MyTree to file named DynTreeValue"
| otherwise = world
where
MyTree::Dynamic
MyTree = dynamic (Node 1 mytree mytree)
where
mytree = (Node 2 (Node 3 Leaf Leaf) Leaf)
Example of another Clean application writing a Dynamic containing the function countleafs to a File named CountsLeafsinTrees. This function can count the numbers of leafs in a Tree and is of type (Tree Int) -> Int. This examples shows that code (in this case the function CountLeafs) can be stored on disk as well, just using WriteDynamic.
module CountLeafs
import StdDynamic, StdEnv
:: Tree a = Node a (Tree a) (Tree a) | Leaf
Start world
# (ok,world) = writeDynamic "CountsLeafsinTrees" CountLeafs world
| not ok = abort "could not write dynamic"
| otherwise = world
where
CountLeafs = dynamic countleafs
countleafs:: (Tree Int) -> Int
countleafs tree = count tree 0
where
count:: (Tree a) Int -> Int
count Leaf nleafs = nleafs + 1
count (Node left right) nleafs = count left (count right nleafs)
count else = abort "count does not match"
The third Clean application reads in the file TreeValue containing a Tree Int and the function countleafs (a plugin) that can counts the number of Leafs in a Tree. So, new functionality is added to the running application Apply. By using the function dynapply the new plugged in function countleafs is applied to the tree that has been read in as well. The application Apply itself has a function to count the number of nodes and applies this function on the tree read in.
Note that this application will only work if all the type Trees defined in the different applications are exactly the same (module the names for the type variables used).
module Apply
import StdDynamic, StdEnv
:: Tree a = Node a (Tree a) (Tree a) | Leaf
Start world
# (ok,countleafs,world) = read "CountsLeafsinTrees" world
| not ok = abort ("could not read CountsLeafsinTrees")
# (ok,treevalue,world) = read "TreeValue" world
| not ok = abort ("could not read TreeValue")
| otherwise = ( countnodes (case treevalue of (v::(Tree Int))= v) 0
, dynapply countleafs treevalue
)
where
dynapply :: Dynamic Dynamic -> Dynamic
dynapply (f::a -> b) (v::a) = dynamic (f v)
dynapply df dv = dynamic "incorrectly typed dynamic application"
countnodes Leaf nnodes = nnodes
countnodes (Node left right) nnodes = countnodes left (countnodes right (nnodes+1))
8.4 Architecture of the implementation
From the examples above we learn that a Dynamic stored on disk can contain data as well as code (unevaluated functions and function applications). How is this information stored into a file and how is a running Clean application extended with new data and new functionality? To understand this one has to know a little bit more about how a Clean application is generated.
Implementation of Dynamics
Clean applications are not interpreted via an interpreter. Executables are generated using compiled machine code. Storing a Dynamic into disk and retrieving it again from disk cannot simply be done by (re) interpretation of Clean source code.
 |
The Clean compiler (written in Clean) compiles Clean implementation modules (.icl and .dcl files) to machine independent abc-code (.abc files). The Clean definition modules are used to check the type consistency between the separately programmed Clean modules. The abc-code contains machine instructions for a virtual abstract machine, the abc-machine (see Plasmeijer and van van Eekelen, 1993). The abc-code is a kind of platform independent byte code specially designed for Clean. The Code Generator (the one and only application in the Clean system which is written in C) translates the abc-code into platform dependent symbolic machine code (.obj files under Windows). The code generator can generate code for different platforms such as for Intel (Windows, Linux), Motorola (Mac) and Sparc (Unix) processors. The Static Linker (written in Clean) links all the object modules of one Clean program together into a click able executable application (.exe file under Windows). The compilation scheme described above can be used even if Dynamics are internally used in an application. But, as soon as Dynamics are communicated to File or communicated to another program, a different run-time support is needed and the traditional compilation scheme is changed to prepare this.
 |
In the changed compilation scheme, the static linker not only generates an application (actually, currently it is a .bat file), but it also generates two additional files. One is called the code repository (.lib file). All object codes of your application are collected here. The other file (.typ file) is a repository that contains all type definitions. The repositories serve as a database which is accessed by the Dynamic Linker. Whenever an (other) running application needs code for a plug in or a type that has to be checked, the Dynamic Linker will look it up in the appropriate repository. Each time a Clean program is recompiled, new repositories are created. Repositories should not be removed by hand because it might make the Dynamics stored on disk unreadable. A special garbage collector is provided that can remove unused repositories.
When a Clean application doing dynamic I/O is started, a special linker (the Dynamic Linker, written in Clean) is started with it as well (if it is not already running). The Dynamic Linker is a server application on the computer. It will serve all running Clean programs that read or write Dynamics. The Dynamic Linker will construct the application or plug-in at run-time in the same way as the Static Linker would do at compile-time for a conventional Clean program. There is no efficiency penalty once the code is linked in.
When a Dynamic is written to disk using the function writeDynamic, two (!) files are created: a .dyn file and a .sysdyn file. The .sysdyn file contains the actual information: a String encoding of the dynamic. This sysdyn file is used by the Dynamic Linker and should not be touched by the user because it might make the Dynamics stored on disk unreadable. The special garbage collector provided will also remove unused .sysdyn files.
The user may only touch and use the .dyn file that contains references to the actual dynamic stored in the .sysdyn file. The .dyn file can be seen as a "typed" file. It can be handled like any other user file. It can be renamed, moved or deleted without any danger.
When a Dynamic is written to a file, an encoding of the graph and its type are written to disk. The graph is encoded in such a way that sharing will be maintained when the graph is read in again. The stored graph may contain unevaluated functions. In a Dynamic on disk, functions are represented by symbolic pointers to the corresponding code repositories. The types stored in a Dynamic on disk point to the corresponding type definitions stored in the type repositories.
No plug-in will be plugged in unless its type is approved. When a Dynamic stored on disk is read in by an (other) application, first only a pointer to the stored Dynamic is used in the Clean program. To use a Dynamic in an application one first has to examine it in a pattern match. In the pattern match the type of the Dynamic is unified with a specified type or with the type of another Dynamics. If the run-time type unification is successful, the Dynamic Linker will check whether all type definitions of the types involved are identical as well. This type information is fetched from the corresponding type repository when needed. If the types are identical and the conventional pattern match succeeds as well, the corresponding function body can be evaluated. Only when the evaluation of the stored Dynamic is demanded, the graph encoded in the Dynamic on disk is reconstructed as far as needed (Dynamics nested in a Dynamic are reconstructed lazily). The Dynamic Linker links in the code corresponding to the unevaluated functions stored in the Dynamic. It is fetched from the code repository and plugged in the running (!) application. In some cases the Dynamic Linker will ask the Code Generator to generate new code (just-in-time code generation) to construct the required image. The Dynamic Linker has to ensure that identical data types defined in different applications are linked in such a way that they are indeed considered to be of the same type at run-time.
8.5 Semantic Restrictions on Dynamics
Dynamics are an experimental feature of Clean 2.0. In the current version there are still many restrictions and limitations.
The following types cannot be packed/unpacked: abstract data types,
uniqueness types, overloaded types. We are working on it.