Re: [Haskell-cafe] Re: A free monad theorem?
On Sun, Sep 03, 2006 at 01:23:13AM +0200, [EMAIL PROTECTED] wrote: Tomasz Zielonka: Programmers define the = method for their monads because they want to use it to bind computations. They know how to pass result(s) from one computation in their Monad to another, and they put this algorithm in the implementation of =. If they didn't care about passing results from one computation to the next one, they wouldn't be using monads in the first place. Shrug. If these programmers didn't care about passing results from one computation to the next one, they wouldn't use functional programming at all. Hm. Would it still be programming?... I myself wanted to write that then they wouldn't be using a general purpose programming language, but something like HTML, etc. But then I thought that you may want to have computations that can't pass values between each other. One example is an algebraic datatype for describing tree-like structures - but you could argue that there is a bottom-up data flow. Anyway, I haven't thought about it too much... Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: A free monad theorem?
Hello All, many thanks for all the interesting answers. I think I have enough now to think about for a while. Cheers, Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: A free monad theorem?
Tomasz Zielonka: Programmers define the = method for their monads because they want to use it to bind computations. They know how to pass result(s) from one computation in their Monad to another, and they put this algorithm in the implementation of =. If they didn't care about passing results from one computation to the next one, they wouldn't be using monads in the first place. Shrug. If these programmers didn't care about passing results from one computation to the next one, they wouldn't use functional programming at all. Hm. Would it still be programming?... Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A free monad theorem?
Il Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka ebbe a scrivere:
On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:
So getting the value out of the monad is not a pure function (extract ::
Monad m = m a - a). I think I stated that, already, in my previous post.
The only generic way of extracting values from a monadic value is
the bind operator. The lack of extract function is a feature :-)
But now I know that you are not really claiming such a function exists.
I do not understand this discussion, but I'd like to.
Can you please tell me what you are talking about in terms of this
example?
Thanks,
Andrea
module Test where
newtype M a = TypeConstructor {unpack::(a, String)}
deriving (Show)
instance Monad M where
return a = (TypeConstructor (a,))
(=) m f = TypeConstructor (a1,b++b1)
where (a,b) = unpack m
(a1,b1) = unpack (f a)
putB b = TypeConstructor ((),b)
putA a = (TypeConstructor (a,))
getA (TypeConstructor (a,b)) = a
getB (TypeConstructor (a,b)) = b
transformM :: Int - M Int
transformM a = do putA 3
putB ciao
putA 6
putB cosa?
return 4
{-
*Test let a = transformM 1
*Test a
TypeConstructor {unpack = (4,ciao cosa?)}
*Test getA a
4
*Test getB a
ciao cosa?
*Test
-}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A free monad theorem?
Benjamin Franksen wrote:
Tomasz Zielonka wrote:
whatever you do, you won't be able to extract an 'a' typed
value, non-bottom from this computation. Cont is defined as:
newtype Cont r a = Cont {runCont :: (a - r) - r)}
So getting the value out of the monad is not a pure function (extract
:: Monad m = m a - a). I think I stated that, already, in my
previous post. I'd even say that the monadic values alone can be
completely meaningless. They often have a meaning only relative to
some environment, thus are (usually) _effectful_ computations. But we
already knew that, didn't we?
The real question (the one that bugs me, anyway) is if one can give a
precise meaning to the informal argument that if the definition of
bind is to be non-trivial then its second argument must be applied to
some non-trivial value at one point (but not, of course, in all
cases, nor necessarily only once), and that this implies that the
computation represented by the first argument must somehow be 'run'
(in some environment) in order to produce such a value.
I think the continuation monad might help to refine the intuition:
Cont a_r_r = a_C_b_r_r = Cont $ \ b_r -
a_r_r (\a - runCont (a_C_b_r_r a) b_r)
so it is clear that
1) The first computation (a_r_r x) might involve running the second
(applying b_r_r to b_r) so it gives a counterexample to the idea that the
first computation is run to completion before the second one starts, though
it preserves the intuition that at least the first computation is started
first.
2) The bind operation has arranged that value(s) of type (a) are supplied in
the course of running the first computation to the second (in the
non-trivial case where the second computation is actually run)
Perhaps the argument could be that because the (a) is polymorphic, this
implies that if the second computation is run at all, at least we know that
the first computation has already started, and that the (a) came from the
part of the first computation we've done so far, though of course this is
still unfortunately very vague.
Regards, Brian.
--
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.
http://www.metamilk.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A free monad theorem?
On Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka wrote: The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once) How about using monad laws, specifically: (return x) = f == f x We assume that = never uses it's second argument, so: (return x) = f == (return x) = g Combining it with the above monad law we get: f x == (return x) = f == (return x) = g == g x so f x = g x for arbitrary f and g. Let's substitute return for f and undefined for g: return x = undefined x so return x = undefined Now that seems like a very trivial (and dysfunctional) monad. I just realized that I haven't addressed your exact problem, but maybe you'll be able to use a similar reasoning to prove your theorem. What (I think) I proved is that: if = never uses its second argument, then the monad is dysfunctional (maybe not even a monad at all). Again, informally, it is obvious. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: A free monad theorem?
Chris Kuklewicz wrote:
Benjamin Franksen wrote:
I'd like to know if the following reasoning can be made more precise:
As we all know, the monadic bind operation has type:
bind :: Monad m = m a - (a - m b) - m b
My intuition says that in order to apply the second argument to some
non-trivial (i.e. non-bottom) value of type a, the bind operator needs to
be able to somehow 'extract' a value (of type a) from the first argument
(of type m a). I would like to argue that this is because bind is
polymorphic in a, which makes it impossible to construct values of type
a 'out of thin air' (besides bottom). Thus, however bind is defined, the
only place where it can obtain a 'real' value of type a is from its first
argument. Although one might think that this implies the existence of
some function
extract :: Monad m = m a - a
it is obvious that this is too limiting, as the IO monad plainly shows.
Even monads that can be implemented in Haskell itself (the vast majority,
it seems) usually need some additional (monad-specific) argument to
their 'extract' (or 'run') function. However, even a value of type IO
a /does/ produce a value of type a, only the 'value producing
computation' is not a (pure) function. But how can all this be made more
precise with less handwaiving?
You can cheat a bit and write your own IO a - a using GHC:
{-
Taken from the shootout at
http://shootout.alioth.debian.org/gp4/benchmark.php?test=knucleotidelang=ghcid=2
-}
import GHC.Exts -- for realWorld# value
import GHC.IOBase -- for IO constructor
{-# INLINE inlinePerformIO #-}
inlinePerformIO :: IO a - a
inlinePerformIO (IO m) = case m realWorld# of (# _, r #) - r
-- Now you can write things like this, which need IO action to define pure
-- functions:
data Seq = Seq !Int !(Ptr Base)
instance Eq Seq where
(==) (Seq (I# size1) (Ptr ptr1)) (Seq _ (Ptr ptr2)) = inlinePerformIO $
IO
(\s - eqmem size1 ptr1 ptr2 s)
{-# INLINE eqmem #-}
eqmem remainingSize ptr1 ptr2 s = if remainingSize ==# 0# then (# s , True
#)
else case readInt8OffAddr# ptr1 0# s of { (# s, i8a #) -
case readInt8OffAddr# ptr2 0# s of { (# s, i8b #) -
if i8a /=# i8b then (# s, False #)
else eqmem (remainingSize -# 1#) (plusAddr# ptr1 1#)
(plusAddr#
ptr2 1#) s } }
Would you (or someone else) care to explain what this exercise in advanced
ghc hacking has to do with my question? I don't exclude the remote
possibility that there is some connection but I don't get it.
Ben
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: A free monad theorem?
Tomasz Zielonka wrote:
On Thu, Aug 31, 2006 at 07:23:55PM +0200, Benjamin Franksen wrote:
I'd like to know if the following reasoning can be made more precise:
As we all know, the monadic bind operation has type:
bind :: Monad m = m a - (a - m b) - m b
My intuition says that in order to apply the second argument to some
non-trivial (i.e. non-bottom) value of type a, the bind operator needs to
be able to somehow 'extract' a value (of type a) from the first argument
(of type m a).
The bind operator doesn't have to neccesarily apply the second argument
to anything. What if m is Maybe, and the first arguments is Nothing?
True, however if the instance for Maybe would have been defined
without /ever/ applying the second argument to anything, then wouldn't this
necessarily be a trivial monad (however one would need to define 'trivial'
here)?
And if the bind operator wants to apply the second argument to
something, it doesn't have to do it only once - consider the [] monad.
Yes, I should have said: Any non-trivial definition of bind has to apply its
second argument at least in _some_ cases and _at least_ once to something
non-bottom.
Other examples:
get :: State s s-- from Control.Monad.State
there is no way you can extract an 's' value from get alone -
you have to supply the state to the whole computation
Cont (const ()) :: Cont () a-- from Control.Monad.Cont
whatever you do, you won't be able to extract an 'a' typed
value, non-bottom from this computation. Cont is defined as:
newtype Cont r a = Cont {runCont :: (a - r) - r)}
So getting the value out of the monad is not a pure function (extract ::
Monad m = m a - a). I think I stated that, already, in my previous post.
I'd even say that the monadic values alone can be completely meaningless.
They often have a meaning only relative to some environment, thus are
(usually) _effectful_ computations. But we already knew that, didn't we?
The real question (the one that bugs me, anyway) is if one can give a
precise meaning to the informal argument that if the definition of bind is
to be non-trivial then its second argument must be applied to some
non-trivial value at one point (but not, of course, in all cases, nor
necessarily only once), and that this implies that the computation
represented by the first argument must somehow be 'run' (in some
environment) in order to produce such a value. -- And, of course, whether
this is actually true in the first place. Would you say that your examples
above are counter-examples to this statement (imprecise as it is,
unfortunately)?
Ben
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A free monad theorem?
So getting the value out of the monad is not a pure function (extract :: Monad m = m a - a). I think I stated that, already, in my previous post. I'd even say that the monadic values alone can be completely meaningless. They often have a meaning only relative to some environment, thus are (usually) _effectful_ computations. But we already knew that, didn't we? It may help to remember that, in the mathematical context where monads where born (AKA category theory), a monad is generally defined as a functor with a join and a unit (satisfying some laws that I would have to look up). The unit should be familiar (it's spelled 'return' in haskell), but join may not be. Its type is join :: Monad m = m (m a) - m a which is a lot like extract, except with one more monad layer wrapped around it. IIRC the relevant identity here is: x = f === join (fmap f x) and with f specialzed to id: join (fmap id x) === x = id join x === x = id I'm not sure why (=) is taken as basic in Haskell. At any rate, my point is that I think your questions might be better framed in terms of the behavior of 'fmap'. The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once), and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value. -- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)? Ben -- Rob Dockins Talk softly and drive a Sherman tank. Laugh hard, it's a long way to the bank. -- TMBG ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A free monad theorem?
On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote: So getting the value out of the monad is not a pure function (extract :: Monad m = m a - a). I think I stated that, already, in my previous post. The only generic way of extracting values from a monadic value is the bind operator. The lack of extract function is a feature :-) But now I know that you are not really claiming such a function exists. The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once) How about using monad laws, specifically: (return x) = f == f x We assume that = never uses it's second argument, so: (return x) = f == (return x) = g Combining it with the above monad law we get: f x == (return x) = f == (return x) = g == g x so f x = g x for arbitrary f and g. Let's substitute return for f and undefined for g: return x = undefined x so return x = undefined Now that seems like a very trivial (and dysfunctional) monad. and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value. Not sure what to do with this one. Certainly, for some monads the environment can be empty, eg. for Identity or []. For the IO monad the lack of the run function is a feature (Let's pretend that unsafePerformIO doesn't exist - in fact, there is no such function in Haskell 98), but you can say that the RTS runs the main IO computation. Informally, it seems obvious that you have to be able to run your monadic computations somehow - otherwise you wouldn't be writing them ;-) I am not sure you can prove it though. -- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)? Well, no, they were counter-examples for the existence of the extract function. As you say, I misunderstood you intent. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
