What is Strictness in LCi?

In the proposed calculus LCi, arguments to calls should be constants and strict - when a 'call is made', i.e. it is selected as a redex, arguments should be in NF.

In the proposed Haskell compiler, there are two steps:

1. Compile Haskell terms to lazy LCi terms.
2. Compile lazy LCi terms to eager LCi terms.

The question is: How would you want to guarantee strictness of the arguments of calls?

1. Annotate arguments to calls strict, or assume they should be reduced strictly in the rewrite semantics, in the first step. Have a mixed approach compiler in the second step.
2. Generate terms such that arguments reduce to NF first according to lazy evaluation, then use the simple 'thunkification' method in the second step.

I am not sure the second step is possible. Is it possible to generate terms such that lazy rewriting will force arguments of calls to NF? If not, what if you'ld go pure SKI? Or sidestep to a separate encoding for constants? I guess the 'trick' would be to apply the constant to the function?! If so, 2) is the preferable compilation method.

Some reading to do...

Bored by ridiculously long compile times.