strict bits of datatypes

[apfelmus at quantentunnel.de]

Jón Fairbairn wrote:
> apfelmus at quantentunnel.de writes:
> 
>> Besides, having
>>
>>   let q = FinCons 3 q in q
>>
>> not being _|_ crucially depends on memoization. 
> 
> Does it?

Sorry for having introduced an extra paragraph, I meant that q =/= _|_
under the new WHNF-rule would depend on memoization. At the memory
location of q, hereby marked with *q, evaluation would yield

  *q: q
 =>
  *q: FinCons 3 q

Now, this can be considered "ok" according to the rule because the data
at the location is WHNF and the second argument of FinsCons is WHNF as
well because we just evaluated q to WHNF.

By introducing an extra parameter, the memoization is gone and
evaluation will yield

  q ()
 =>
  FinCons 3 (q ())

The point is that the second argument to FinCons is not WHNF, so we have
to evaluate that further in order to generate only values that conform
to the new WHNF-rule. Of course, this evaluation will diverge now.

With the above, I want to show that the proposed new WHNF-rule gives
non-_|_ values in very special cases only. I don't think that these are
worth it.


Regards,
apfelmus

PS: Your derivations are fine in the case of a non-strict FinCons. But
the point is to make in strict.