Bayle Shanks's website: proj-oot-old-150618-ootLazy

oot lazy design questions:

do we need full laziness, like in Haskell, or is a core library focus on lazy sequences, like in Clojure, sufficient?
is there a place for codata 'streams' vs data 'processes' as interfaces as described in http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/#comments ?

safe autostrictification, eager, lazy, lazyrec:

1) you can declare functions as 'lazyrec', meaning that you don't want autostrictification within them 2) when calling functions, you can call them thru the functor 'lazyrec', which is like declaring them 'lazyrec' just for that call 3) you can declare values as 'lazy', meaning that you don't want autostrictification applied to them or their heirs 4) you can declare values as 'eager', meaning that you want strictification applied to them and their heirs

during compile time:

1) infer substructural recursion. Mark such functions as 'only yields infinite data if given infinite data'. (this covers 'sum') 2) infer functions will only recur on some of their arguments, and mark them as 'always yields finite data' and 'only yields infinite data if given infinite data' in the other arguments (this covers 'take') 3) transitively dataflow trace eager data through functions that 'only yields infinite data if given infinite data', to mark their outputs as eager when only eager data is provided 4) transitively dataflow trace lazy data through functions that are not 'always yields finite data', to mark their outputs as lazy when lazy data is provided 5) the transitive dataflow traces of eager and lazy end when you get above the lexical scope of the original eager/lazy declaration. for these purposes a declaration inside the arguments passed to a function are their own lexical scope. e.g. in 'y = f (eager x) w', y is not eager. 6) if any value is marked both 'eager' and 'lazy' then raise a compile-time error

and then during runtime:

1) upon exiting a function or calling into a function, for those outputs or parameter values that are marked eager, strictify 2) upon exiting a function, check to see if we are stuck in a mutual recursion loop that has not produced any lazy output in an entire pass. If so, then unless either (a) the data is marked 'lazy', or (b) the function at the top of the loop is marked 'lazyrec', strictify.

mb we need to allow the programmer to mark sections of code (like the atomic marker and the transaction marker) to which stream fusions should be applied?

or can the compiler discover this automatically?

it seems that the key thing w/r/t foldl, foldr, and stack overflows, is for the compiler to recognize a function or functions which recursively call into themselves (possibly without strictification) in a way that may cause a stack overflow if they are fed an input list longer than a certain length. in this case, either (a) the compiler can add strictification or convert almost-tail-recursive code to tail recursive, (b) the user has marked this operation as "dangerous", or (c) there is a compile-time error.

but forcing the user to explicitly mark this as 'dangerous' seems inconsistent with my decision that side-effectful functions need not be marked as such (although pure functions can be marked as such). why should this be any different? related, i am forcing the programmer to explicitly mark references in data structures.

perhaps, if an opportunity for stream fusion is detected, this can just overrule the detection of a strictification opportunity? or can there exist situations where stream fusion would be possible but this coexists with a foldl-ish danger that would be nullified by a conversion to foldl'?

data could have a dynamic __shouldStrictify function, dynamizing the 'strict data flag' idea

so i guess there are 3 possible types of assurances on function termination:

(1) if all of the inputs are finite, then the output is finite (this sort of assurance is provided by structural recursion proofs) (2) if all of the inputs are finite, then the output may be infinite, but a request for just the head will terminate (this sort of assurance is provided by guarded recursion proofs) (3) (no assurance on termination) if all of the inputs are finite, then the output may be infinite, and even a request for just the head may not terminate

---

unify laziness and promises

---

ok current proposal:

oot is a non-strict language, whose evaluation strategy is somewhere between eager and lazy.

The language guarantees:

non-strict semantics; evaluation of an expression will terminate even if some of its subexpressions diverge, as long as those subexpressions are not needed in a call-by-need reduction
an expression can be annotated "lazy" or "strict" or "strictr" (strict recursive). Upon expanding an expression annotated 'lazy', it will be suspended in a thunk unless it is immediately needed. Upon expanding an expression annotated 'strict', its head will be expanded. Upon expanding an expression annotated 'strictr', it will be recursively reduced as much as it can be.
for any particular program, there is some finite bound on the depth of any explicitly represented nested chain of thunks (which are all consecutively not marked 'lazy'), provided that one or more thunks in that chain can be reduced to a non-thunk without creating another thunk. This bound may be different for different programs.
for any particular program, there is some finite bound on the number of thunks that are not required by call-by-need semantics, yet will be expanded in any one evaluation step before starting any other work, not counting thunks marked 'strict' or thunks below a thunk marked 'recursive strictify (strictr)'. For these purposes, evaluating 'undefined' is treated as if it were evaluating an infinite number of thunks. This bound may be different for different programs.

Note that the last two guarantees promise that:

unless things are annotated 'lazy', the language won't let things like 'foldl sum [0..999999]' create a ridiculously long chain of evaluatable-but-unevaluated chunks
unless things are annotated 'strict' or unless the program would diverge under non-strict semantics, the language won't try to strictify an infinite data structure

There is also an annotation meaning "guaranteed safe to evaluate lazily", meaning that the compiler (or someone else) promises that evaluating this head lazily won't break the required guarantees, and another annotation "guaranteed safe to evaluate strictly". These can be used when the compiler, or programmer, wants to express that it has statically concluded that lazy or strict (or both) evaluation would definitely be allowed, however it wants to leave it up to a later pass, or to an interpreter or runtime, to choose for the purposes of efficiency which evaluation strategy to actually use.

There are no guarantees whether or not various expressions may be speculatively executed concurrently with the mainline evaluation. For example, some implementations may wish to speculatively execute every expression in parallel.

When there is impure (non-referentially-transparent) code pretending to be pure, it can be annotated to indicate whether or not it is okay to speculatively execute it (and what the rollback procedure is for any side-effects). If not, then it won't be executed until it is needed. For example, exceptions will not be thrown in speculative execution (unless the implementation supports speculatively throwing them); however, random number usage may or may not be marked to speculative execute.

---

actually maybe do weaken the language guarantees to include the stuff about cycles in the dynamic control flow graph; the idea of having a fixed cutoff is an implementation detail which is just an easy way to meet this weakened criteria

---