[Haskell-cafe] Monad laws
David Sabel
sabel at ki.informatik.uni-frankfurt.de
Wed Mar 3 03:16:19 EST 2010
Hi,
thanks for all the comments.
In ghc 6.12.1 the behavior is strange:
If f is "defined" in the interpreter via let, then the seq-expression converges
GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help
> let f = \x -> (undefined::IO Bool)
> seq (f True) True
True
but if you build a let-expression then it diverges
> let f = \x -> (undefined::IO Bool) in seq (f True) True
*** Exception: Prelude.undefined
for the first way: if you use another type, then it diverges:
> let f = \x -> (undefined::Bool)
> seq (f True) True
*** Exception: Prelude.undefined
Regards,
David
Andrés Sicard-Ramírez schrieb:
>
> On 2 March 2010 15:44, Luke Palmer <lrpalmer at gmail.com
> <mailto:lrpalmer at gmail.com>> wrote:
>
> On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
> <sabel at ki.informatik.uni-frankfurt.de
> <mailto:sabel at ki.informatik.uni-frankfurt.de>> wrote:
> > Hi,
> > when checking the first monad law (left unit) for the IO-monad
> (and also for
> > the ST monad):
> >
> > return a >>= f ≡ f a
> >
> > I figured out that there is the "distinguishing" context (seq []
> True) which
> > falsifies the law
> > for a and f defined below
> >
> >
> >> let a = True
> >> let f = \x -> (undefined::IO Bool)
> >> seq (return a >>= f) True
> > True
> >> seq (f a) True
> > *** Exception: Prelude.undefined
> >
> > Is there a side-condition of the law I missed?
>
> No, IO just doesn't obey the laws. However, I believe it does in the
> seq-free variant of Haskell, which is nicer for reasoning. In fact,
> this difference is precisely what you have observed: the
> distinguishing characteristic of seq-free Haskell is that (\x ->
> undefined) == undefined, whereas in Haskell + seq, (\x -> undefined)
> is defined.
>
>
> In GHC 6.12.1 both expressions reduce to True, but it doesn't happen in
> GHC 6.10.4. Any ideas why the behaviour is different?
>
> --
> Andrés
More information about the Haskell-Cafe
mailing list