Lennart Augustsson wrote:
I'm not sure what you're asking. The (untyped) lambda calculus is
Turing complete.
How could seq improve that?
Obviously, it can't. But how can it hurt?
Classical lambda calculus does not model the
semantics of laziness, so seq is equivalent to
flip const there,
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.
I'm not sure why you bring up lazy evaluation (I presume you
mean lazy evaluation as in call-by-need). Having call-by-need
or not is unobservable,
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
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
easily.
But I'm also pretty happy with encoding all the other data types within
the lambda calculus
I'm not sure what you're asking. The (untyped) lambda calculus is
Turing complete.
How could seq improve that?
On Feb 8, 2007, at 11:18 , Yitzchak Gale wrote:
Lennart Augustsson wrote:
I think seq is funny because it is not lambda definable.
Does the set of computable functions on the
Lennart Augustsson wrote:
I think seq is funny because it is not lambda definable.
I wrote:
Does the set of computable functions on the natural
numbers defined by the lambda calculus augmented
with seq have higher Turing degree than the
set of classical computable functions?
I guess I was
Lennart Augustsson wrote:
I think seq is funny because it is not lambda definable.
Does the set of computable functions on the natural
numbers defined by the lambda calculus augmented
with seq have higher Turing degree than the
set of classical computable functions?
-Yitz
Aaron McDaid wrote:
Could seq be changed so that it will not give an error if it finds
undefined? Am I right in thinking that seq is supposed to
theoretically do nothing, but simply give a hint to the compiler so to
speak? If that is true, it should merely attempt to evaluate it, but
ignore
Aaron McDaid wrote:
Apologies for referring to this old thread...
At least for me, this is not old. It is still very
much on my mind.
Simply, 'undefined undefined' is a bit more defined than simply
'undefined'. Just like 'undefined:undefined' is at least a non-empty
list; which can be
Just for the record, I think this completes the
requirements of my challenge. Please comment!
Is this correct?
Thanks.
1. Find a way to model strictness/laziness properties
of Haskell functions in a category in a way that is
reasonably rich.
We use HaskL, the category of Haskell types,
Could seq be changed so that it will not give an error if it finds
undefined? Am I right in thinking that seq is supposed to
theoretically do nothing, but simply give a hint to the compiler so to
speak? If that is true, it should merely attempt to evaluate it, but
ignore it if it cannot evaluate
Aaron McDaid wrote:
Could seq be changed so that it will not give an
error if it finds undefined?
The definition of seq is that seq _|_ x = _|_. That is
what it is supposed to do.
Actually, the behavior of seq on undefined is very
tame - it raises an exception which can be caught.
Sometimes
I think seq is funny because it is not lambda definable.
All other constructs in H98 are (except for ! on data types which is
defined in terms of seq).
-- Lennart
On Feb 8, 2007, at 01:12 , Yitzchak Gale wrote:
Haskell is a non-strict language, so non-strict
values are legitimate,
Hi,
Apologies for referring to this old thread...
I rearranged the code a little bit while experimenting but retained
the same behaviour:
Prelude let f = undefined :: Int - IO Int
Prelude (f 3 f 3) `seq` 42
42
Prelude (f 3) `seq` 42
*** Exception: Prelude.undefined
I think
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?
Thanks,
Yitz
___
Haskell-Cafe mailing list
I wrote:
1. Find a way to model strictness/laziness properties
of Haskell functions in a category in a way that is
reasonably rich.
Duncan Coutts wrote:
The reason it's not obvious for categories is because
the semantics for Haskell comes from domain theory
(CPOs etc) not categories.
The
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
On 2007 January 23 Tuesday 17:33, Yitzchak Gale wrote:
1. Find a way to model strictness/laziness properties of Haskell functions
in a category in a way that is reasonably rich.
2. Map monads in that category to Haskell, and see what we get.
3. Compare that to the traditional concept of a
Lennart Augustsson wrote:
I don't think disallowing seq for functions makes them any more
second class than not allow == for functions. I'm willing to
sacrifice seq on functions to get parametricity back.
The underlying assumption that having seq makes us lose parametricity is
a (widely
Janis Voigtlaender wrote:
Lennart Augustsson wrote:
There is a good reason seq cannot be defined for functions in
the pure lambda calculus... It doesn't belong there. :)
How about the same argument for general recursion? As in: There is a
good reason (typability) that fixpoint combinators
Janis Voigtlaender wrote:
Janis Voigtlaender wrote:
Lennart Augustsson wrote:
There is a good reason seq cannot be defined for functions in
the pure lambda calculus... It doesn't belong there. :)
How about the same argument for general recursion? As in: There is a
good reason
On Wed, 2007-01-24 at 00:33 +0200, Yitzchak Gale wrote:
My challenge is:
1. Find a way to model strictness/laziness properties
of Haskell functions in a category in a way that is
reasonably rich.
The reason it's not obvious for categories is because the semantics for
Haskell comes from
Well, I think fix destroys parametricity too, and it would be better
to get rid of fix. But I'm not proposing to do that for Haskell,
because I don't have a viable proposal to do so. (But I think the
proposal would be along the same lines as the seq one; provide fix
in a type class so we can
Lennart Augustsson wrote:
Well, I think fix destroys parametricity too, and it would be better
to get rid of fix. But I'm not proposing to do that for Haskell,
because I don't have a viable proposal to do so. (But I think the
proposal would be along the same lines as the seq one; provide fix
On Jan 24, 2007, at 8:27 AM, Lennart Augustsson wrote:
Well, I think fix destroys parametricity too, and it would be better
to get rid of fix. But I'm not proposing to do that for Haskell,
because I don't have a viable proposal to do so. (But I think the
proposal would be along the same
Limiting the value recursion is not enough, of course. You'd have to
limit the type recursion as well.
-- Lennart
On Jan 24, 2007, at 10:41 , Robert Dockins wrote:
On Jan 24, 2007, at 8:27 AM, Lennart Augustsson wrote:
Well, I think fix destroys parametricity too, and it would
troll
Prelude let f .! g = ((.) $! f) $! g
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
Prelude ((= f) .! return) `seq` 42
42
/troll
Regards,
Yitz
___
Haskell-Cafe
On Tue, 2007-01-23 at 13:35 +0200, Yitzchak Gale wrote:
troll
Prelude let f .! g = ((.) $! f) $! g
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
Prelude ((= f) .! return) `seq` 42
42
/troll
Perhaps
I wrote:
Prelude let f .! g = ((.) $! f) $! g
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
Prelude ((= f) .! return) `seq` 42
42
Duncan Coutts wrote:
Perhaps I'm missing something but I don't see what's
Could you explain why would a class Seq not be sufficient?
If there were a class Seq, I'd not want functions to be in
that class.
-- Lennart
On Jan 23, 2007, at 08:57 , Yitzchak Gale wrote:
I wrote:
Prelude let f .! g = ((.) $! f) $! g
Prelude let f = undefined :: Int - IO Int
Hi,
Lennart Augustsson wrote:
Could you explain why would a class Seq not be sufficient?
If there were a class Seq, I'd not want functions to be in
that class.
Oh, I see. Well that is pretty much the same
as ignoring seq altogether. I am hoping to get
a better answer than that - where we can
Yitzchak Gale wrote:
I wrote:
Prelude let f .! g = ((.) $! f) $! g
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
Prelude ((= f) .! return) `seq` 42
42
Duncan Coutts wrote:
Perhaps I'm missing something but I
Brian Hulley wrote:
Yitzchak Gale wrote:
I wrote:
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
The monad laws say that (= f) . return must be
identical to f.
I thought it was:
return x = f = f x
so
Brian Hulley wrote:
Brian Hulley wrote:
Yitzchak Gale wrote:
I wrote:
Prelude let f = undefined :: Int - IO Int
Prelude f `seq` 42
*** Exception: Prelude.undefined
Prelude ((= f) . return) `seq` 42
42
The monad laws say that (= f) . return must be
identical to f.
I thought it was:
Can someone explain to me, given that (a) I'm not particularly expert
at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a
bit fuzzybrained of late:
Given that _|_ represents in some sense any computation not
representable in and/or not consistent with Haskell, why/how is
On Jan 23, 2007, at 2:09 PM, Brandon S. Allbery KF8NH wrote:
Can someone explain to me, given that (a) I'm not particularly
expert at maths, (b) I'm not particularly expert at Haskell, and
(c) I'm a bit fuzzybrained of late:
Given that _|_ represents in some sense any computation not
Brandon S. Allbery KF8NH wrote:
Can someone explain to me, given that (a) I'm not particularly expert
at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a bit
fuzzybrained of late:
Me too...
Given that _|_ represents in some sense any computation not
representable in
On Jan 23, 2007, at 14:48 , Robert Dockins wrote:
Its possible, however, that I don't understand your question. The
formula (p^~p)-q (AKA, proof by contradiction) is valid most
classical and constructive logics that I know of, so I'm not quite
sure what you're getting at.
I'm not
On Jan 23, 2007, at 14:58 , Seth Gordon wrote:
The only catch I see to that POV is that the way `seq` is defined,
undefined `seq` 42 *must* return an error. If this were
analogous to
(p^~p)-q, then undefined `seq` 42 would be allowed to return any
value whatsoever.
That's not quite what
Hi
That's not quite what I was trying to say. (p^~p)-q is equivalent
to _|_ in the sense that once you derive/compute (respectively) it,
the world in which it exists breaks.
I think thats a bit overly harsh view of _|_ to take. The world does
not break once you compute _|_ - a _|_ value
On Jan 23, 2007, at 15:34 , Neil Mitchell wrote:
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But that
Hi
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But that is exactly the problem: `seq` forces _|_ to
Brandon S. Allbery KF8NH wrote:
That's not quite what I was trying to say. (p^~p)-q is equivalent
to _|_ in the sense that once you derive/compute (respectively) it,
the world in which it exists breaks. (I don't think formal logic
can have a Haskell-like _|_, but deriving (p^~p)-q is
On Jan 23, 2007, at 15:50 , Neil Mitchell wrote:
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there
aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But
Hi Brian,
Brian Hulley wrote:
I thought it was:
return x = f = f x
...I think the problem you're encountering is just
that the above law doesn't imply:
(= f) . return = f
Sorry, I was not clear.
For the purposes of this thread, I am using the
word monad in the category-theoretic
I don't think disallowing seq for functions makes them any more
second class than not allow == for functions. I'm willing to
sacrifice seq on functions to get parametricity back.
There is a good reason seq cannot be defined for functions in
the pure lambda calculus... It doesn't belong there.
46 matches
Mail list logo
