Last modified: Thu Oct 19, 2001

Data Field Haskell Extensions

Data Field Haskell extends Haskell with the following classes, data types, functions, and constructs. They are provided by the Datafield and Pord modules, additions to the Show and Eval classes, and some constructs which are added directly to the language. The descriptions here are informal and the list is not complete. A full account is given in Jonas Holmerin's masters thesis. There is also detailed online documentation of the extensions: the Datafield and Pord modules, and the other extensions.

Warning: this text was originally written for the Haskell 1.3 version of the language and has not been scanned for updates to the Haskell 98 version. Minor details may thus be obsolete.

Classes and Data Types

• Pord a: a class which provides a pointwise partial ordering on tuples (as opposed to the lexicographical total ordering provided by Ord). This class is a mere technicality which makes it possible to define meet on dense bounds in a generic way.
• Datafield a b: data type for data fields with index type a and value type b.
• Bounds a: data type for bounds over index type a.

Basic Operations on Data Fields

• datafield :: (Pord a,Ix a) => (a -> b) -> Bounds a -> Datafield a b: builds data fields from functions and bounds.
• (!) :: Datafield a b -> a -> b: data field application (indexing). Hyperstrict in the index.
• bounds :: (Pord a,Ix a) :: Datafield a b -> Bounds a: extracts the bound of a data field.

Construction of Bounds

• (<:>) :: (Ix a, Pord a) => a -> a -> Bounds a: creates a dense bound over a. (Finite)
• sparse :: (Pord a, Ix a) => [a] -> Bounds a: creates a sparse bound over a from a list. (Finite)
• predicate :: (Ix a, Pord a) => (a -> Bool) -> Bounds a: creates a predicate bound over a. (Infinite)
• universe :: (Ix a, Pord a) -> Bounds a: represents the universal set. (Infinite)
• empty :: (Ix a, Pord a) -> Bounds a: represents the empty set.
(Finite)
• (<*>) :: (Pord a, Ix a, Pord b, Ix b) => Bounds a -> Bounds b -> Bounds (a,b): creates a two-dimensional product bound over (a,b) from a bound over a and a bound over b. (Finite iff both a and b are finite.)
  (There are also functions prod_n which create n-dimensional product bounds.)

Here are some illustrations of bounds: dense and sparse one-dimensional bounds,

and two-dimensional bounds: some product bounds, and a sparse bound.

Operations on Bounds

• join :: (Pord a, Ix a) => Bounds a -> Bounds a -> Bounds a: computes the "union" of two bounds.
• meet :: (Pord a, Ix a) => Bounds a -> Bounds a -> Bounds a: computes the "intersection" of two bounds.
• (<\>) :: (Pord a, Ix a) => Datafield a b -> Bounds a -> Datafield a b: explicit restriction of a data field with a bound.
• finite :: (Pord a, Ix a) => Bounds a -> Bool: test for finiteness of bounds
• enumerate :: (Pord a, Ix a) => Bounds a -> [a]: list of the elements in the set defined by a finite bound, ordered by the "<" operation in the Ord class.
• size :: (Pord a, Ix a) => Bounds a -> Int: the number of elements in the set defined by a finite bound
• inBounds :: (Pord a, Ix a) => a -> Bounds a -> Bool: test of membership in the set defined by a bound.

The tables below give the result "type" of join and meet as a function of the argument "types". E = empty, U = universe, S = sparse, D = dense, P = predicate, x = product bound. "S/P" in the table for join means that the result is sparse if the product bound is finite, and a predicate otherwise.

meet	E	U	S	D	P	x
E	E	E	E	E	E	E
U		U	S	D	P	x
S			S	S	S	S
D				D	S	x
P					P	P
x						x

join	E	U	S	D	P	x
E	E	U	S	D	P	x
U		U	U	U	U	U
S			S	S	P	S/P
D				D	P	x
P					P	P
x						x

Here are some illustrations of meet: between dense and sparse one-dimensional bounds,

and two-dimensional bounds: between product bounds, and between a product and a sparse bound.

Note how meet on product bounds is applied elementwise. join works in the following way: for one-dimensional bounds,

and some two-dimensional bounds.

Again, note how also join on product bounds is applied elementwise. Furthermore note that join on dense bounds may yield an overapproximation of the union on the corresponding sets.

Operations on Finite Data Fields

• hstrictTab :: (Pord a, Ix a, Eval a) => Datafield a b -> Datafield a b: a data field evaluator which evaluates all elements in a finite data field in a hyperstrict fashion. (There are also data field evaluators tab, which creates a data structure holding the unevaluated elements of the data field, and strictTab which in addition evaluates each element to whnf.)
• foldlDf :: (Pord a, Ix a, Eval a) => (b -> c -> b) -> b -> (Datafield a c) -> b: the data field equivalent to foldl for lists. As for lists, there are a number of different data field folds.

Miscellaneous

• isoutofBounds :: a: a polymorphic error value representing the result of the application of a data field to an index falling out of bounds. In contrast to ordinary Haskell error values, the return of this value does not abort the computation. This value could be defined as Nothing in the Maybe-monad: however, its semantics as an error value is completely predefined, which makes it possible to hide its handling and build it into the implementation.

Forall-abstraction

The syntax of forall-abstraction is precisely analogous to the syntax of lambda-abstraction. Its most general form involves pattern-matching on its arguments:

forall apat₁ ... apat_n -> exp

which can be resolved into a simpler, equivalent form, just as for lambda-abstraction. See here for details. Of particular importance is pattern-matching over simple tuples:

forall ( x₁, ...,x_n ) -> exp

which can be used to define multidimensional data fields. As for lambda-abstraction, this is distinct from

forall x₁ ... x_n -> exp

which defines a nested data field. All forall-expressions can be translated into a forall-expression with the outermost abstraction being over a single variable. The semantics for such an expression forall x -> e is

datafield (\x -> e) B(e,{x},Ø)

where B(e,{x},Ø) is a bound which is derived from the body e of the forall-expression. B(e,{x},Ø) is defined in such a way that the set it defines contains the domain of \x -> e. For a precise definition of the semantics of forall-abstraction, see here. For a more informal description of the semantics, which gives some more intuition, see here.

For-abstraction

For-abstraction provides a syntax to define a data field by cases over different parts of its domain. It is thus more explicit than forall-abstraction. The syntax is

for pat in { e₁ -> e₁' ; ... ; e_n -> e_n' }

Here, the expressions e_i are bounds and each e_i' defines the value of the data field within the set defined by e_i. The bound of the data field is enclosed in the union (join) of the different e_i (it can possibly be further restricted by the different e_i'). If bounds overlap, then the leftmost e_i' has precedence within the area of overlap. For a precise definition of the semantics of for-abstraction, see here.