Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Nested data types and bisimilarity (dan portin)
2. Re: Monads (Patrick Lynch)
3. Re: Monads (Brent Yorgey)
----------------------------------------------------------------------
Message: 1
Date: Sat, 5 Mar 2011 03:17:57 -0800
From: dan portin <danpor...@gmail.com>
Subject: Re: [Haskell-beginners] Nested data types and bisimilarity
To: Brent Yorgey <byor...@seas.upenn.edu>
Cc: beginners@haskell.org
Message-ID:
<aanlktin1-yc26fo7phgg3psfzqoyghdk0rgjwtyds...@mail.gmail.com>
Content-Type: text/plain; charset="iso-8859-1"
> Actually, you are missing the point. ;) The point of bisimulations is
> that they are defined *coinductively*, so they let you work with
> potentially infinite data structures. In your example, proving that
> xs and ys are in the relation R really is that simple -- 1 = 1, and
> then to complete the proof we are allowed to use the coinduction
> hypothesis that xs and ys are in the relation R, since they are
> guarded by a constructor (:).
>
> Dan, does this help answer your original question? If not I can try
> to give a more detailed answer in the morning.
>
I understand the coinduction principle for data structures like streams
(e.g., Felipe's example) and finitely branching trees (from papers like "A
calculus of binary trees"). In general, for lists and types constructed from
arrow, product, and so on, it's easy to define conditions for a relation to
be a bisimulation. For instance, I know that a relation *R* is a
bisimulation over *n*-branching trees *t1 *and *t2* (for some *n*) if their
roots are equal and each of their subtrees are in *R*. My problem is,
specifically, with the case of infinitely branching trees. In Haskell, these
are modeled by the data type
T a = T a [T a]
and the possibility arises, of course, that the list [T a] is a stream.
Clearly, we can't just say that a relation *R* is a bisimulation on trees *
t1* and *t2* of type T a if their root values are equal and their *lists* of
subtrees are equal. Because if the lists are infinite, we have to prove that
they are bisimilar. And the coinduction principle for lists requires us to
have established that the head of each list is equal. But this is what we're
trying to prove!
So my questions is: what must be established to show that a relation is a
bisimulation on an infinitely branching tree of type T a? This question
arises because I'm having trouble "combining" the individual principles for
trees and lists.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20110305/28573e76/attachment-0001.htm>
------------------------------
Message: 2
Date: Sat, 05 Mar 2011 09:25:21 -0500
From: "Patrick Lynch" <kmandpjly...@verizon.net>
Subject: Re: [Haskell-beginners] Monads
To: "Brent Yorgey" <byor...@seas.upenn.edu>
Cc: beginners@haskell.org
Message-ID: <2A208718380B4F30A5361A1A363F8A0B@UserPC>
Content-Type: text/plain; format=flowed; charset=iso-8859-1;
reply-type=original
Brent,
Eureeka! I'll be damned - I can create my own class...(I had a 'typo' in my
class MyCalculator class code -- that is, myadd::...should be myAdd::...) it
works just fine...thank you. You should of bet me...
I've purchased Awodey's book: "Category Theory"...thanks again...
I've got the following books on my reading list:
"Programming in Haskell" by Graham Hutton
"Learn You a Haskell for Great Good!" by Miran Lipovaca
"Real World Haskell" by Bryan O'Sullivan, etal
"The Haskell Road to Logic, Maths and Programming" by Kees Doets, etal
"An Introduction to Functioanl Programming Systems Using Haskell" by
A.J.T Davie
"Introduction to Functional Programming using Haskell" by Richard Bird
"The Craft of Functional Programming" by Simon Thompson
I've been working with Simon Thompson, so I'll start working his book
next...
If you can recommend a book that covers Monads [for a mere practicing
software consultant], I'd welcome it...
Good weekend,
Pat
----- Original Message -----
From: "Brent Yorgey" <byor...@seas.upenn.edu>
To: "Patrick Lynch" <kmandpjly...@verizon.net>
Cc: <beginners@haskell.org>
Sent: Friday, March 04, 2011 11:33 PM
Subject: Re: [Haskell-beginners] Monads
> On Fri, Mar 04, 2011 at 05:20:27PM -0500, Patrick Lynch wrote:
>>
>> I'd love to take a crack at Category Theory [my mathematics is good]
>> but this looks like a formidable task...
>
> It is not that formidable just to get started. But it is so abstract
> that it can be difficult to gain intuition for. If you want to learn
> some category theory I recommend Awodey's book.
>
>> I'll proceed using the Monad classes and instances as is - and hope
>> that at some point I'll be able to create my own Monads...
>
> Creating one's own monads is overrated. I almost never do it.
> Usually I can just put something together using monad transformers
> that fits my needs.
>
>>
>> btw: can you create a class in Haskell -[I'm guessing the answer to
>> this is no -- see below, it doesn't work]?
>>
>> class MyCalculator a where
>> myadd::( Num a) => a -> a -> a
>> myAdd x y = x + y
>
> Sure, you can do that. What do you mean when you say that it doesn't
> work?
>
> -Brent
>
>>
>> ----- Original Message ----- From: "Brent Yorgey"
>> <byor...@seas.upenn.edu>
>> To: <beginners@haskell.org>
>> Cc: "Patrick Lynch" <kmandpjly...@verizon.net>
>> Sent: Friday, March 04, 2011 3:07 PM
>> Subject: Re: [Haskell-beginners] Monads
>>
>>
>> >On Wed, Mar 02, 2011 at 04:38:07PM -0500, Patrick Lynch wrote:
>> >>
>> >>----- Original Message ----- From: "Brent Yorgey"
>> >><byor...@seas.upenn.edu>
>> >>To: <beginners@haskell.org>
>> >>Sent: Wednesday, March 02, 2011 10:37 AM
>> >>Subject: Re: [Haskell-beginners] Monads
>> >>
>> >>
>> >>>On Wed, Mar 02, 2011 at 10:04:38AM -0500, Patrick Lynch wrote:
>> >>>>Daniel,
>> >>>>Thank you...I understand now...
>> >>>>Good day
>> >>>>
>> >>>> instance Functor Maybe where
>> >>>> fmap f (Just x) = Just (f x)
>> >>>> fmap f Nothing = Nothing
>> >>>
>> >>>So you are confused about this code? Can you be more specific what
>> >>>you are confused about? Try thinking carefully about all the types
>> >>>involved. What is the type of f? (You already answered this: a -> b.)
>> >>>What is the type of (Just x)? The type of x? What type is required on
>> >>>the right hand side of the = ? And so on.
>> >>
>> >>
>> >>-Hi Brent
>> >>I know that Maybe type is: data Maybe a = Nothing | Just a
>> >>...so, I assume that the type to the right of the '=' should be
>> >>Maybe a..
>> >
>> >Not quite. Let's look again at the type of fmap here:
>> >
>> > fmap :: (a -> b) -> Maybe a -> Maybe b
>> >
>> >So fmap will be taking *two* parameters, the first of type (a -> b),
>> >the second of type Maybe a. Then it needs to return something of type
>> >Maybe b (so this is what will be on the right hand side of the =).
>> >
>> >> instance Functor Maybe where
>> >> fmap Nothing = Nothing
>> >> fmap Just x = Just x
>> >
>> >You're missing the first argument to fmap (the one of type a -> b).
>> >Let's call it f. Since the second argument is of type (Maybe a)
>> >you're right that we should handle all cases (Nothing and Just).
>> >
>> > fmap f Nothing = Nothing
>> >
>> >so here we need to return something of type 'Maybe b'. Well, we don't
>> >have any values of type b, so the only thing we can do is return
>> >Nothing.
>> >
>> > fmap f (Just x) = ?
>> >
>> >The reason we need the parentheses around (Just x) is simply that
>> >otherwise the compiler thinks we are writing a definition of fmap that
>> >takes three arguments: f, Just, and x, but that doesn't make sense.
>> >
>> >Now, here f has type (a -> b), and (Just x) has type (Maybe a), hence
>> >x has type a. If we apply f to x we get something of type b, so we
>> >can define
>> >
>> > fmap f (Just x) = Just (f x)
>> >
>> >Does that make sense?
>> >
>> >-Brent
>>
------------------------------
Message: 3
Date: Sat, 5 Mar 2011 10:11:32 -0500
From: Brent Yorgey <byor...@seas.upenn.edu>
Subject: Re: [Haskell-beginners] Monads
To: Patrick Lynch <kmandpjly...@verizon.net>
Cc: beginners@haskell.org
Message-ID: <20110305151131.ga19...@seas.upenn.edu>
Content-Type: text/plain; charset=us-ascii
On Sat, Mar 05, 2011 at 09:25:21AM -0500, Patrick Lynch wrote:
> Brent,
>
> Eureeka! I'll be damned - I can create my own class...(I had a 'typo'
> in my class MyCalculator class code -- that is, myadd::...should be
> myAdd::...) it works just fine...thank you. You should of bet me...
> I've purchased Awodey's book: "Category Theory"...thanks again...
>
> I've got the following books on my reading list:
> "Programming in Haskell" by Graham Hutton
> "Learn You a Haskell for Great Good!" by Miran Lipovaca
> "Real World Haskell" by Bryan O'Sullivan, etal
> "The Haskell Road to Logic, Maths and Programming" by Kees Doets, etal
> "An Introduction to Functioanl Programming Systems Using Haskell"
> by A.J.T Davie
> "Introduction to Functional Programming using Haskell" by Richard Bird
> "The Craft of Functional Programming" by Simon Thompson
> I've been working with Simon Thompson, so I'll start working his book
> next...
>
> If you can recommend a book that covers Monads [for a mere practicing
> software consultant], I'd welcome it...
Real World Haskell is such a book -- I haven't read the part about
monads but I've heard good things about it, that it introduces them in
a quite practical, example-driven, no-nonsense way.
-Brent
>
> Good weekend,
> Pat
>
> ----- Original Message ----- From: "Brent Yorgey"
> <byor...@seas.upenn.edu>
> To: "Patrick Lynch" <kmandpjly...@verizon.net>
> Cc: <beginners@haskell.org>
> Sent: Friday, March 04, 2011 11:33 PM
> Subject: Re: [Haskell-beginners] Monads
>
>
> >On Fri, Mar 04, 2011 at 05:20:27PM -0500, Patrick Lynch wrote:
> >>
> >>I'd love to take a crack at Category Theory [my mathematics is good]
> >>but this looks like a formidable task...
> >
> >It is not that formidable just to get started. But it is so abstract
> >that it can be difficult to gain intuition for. If you want to learn
> >some category theory I recommend Awodey's book.
> >
> >>I'll proceed using the Monad classes and instances as is - and hope
> >>that at some point I'll be able to create my own Monads...
> >
> >Creating one's own monads is overrated. I almost never do it.
> >Usually I can just put something together using monad transformers
> >that fits my needs.
> >
> >>
> >>btw: can you create a class in Haskell -[I'm guessing the answer to
> >>this is no -- see below, it doesn't work]?
> >>
> >> class MyCalculator a where
> >> myadd::( Num a) => a -> a -> a
> >> myAdd x y = x + y
> >
> >Sure, you can do that. What do you mean when you say that it doesn't
> >work?
> >
> >-Brent
> >
> >>
> >>----- Original Message ----- From: "Brent Yorgey"
> >><byor...@seas.upenn.edu>
> >>To: <beginners@haskell.org>
> >>Cc: "Patrick Lynch" <kmandpjly...@verizon.net>
> >>Sent: Friday, March 04, 2011 3:07 PM
> >>Subject: Re: [Haskell-beginners] Monads
> >>
> >>
> >>>On Wed, Mar 02, 2011 at 04:38:07PM -0500, Patrick Lynch wrote:
> >>>>
> >>>>----- Original Message ----- From: "Brent Yorgey"
> >>>><byor...@seas.upenn.edu>
> >>>>To: <beginners@haskell.org>
> >>>>Sent: Wednesday, March 02, 2011 10:37 AM
> >>>>Subject: Re: [Haskell-beginners] Monads
> >>>>
> >>>>
> >>>>>On Wed, Mar 02, 2011 at 10:04:38AM -0500, Patrick Lynch wrote:
> >>>>>>Daniel,
> >>>>>>Thank you...I understand now...
> >>>>>>Good day
> >>>>>>
> >>>>>> instance Functor Maybe where
> >>>>>> fmap f (Just x) = Just (f x)
> >>>>>> fmap f Nothing = Nothing
> >>>>>
> >>>>>So you are confused about this code? Can you be more specific what
> >>>>>you are confused about? Try thinking carefully about all the types
> >>>>>involved. What is the type of f? (You already answered this: a -> b.)
> >>>>>What is the type of (Just x)? The type of x? What type is required on
> >>>>>the right hand side of the = ? And so on.
> >>>>
> >>>>
> >>>>-Hi Brent
> >>>>I know that Maybe type is: data Maybe a = Nothing | Just a
> >>>>...so, I assume that the type to the right of the '=' should be
> >>>>Maybe a..
> >>>
> >>>Not quite. Let's look again at the type of fmap here:
> >>>
> >>> fmap :: (a -> b) -> Maybe a -> Maybe b
> >>>
> >>>So fmap will be taking *two* parameters, the first of type (a -> b),
> >>>the second of type Maybe a. Then it needs to return something of type
> >>>Maybe b (so this is what will be on the right hand side of the =).
> >>>
> >>>> instance Functor Maybe where
> >>>> fmap Nothing = Nothing
> >>>> fmap Just x = Just x
> >>>
> >>>You're missing the first argument to fmap (the one of type a -> b).
> >>>Let's call it f. Since the second argument is of type (Maybe a)
> >>>you're right that we should handle all cases (Nothing and Just).
> >>>
> >>> fmap f Nothing = Nothing
> >>>
> >>>so here we need to return something of type 'Maybe b'. Well, we don't
> >>>have any values of type b, so the only thing we can do is return
> >>>Nothing.
> >>>
> >>> fmap f (Just x) = ?
> >>>
> >>>The reason we need the parentheses around (Just x) is simply that
> >>>otherwise the compiler thinks we are writing a definition of fmap that
> >>>takes three arguments: f, Just, and x, but that doesn't make sense.
> >>>
> >>>Now, here f has type (a -> b), and (Just x) has type (Maybe a), hence
> >>>x has type a. If we apply f to x we get something of type b, so we
> >>>can define
> >>>
> >>> fmap f (Just x) = Just (f x)
> >>>
> >>>Does that make sense?
> >>>
> >>>-Brent
> >>
>
------------------------------
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 33, Issue 7
****************************************
