[Haskell-cafe] IO is not a monad
lennart at augustsson.net
Mon Feb 12 18:29:25 EST 2007
No, I can't say off hand if seq-hnf would keep eta valid, either.
Neither do I know how to implement seq-hnf efficiently. :)
As far as eta for other types, yes, I'll take it if I can get it's
But I'm also pretty happy with encoding all the other data types within
the lambda calculus (which was how Haskell behaved before seq).
On Feb 12, 2007, at 22:05 , Claus Reinke wrote:
>> Adding seq ruins eta reduction. For normal order lambda calculus
>> we have '\x.f x = f' (x not free in f). If we add seq this is no
>> longer true.
> isn't that a problem of seq (and evaluation in Haskell generally)
> not being strict enough (ie, forcing evaluation only to weak head
> normal form rather than to head normal form)?
> for instance:
> seq (\x->_|_ x) () = () =/= _|_ = seq _|_ ()
> but (assuming a variant, seq-hnf, forcing to hnf instead):
> seq-hnf (\x-> _|_ x ) () = _|_ = seq-hnf _|_ ()
> I don't have my "phone book" here, but didn't Barendregt have a
> of what kind of normal form would be an appropriate choice for the
> of lambda terms, with hnf being "good" and whnf or nf being "bad"?
> to whnf is a pragmatic choice, with a long history, and its own
> calculus, which is not quite the ordinary lambda calculus.
> but it's been ages since I learned these things, so I might be
>> I'm a fan of eta, it makes reasoning easier. It also means
>> the compiler can do more transformations.
> I also like eta conversion, as well as its variations for non-
> function types. what they have in common is that the expanded form
> provides syntactic/structural evidence for properties that are only
> semantically present in the reduced form. for instance, if we add
> non-functions to the calculus, eta has to be
> constrained with type information for f - as the expanded form
> promises that we have a function, holding more information than the
> reduced form.
> variations of eta for non-function types, this allows us to make
> contexts less strict (the kind of "borrowing information from the
> future" so often needed in cyclic programming, or in dealing with
> other potentially infinite structures):
> lazy_id_pair x = (fst x,snd x) -- lazy_id_pair _|_ = (_|_,_|_)
> strict_id_pair (a,b) = (a,b) -- strict_id_pair _|_ = _|_
> at the expense of not having laws like:
> x = (fst x,snd x) -- not true in general, even if we know
> that x::(a,b)
> x = x >>= return -- not true in general, even if x :: Monad m
> => m a
> x = \y-> x y -- not true in general, even if x :: a -> b
> we still have the inequalities, though - the expanded form being more
> defined than the reduced form.
> x :: t ]= (expand-at-t x) :: t -- eta conversion at type t
> so compilers could use eta-expansion, but not eta-reduction (not
> an approximate analysis of an undecidable property). do you happen
> to have an example in mind where eta-reduction would be beneficial
> as a compiler transformation, but analysis (to demonstrate that the
> expanded functional expression terminates successfully) impractical?
More information about the Haskell-Cafe