For my own edification (experts: please remark if I stray from any conventional notions--be as picky as possible) and perhaps for anyone who didn't quite grok Ross Paterson's punchline, I'm going to try to answer the question "How does seq affect the definedness CPO?"
At the heart of these two recursive definitions q = 3 : q (1) r = r `seq` (3 : r) (2) we find these two functions f and g f x = 3 : x g x = x `seq` (3 : x) such that q = lfp f r = lfp g This is the least fixed point approach to recursive definitions. (From Scott and Strachey? I'm not sure of the origins...) In the CPO of definedness, x < y means that "x is less-defined than y". Since _|_ is "undefined": forall x . _|_ <= x. For a more meaty case, consider l1 = Cons 3 Nil l2 = Cons 3 _|_ l2 > l1 because l1 is more defined. If values don't share the same structure, (a tree and a list for instance) I don't think their comparison is meaningful (experts?). The intuition behind the lfp as a definition principle is that of refinement/approximation. When constructing a value for the recursively definition, we begin with _|_ which represents no information. Finding the lfp of function means that we apply the function as many times as is necessary to define the value. Each application of the function refines the value a bit more until we have the sufficient approximation of the full value. What constitutes "sufficient" is determined by how the value is used: consider ((head . tail) q) versus (length q). Intuitively q = lfp f = f(f(f(f(f(f .... (f(f(f _|_)))...))))) (*) r = lfg g = g(g(g(g(g(g .... (g(g(g _|_)))...))))) (**) q is infinite 3s because f is non-strict. Operationaly, when f is applied to the thunk representing the final q value, it contributes the (3:) constructor to the definition of q, making q more defined. Note that it does not need to force the evaluation of q in order to make this contribution. Thus, the intuitive (f _|_) of (*) is never evaluated. r is _|_ because g is strict. When g is applied to the thunk representing the final q value, it forces its evaluation which operationaly leads us to g again being applied to the final q value thunk without making any contribution to the definition. Thus, the intuitive (g _|_) of (**) is always evaluated. Since g is strict, g _|_ = _|_ and this reduction trickles all the way out until r = _|_. As Robert Dockins showed, any recursive definition of a Fin value unfolds to an equation like (2) because of the strictness annotation in the datatype. We just discussed that the lfp semantics of an equation of (2)'s form will always result in _|_. On the other hand, any finite definition of a Fin value works fine. So ihope's Fin data type is either a finite list or _|_, as was purposed. Was that all square? Dotted i's and such? Nick On 10/11/06, Ross Paterson <[EMAIL PROTECTED]> wrote:
On Wed, Oct 11, 2006 at 11:04:49AM -0400, Robert Dockins wrote: > let q = seq q (FinCons 3 q) in q (beta) > > We have (from section 6.2): > seq _|_ y = _|_ > seq x y = y iff x /= _|_ > > Now, here we have an interesting dilemma. The meaning of a recursive definition is the least fixed point of the equation, in this case _|_. Same as let x = x in x. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
