Type functile is just a type synonym for functions from tile to tile. Yet, Functile d iv v1 v2 inherits from the inverse structure of its codomain and its extension to Num and Fractional.

A tile function is a duration preserving tile function when

durationT t == durationT (f t)

Maps every tile function to a duration preserving tile function.

forceDurP f t = re [f t] + delayT t

in such a way that

re[forceDurP f t] == re[f t]

A stronger notion: a tile function is a delay preserving tile function when

f (delayT t) == delayT (f t)

Maps every tile function to a delay preserving tile function.

forceDelayP f t = re [f t] + delayT t

in such a way that

(t /= delayT t) implies re[forceDelayP f t] == re[f t]

Clearly, we also have

isDelayPreserving t => isDurationPreserving t

The empty tile type is terminal and weak initial restricting to duration preserving functions with function delayT as arrow from and to the empty tile type.

Restricting further to delay preserving functions makes EmptyTile d iv truely initial (delayT is the unique arrow from EmptyTile d iv into Tile d iv).

For all f :: Tile d iv v -> Tile d iv Void

isDurationPreserving f implies f t == delayT t

and for all f :: Tile d iv Void -> Tile d iv v

isDelayPreserving f implies f t == delayT t

Our adhoc encoding of the empty type

Applies a tile of functions over tiles to a tile. This function is delay preserving in its second arguement:

delayT (applyT tf t) == delayT t

Lifts a function over tiles into a tile of function of tile, in such a way that

f t == applyT (fromFuncT f) t

Warning : for this, we truly need a greatest element (aka top) in the lattice d

Evaluates the categorical product of a tile of functions and an argument tile. Argument tile is cut according to the duration of functions to be applied.

Currifies a function of tiles (duration/delay preservation properties yet to be checked)

Uncurrifies a function of tiles (duration/delay preservation properties yet to be checked)

Swaps left and right types in a biproduct type

Canonical left projection

Canonical right projection

Canonical left injection

Canonical right injection

With combination properties

id==fromLeftT . toLeftT and id == fromRightT . toRightT

delayT==fromLeftT . toRightT and delayT == fromRightT . toLeftT

Factorizes tile functions through product, that is, for all duration preserving functions, the following properties are satisfied:

fromLeftT (factorProductT f1 f2 t) ==  f1 t

fromRightT (factorProductT f1 f2 t) ==  f2 t

In other words, provided unicity of such a factorization, Tile d iv (Either v1 v2) is the categorical product of Tile d iv v1 and Tile d iv v1.

Factorizes tile functions through sum, that is, for all delay preserving functions, the following properties are satisfied:

factorSumT f1 f2 (toLeftT t) ==  f1 t

factorSumT f1 f2 (toRightT t) ==  f2 t

In other words, provided unicity of such a factorization, Tile d iv (Either v1 v2) is the categorical sum of Tile d iv v1 and Tile d iv v1

Mixes two tiles almost without loss of information.

Demixes a mixed tile without loss of information. The property

muxT . demuxT t == t

holds for every tile t of Tile d iv (Either v1 v2), and the property

demuxT . muxT (t1,t2) == (t1,t2)

holds whenever |duration t1 == duration t2|.

Applies in a list of functions over the same arguement and return the parallel merge of their results. This parallel product of functions is defined by:

parFT [] t = delayT t
parFT (f:fs) t = re [f t] + parFT fs t

Remark : with zero object and finite products and sums that coincides, the category of delay preserving tile functions is a 'semiadditive category'. The binary version of the parallel composition is the induced abelian monoid product inside homsets.

Derived binary parallel product defined by

f1 |+| f2 = parFT [f1,f2]

Properties of the binary parallel product:

• Neutral element:

f |+| delayT == forceDurP f, delayT |+| f  == forceDurP f

• Associativity:

f1 |+| (f2 |+| f3) == (f1 |+| f2) |+| f3

• Commutativity:

f1 |+| f2 == f2 |+| f1

• Idempotence

(f |+| f) == f

• Distributivity

(f1 |+| f2) . g == (f1 . g) |+| (f2 . g)

The following property would hold in an additive category...

g . (f1 |+| f2) /= (g . f1) |+| (g . f2) for some g

Applies in a list of functions over the same arguement and return the sequential merge of their results. This sequential product is defined by:

seqFT [] t = delayT t
seqFT (f:fs) t = re[f t + seqFT fs t] + delayT t

Derived binary sequential composition defined by

f1 |*| f2 = seqFT [f1,f2]

Properties of the binary sequential product:

yet to be discovered....

Records slices of the input tile of some duration and replay them applying some function parameter.

recordAndReplay d f t
   = let recordD = takeD d t
     in recordD + re [f recordD] + recT (recordAndReplayD d) f (dropD d t)

This is a typical example of a pull reactive function where the clock structure of the output is governed by itself.