On Jan 25, 2007, at 6:57 AM, Yitzchak Gale wrote:
Scott Turner wrote:
Paul B. Levy's studies of "call-by-push-value" model strictness/ laziness using a category theoretic approach.
That sounds interesting. Do you have a reference for that?
http://www.cs.bham.ac.uk/~pbl/papers/ The first sentence of the paper "Call-by-push-value: Deomposing Call- By-Value and Call-By-Name" reads: Let us consider typed call-by-value (CBV) and typed call-by-name (CBN), and observe convergence at ground type only. (This restriction does not matter in CBV, but in CBN, it makes the η-law for functions into an observational equivalence.) That sounds a lot like it explicitly excludes a polymorphic "seq". However, I'm not very familiar with this work, so I don't know if that is a critical restriction, or merely incidental to the presentation of this paper.
Thanks, Yitz
Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG