tcalculus-1.0.0: A DSL prototype for structured realtime/reactive functional programing

Copyright(c) David Janin, 2016
Licensesee the LICENSE file in the distribution
Maintainerjanin@labri.fr
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell2010

Tile.Functile

Contents

Description

Functions from tiles to tiles inherit from the rich algebraic structure of tiles. Then, defining delay preserving functions, we eventually get a monoidal cartesian closed category that is also a (weak) semiadditive category, with parallel product of functions as abelian, linear product in homsets (see Tile.TCategories for the various instances within Control.Category).

Synopsis

Functions over tiles and two subclasses

type Functile d iv v1 v2 = Tile d iv v1 -> Tile d iv v2 Source #

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.

Duration preserving functions

isDurationPreserving :: (Eq d, Num d, Lattice d, POrd v2) => Functile d iv v1 v2 -> Tile d iv v1 -> Bool Source #

A tile function is a duration preserving tile function when

durationT t == durationT (f t)

forceDurP :: (Eq d, Num d, POrd v1, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 Source #

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]

Delay preserving functions

isDelayPreserving :: (Eq d, Num d, Lattice d, POrd v2) => Functile d iv v1 v2 -> Tile d iv v1 -> Bool Source #

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

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

forceDelayP :: (Eq d, Num d, POrd v1, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 Source #

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

Terminal and (weak) initial objects

type EmptyTile d iv = Tile d iv Void Source #

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

data Void Source #

Our adhoc encoding of the empty type

Exponentiation

applyT :: (Num d, Eq d, Lattice d) => Tile d iv (Functile d iv v1 v2) -> Tile d iv v1 -> Tile d iv v2 Source #

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

fromFuncT :: (Num d, Eq d, Lattice d) => Functile d iv v1 v2 -> Tile d iv (Functile d iv v1 v2) Source #

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

Monoidal properties

evalT :: (Num d, Eq d, Lattice d) => Tile d iv (Either (Functile d iv v1 v2) v1) -> Tile d iv v2 Source #

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.

curryT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v3 -> Functile d iv v1 (Functile d iv v2 v3) Source #

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

uncurryT :: (Num d, Eq d, Lattice d) => Functile d iv v1 (Functile d iv v2 v3) -> Functile d iv (Either v1 v2) v3 Source #

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

swapT :: (Eq d, Num d, Lattice d) => Tile d iv (Either v1 v2) -> Tile d iv (Either v2 v1) Source #

Swaps left and right types in a biproduct type

Categorical sum and product

Left and right projections

fromLeftT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v1 Source #

Canonical left projection

fromRightT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v2 Source #

Canonical right projection

Left and right injections

toLeftT :: (Num d, Eq d, Lattice d) => Functile d iv v1 (Either v1 v2) Source #

Canonical left injection

toRightT :: (Num d, Eq d, Lattice d) => Functile d iv v2 (Either v1 v2) Source #

Canonical right injection

With combination properties

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

Factorization through product

factorProductT :: (Eq d, Num d, Lattice d) => Functile d iv v v1 -> Functile d iv v v2 -> Functile d iv v (Either v1 v2) Source #

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.

Factorization through sum (not unique)

factorSumT :: (Eq d, Num d, Lattice d) => Functile d iv v1 v -> Functile d iv v2 v -> Functile d iv (Either v1 v2) v Source #

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

More on the resulting weak semiadditive category

Routing primitives

muxT :: (Eq d, Num d, Lattice d) => (Tile d iv v1, Tile d iv v2) -> Tile d iv (Either v1 v2) Source #

Mixes two tiles almost without loss of information.

demuxT :: (Eq d, Num d, Lattice d) => Tile d iv (Either v1 v2) -> (Tile d iv v1, Tile d iv v2) Source #

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|.

Parallel application of tile functions

parFT :: (Eq d, Num d, Lattice d) => [Functile d iv v1 v2] -> Functile d iv v1 v2 Source #

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.

(|+|) :: (Eq d, Num d, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 infixl 9 Source #

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

Sequential application of tile functions

seqFT :: (Eq d, Num d, Lattice d) => [Functile d iv v1 v2] -> Functile d iv v1 v2 Source #

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

(|*|) :: (Eq d, Num d, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 infixl 8 Source #

Derived binary sequential composition defined by

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

Properties of the binary sequential product:

yet to be discovered....

Function examples

recordAndReplayD :: (Eq d, Num d, Lattice d) => d -> Functile d iv v v -> Functile d iv v v Source #

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.

Orphan instances

(Eq d, Fractional d, Lattice d) => Fractional (Functile d iv v1 v2) Source # 

Methods

(/) :: Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 #

recip :: Functile d iv v1 v2 -> Functile d iv v1 v2 #

fromRational :: Rational -> Functile d iv v1 v2 #

(Eq d, Num d, Lattice d) => Num (Functile d iv v1 v2) Source # 

Methods

(+) :: Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 #

(-) :: Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 #

(*) :: Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2 #

negate :: Functile d iv v1 v2 -> Functile d iv v1 v2 #

abs :: Functile d iv v1 v2 -> Functile d iv v1 v2 #

signum :: Functile d iv v1 v2 -> Functile d iv v1 v2 #

fromInteger :: Integer -> Functile d iv v1 v2 #