Send Beginners mailing list submissions to
[email protected]
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
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: [Haskell-cafe] Enum and Bounded in generic type
(Robert Greayer)
2. about the concatenation on a tree (Max cs)
3. Re: [Haskell-cafe] bottom case in proof by induction
(Martijn van Steenbergen)
4. Re: [Haskell-cafe] 'Iterating a data type' (Luke Palmer)
5. Re: [Haskell-cafe] bottom case in proof by induction
(Luke Palmer)
6. Re: [Haskell-cafe] bottom case in proof by induction
(Jonathan Cast)
7. Re: [Haskell-cafe] Enum and Bounded in generic type
(Derek Elkins)
----------------------------------------------------------------------
Message: 1
Date: Tue, 30 Dec 2008 09:45:36 -0800 (PST)
From: Robert Greayer <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] Enum and Bounded in
generic type
To: [email protected], [email protected], [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Raeck said:
> Hi, how can I make the following code work? (show all the possible values of
> a type 'a')
>> showAll :: (Eq a, Bounded a, Enum a) => a -> [a]
>> showAll a = [minBound..maxBound]::[a]
What you are really looking for, I think, is a polymorphic value of type [a],
where a is some enumerable, bounded type.
allValues :: (Enum a, Bounded a) => [a]
allValues = [minBound .. maxBound]
You can omit the type signature, but then you'll run into the monomorphism
restriction (which you'll can turn off with, e.g. -XNoMonomorphismRestriction)
------------------------------
Message: 2
Date: Wed, 31 Dec 2008 14:59:24 +0000
From: "Max cs" <[email protected]>
Subject: [Haskell-beginners] about the concatenation on a tree
To: "[email protected]" <[email protected]>,
"[email protected]" <[email protected]>
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
hi all, not sure if there is someone still working during holiday like me :
)
I got a little problem in implementing some operations on tree.
suppose we have a tree date type defined:
data Tree a = Leaf a | Branch (Tree a) (Tree a)
I want to do a concatenation on these tree just like the concat on list.
Anyone has idea on it? or there are some existing implementation?
Thank you and Happy New Year!
regards,
Max
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20081231/8de41a30/attachment-0001.htm
------------------------------
Message: 3
Date: Thu, 01 Jan 2009 02:16:39 +0100
From: Martijn van Steenbergen <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] bottom case in proof
by induction
To: Luke Palmer <[email protected]>
Cc: [email protected], [email protected], [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Luke Palmer wrote:
> First, by simple definition, id _|_ = _|_. Now let's consider foo _|_.
> The Haskell semantics say that pattern matching on _|_ yields _|_, so
> foo _|_ = _|_. So they are equivalent on _|_ also. Thus foo and id are
> exactly the same function.
Would it in general also be interesting to look at foo == id for input
(_|_:xs) and all other possible positions and combinations of positions
for bottom? I wonder how many cases you need to take into consideration
to have covered every possible situation.
Martijn.
------------------------------
Message: 4
Date: Mon, 29 Dec 2008 18:28:46 -0700
From: "Luke Palmer" <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] 'Iterating a data
type'
To: [email protected]
Cc: Beginners Haskell <[email protected]>, Cafe Haskell
<[email protected]>
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
On Mon, Dec 29, 2008 at 6:24 PM, <[email protected]> wrote:
> Are there anyway to express the "iterating" of a user-defined data type in
> Haskell?
>
> For example, in
>
> data Shape = Square | Circle | Triangle
>>
>
> how can I 'iterate' them and apply them all to the same function without
> indicating them explicitly?
> such as [func Square, func Circle, func Triangle].
> Can I use a form similar to the following case in a list instead:
>
> Numbers = [1,2,3,4,5]
>>
>
> [func x | x <- Numbers ]
>>
>
> Actually what I want is to obtain all the possible values of a data type
> (Shape).
For "enum" style data, where all the constructors have no arguments, you can
do deriving (Bounded, Enum), so:
data Shape = Square | Circle | Triangle
deriving (Bounded,Enum)
Then:
numbers = [minBound..maxBound] :: [Shape]
Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20081229/a5358a1f/attachment-0001.htm
------------------------------
Message: 5
Date: Wed, 31 Dec 2008 15:19:26 -0700
From: "Luke Palmer" <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] bottom case in proof
by induction
To: [email protected]
Cc: [email protected], [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
2008/12/31 <[email protected]>
> Dear all,
>
> Happy New Year!
>
> I am learning the Induction Proof over Haskell, I saw some proofs for the
> equivalence of two functions will have a case called 'bottom' but some of
> them do no have. What kind of situation we should also include the bottom
> case to the proof? How about the functions do not have the 'bottom' input
> such as:
>
> foo [] = []
> foo (x:xs) = x : (foo xs)
>
Okay, I'm not sure what you mean by bottom. You could either mean the base
case, or you could mean bottom -- non-terminating inputs -- as in domain
theory.
Let's say you wanted to see if foo is equivalent to id.
id x = x
We can do it without considering nontermination, by induction on the
structure of the argument:
First, the *base case*: empty lists.
foo [] = []
id [] = []
Just by looking at the definitions of each.
Now the inductive case. Assume that foo xs = id xs, and show that foo
(x:xs) = id (x:xs), for all x (but a fixed xs).
foo (x:xs) = x : foo xs
foo xs = id xs by our the induction hypothesis, so
foo (x:xs) = x : id xs = x : xs
And then just by the definition of id:
id (x:xs) = x : xs
And we're done.
Now, maybe you meant bottom as in nontermination. In this case, we have to
prove that they do the same thing when given _|_ also. This requires a
deeper understanding of the semantics of the language, but can be done
here.
First, by simple definition, id _|_ = _|_. Now let's consider foo _|_. The
Haskell semantics say that pattern matching on _|_ yields _|_, so foo _|_ =
_|_. So they are equivalent on _|_ also. Thus foo and id are exactly the
same function.
See http://en.wikibooks.org/wiki/Haskell/Denotational_semantics for more
about _|_.
Happy mathhacking,
Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20081231/71a112a0/attachment-0001.htm
------------------------------
Message: 6
Date: Wed, 31 Dec 2008 22:08:57 -0600
From: Jonathan Cast <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] bottom case in proof
by induction
To: [email protected]
Cc: Luke Palmer <[email protected]>, [email protected],
[email protected]
Message-ID: <1230782941.6019.12.ca...@jonathans-macbook>
Content-Type: text/plain
On Thu, 2009-01-01 at 03:50 +0000, [email protected] wrote:
> I am afraid I am still confused.
>
> > foo [] = ...
> > foo (x:xs) = ...
> > There is an implied:
> > foo _|_ = _|_
> > The right side cannot be anything but _|_. If it could, then that
> would imply we could solve the halting problem:
>
> in a proof, how I could say the right side must be _|_ without
> defining foo _|_ = _|_ ?
This definition is taken care of for you by the definition of Haskell
pattern matching. If the first equation for a function has a pattern
other than
* a variable or
* a lazy pattern (~p)
for a given argument, then supplying _|_ for that argument /must/ (if
the application is total) return _|_. By rule. (We say the pattern is
strict, in this case).
> and in the case of
>
> > bad () = _|_
> > bad _|_ = ()
Note that these equations (which are not in the right form for the
Haskell equations that define Hasekll functions) aren't satisfied by any
Haskell function!
> mean not every function with a _|_ input will issue a _|_ output,
True --- but we can say a couple of things:
* For all Haskell functions f, if f _|_ is an application of a
constructor C, then f x is an application of C (to some value), for all
x. [1]
* For all Haskell functions f, if f _|_ is a lambda expression, then f
x is a lambda expression, for all x.
The only other possibility for f _|_ is _|_.
(Do you see why bad above is impossible?)
> so we have to say what result will be issued by a _|_ input in the
> definitions of the functions if we want to prove the equvalence
> between them?
You have to deduce what the value at _|_ will be.
> However, in the case of map f _|_ , I do believe the result will be
> _|_ since it can not be anything else, but how I could prove this? any
> clue?
Appeal to the semantics of Haskell pattern matching. If you like, you
can de-sugar the definition of map a little, to get
map = \ f xn -> case xn of
[] -> []
x:xn0 -> f x : map f xn0
And then you know that
case _|_ of
[] -> ...
...
= _|_
whatever you fill in for the ellipses. (Do you see why this *must* be
part of the language definition?)
> ps, the definition of map does not mention anything about _|_ .
The behavior of map f _|_ is fixed by the definition of Haskell pattern
matching.
jcc
------------------------------
Message: 7
Date: Tue, 30 Dec 2008 11:22:34 -0600
From: Derek Elkins <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] Enum and Bounded in
generic type
To: [email protected]
Cc: [email protected], [email protected]
Message-ID: <1230657754.31199.1.ca...@derek-laptop>
Content-Type: text/plain; charset=utf-8
On Tue, 2008-12-30 at 17:12 +0000, [email protected] wrote:
> Hi, how can I make the following code work? (show all the possible values of
> a type 'a')
>

> > showAll :: (Eq a, Bounded a, Enum a) => a -> [a]
> > showAll a = [minBound..maxBound]::[a]
The bottom 'a' has nothing to do with the 'a' in the type signature.
Your code is equivalent to

> > showAll :: (Eq a, Bounded a, Enum a) => a -> [a]
> > showAll a = [minBound..maxBound]::[b]
Which is not type correct as [minBound..maxBound] :: (Bounded a, Enum a) => [a]
You don't need that type annotation (or the type signature for that matter), so
just omit it.
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 7, Issue 4
***************************************
