strict bits of datatypes

[Jón Fairbairn]

apfelmus at quantentunnel.de writes:

> Besides, having
> 
>   let q = FinCons 3 q in q
> 
> not being _|_ crucially depends on memoization. 

Does it? Mentally I translate that as 

   let q = Y (\q -> FinCons 3 q) in q

=>
   Y (\q-> FinCons 3 q)
=>
   (\q -> FinCons 3 q) (Y (\q-> FinCons 3 q))
=>
   FinCons 3 (Y (\q -> FinCons 3 q))

which, assuming a plausible lambda expression for FinCons,
is a soluble term.

> Even with the characterization by WHNF,
> 
>   let q x = FinCons 3 (q x) in q ()
> 
> is _|_.

Again 

   q = Y(\q x -> FinCons 3 (q x))

so q ()
=> Y(\q x -> FinCons 3 (q x)) ()
=> (\q x -> FinCons 3 (q x))(Y(\q x -> FinCons 3 (q x))) ()
=> (\x -> FinCons 3 (Y(\q y-> FinCons 3 (q y)) x)) ()
=> FinCons 3 (Y(\q x -> FinCons 3 (q x)) () )

which is in WHNF (and soluble too)

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk