|
@@ -0,0 +1,132 @@
|
|
|
+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)
|
|
|
+
|
|
|
+apply : (a |->| b) * a -> |<b>|
|
|
|
+
|
|
|
+suspend : (a -> |<b>|) -> (a |->| b)
|
|
|
+
|
|
|
+ignore : |<b>| -> (a |->| b)
|
|
|
+
|
|
|
+nop : |<'nop'>|
|
|
|
+
|
|
|
+id : a |->| a
|
|
|
+
|
|
|
+
|
|
|
+return(x) = task(fun() -> x end)
|
|
|
+apply(func(f), x) = task(f, x)
|
|
|
+suspend(fun(X) -> return(f(x)) end) = func(f)
|
|
|
+ignore(x) = suspend(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, func(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) * |< [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'+{'ok', a}) -> |<a>|
|
|
|
+
|
|
|
+loopback terminates when the operation returns 'stop'.
|