123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175 |
- Types
- -----
- |<a>| = a task that, when run, produces a value of type 'a
- a |->| b = an operation that, when run with a value of type 'a, produces a value
- of type 'b
- a |->| b ~ a -> |<b>|
- 0 |->| a ~ |<a>|
- Primitives
- ----------
- task : (a -> b) * a -> |<b>|
- task : (0 -> a) -> |<a>|
- return : a -> |<a>|
- func : (a -> b) -> (a |->| b)
- app : (a |->| b) * a -> |<b>|
- dynamic : (a -> |<b>|) -> (a |->| b)
- ignore : |<b>| -> (a |->| b)
- nop : |<'nop'>|
- id : a |->| a
- return(x) = task(fun() -> x end)
- app(func(f), x) = task(f, x)
- dynamic(fun(X) -> return(f(x)) end) = func(f)
- ignore(x) = dynamic(fun(_) -> x)
- nop = return('nop')
- id = func(fun(X) -> X)
- cannot construct an element of type 0 |->| a.
- Pipelines
- ---------
- pipe : (a |->| b) * (b |->| c) -> (a |->| c)
- pipe : [ a_1 |->| a_2, a_2 |-> a_3, ..., a_n-1 |->| a_n ] -> (a_1 |->| a_n)
- bind : |<a>| * (a -> |<b>|) -> |<b>|
- feed : |<a>| * (a |->| b) -> |<b>|
- sequence : |<a>| * |<b>| -> |< [a, b] >|
- sequence : [ |<a_1>|, |<a_2>|, ..., |<a_n>| ] -> |< [a_1, a_2, ..., a_n] >|
- pipe(f_1, pipe(f_2, ...f_n...)) = pipe([f_1, f_2, ..., f_n])
- pipe(pipe(f, g), h) = pipe(f, pipe(g, h))
- pipe(id, f) = f
- pipe(f, id) = f
- bind(bind(x, f), g) = bind(x, fun(X) -> bind(f X, g) end)
- bind(x, return) = x
- bind(return(x), f) = f x
- feed(x, dynamic(f)) = bind(x, f)
- Scattering
- ----------
- scatter : |<a>| * |<b>| -> |< [a, b] >|
- scatter : [ |<a_1>|, |<a_2>|, ..., |<a_n>| ] -> |< [a_1, a_2, ..., a_n] >|
- parallel : (a |->| a') * (b |->| b') -> ([a, b] |-> [a', b'])
- parallel : [ a_1 |->| a_1', a_2 |->| a_2', ..., a_n |->| a_n' ]
- -> ([a_1, a_2, ..., a_n] |->| [a_1', a_2', ..., a_n'])
- fanout : (a |->| b) * (a |->| c) -> (a |->| [b, c])
- fanout : [ a |->| b_1, a |->| b_2, ..., a |->| b_n ]
- -> (a |->| [b_1, b_2, ..., b_n])
- pointwise : ([a_1, a_2, ..., a_n] |->| [b_1, b_2, ..., b_n])
- * ([b_1, b_2, ..., b_n] |->| [c_1, c_2, ..., c_n])
- -> ([a_1, a_2, ..., a_n] |->| [c_1, c_2, ..., c_n])
- pointwise : [ [a_11, a_12, ..., a_1n] |->| [a_21, a_22, ..., a_2n],
- [a_21, a_22, ..., a_2n] |->| [a_31, a_32, ..., a_3n],
- ...,
- [a_m-11, a_m-12, ..., a_m-1n] |->| [a_m1, a_m2, ..., a_mn] ]
- -> ([a_11, a_12, ..., a_1n] |->| [a_m1, a_m2, ..., a_mn])
- map : (a |->| b) * |< [a] >| -> |< [b] >|
- reduce : ([a] |->| b) * ([b] |->| b) * |< [a] >| -> |< [c] >|
- Choice
- ------
- tag : t * |<a>| -> |< {t, a} >|
- tagging : t * (a |->| b) -> (a |->| {t, b})
- cases : (a |->| a') * (b |->| b') -> (a+b |->| a'+b')
- cases : [ a_1 |->| b_1, a_2 |->| b_2, ..., a_n |->| b_n ]
- -> (a_1+a_2+...+a_n |->| b_1+b_2+...+b_n)
- cases nondeterministically picks any non-'nop' output, or is 'nop' if there is
- none. use tags to force determinism.
- fanin : (a |->| c) * (b |->| c) -> (a+b |->| c)
- fanin : [ a_1 |->| b, a_2, |->| b, ..., a_n |->| b ]
- -> (a_1+a_2+...+a_n |->| b)
- fanin = cases, since '+' is simple union.
- fastest : |<a>| * |<b>| -> |< a+b >|
- fastest : [ |<a_1>|, |<a_2>|, ..., |<a_n>| ] -> |< a_1+a_2+...+a_n >|
- slowest : |<a>| * |<b>| -> |< a+b >|
- slowest : [ |<a_1>|, |<a_2>|, ..., |<a_n>| ] -> |< a_1+a_2+...+a_n >|
- Loops
- -----
- loopback : (a |->| {'stop', b}+{'loop', a}) -> (a |->| b)
- loopback terminates when the operation returns 'stop'.
- Interpretation
- --------------
- simpl : |<a>| -> |<a>|
- simpl : (a |->| b) -> (a |->| b)
- simpl simplifies and optimizes a task or operation.
- linearize : |<a>| -> (0 -> a)
- linearize : (a |->| b) -> (a -> b)
- linearize interprets a task or operation to run sequentially on a single node.
- localize : |<a>| -> (0 -> a)
- localize : (a |->| b) -> (a -> b)
- localize interprets a task or operation to run in parallel on a single node.
- distribute : |<a>| -> (ResourceInfo -> a)
- distribute : (a |->| b) -> (ResourceInfo * a -> b)
- distribute interprets a task or operation to run in parallel distributed among
- several nodes.
- run_linear : |<a>| -> a
- run_linear : (a |->| b) * a -> b
- run_linear(x) = linearize(x)()
- run_linear(x, y) = linearize(x)(y)
- run_local : |<a>| -> a
- run_local : (a |->| b) * a -> b
- run_local(x) = localize(x)()
- run_local(x, y) = localize(x)(y)
- run : ResourceInfo * |<a>| -> a
- run : ResourceInfo * (a |->| b) * a -> b
- run(Info, x) = distribute(x)(Info)
- run(Info, x, y) = distribute(x)(Info, y)
|