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: structural induction, two lists, simultaneous (Rustom Mody)
2. Re: exercises/examples for streams (Carl Eyeinsky)
3. Why does Haskell PVP have two values for the major version?
"A.B..." and a couple other questions (Zach Moazeni)
----------------------------------------------------------------------
Message: 1
Date: Mon, 15 Dec 2014 23:24:35 +0530
From: Rustom Mody <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] structural induction, two lists,
simultaneous
Message-ID:
<CAJ+Teoed0v09TWtusw7_KZHuFYbdkNj3nE_JfTq6SZ7AtHv=r...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
On Mon, Dec 15, 2014 at 7:12 AM, Pascal Knodel <[email protected]>
wrote:
>
> Hi list,
>
>
> Proposition:
>
> map f (ys ++ zs) = map f ys ++ map f zs
>
> (Haskell, the craft of functional programming, exercise 11.31)
>
>
> Almost every time I'm asked to do (structural) induction over multiple
> 'things', in this example lists, I don't know how to do it.
> (I encountered similar difficulties when I worked through chapter 9, see
> https://github.com/pascal-knodel/haskell-craft/tree/master/Chapter%209 ,
> ex. 9.5 , https://github.com/pascal-knodel/haskell-craft/blob/
> master/Chapter%209/E%279%27%275.hs).
> I think my proof in this case isn't formally correct. It feels like it
> isn't.
>
> I would like to do the example with your help, so that I feel a
> little bit safer.
>
> Let's start with the base case. If I have two lists, do I select
> one, say ys := [] . Only one or one after another? Or both 'parallel'?
> I could state ys ++ zs := [] too, does it help?
>
> I could imagine that the proposition could be expanded to something like
>
> map f (l1 ++ l2 ++ ... ++ lN) = map f ys ++ map f zs
> = map f l1 ++ map f l2 ++ ... ++ map f lN
>
> And I could imagine that it is possible to do induction over more than two
> lists too.
>
> What is the reason why we can do it over two 'objects' at the same time?
> How do I start? Can you explain this to me?
>
>
This is a right question
It is somewhat a proof-version of currying
What you want to prove is
(? f,ys,zs ? map f (ys ++ zs) = map f ys ++ map f zs)
= "reorder the variables"
(? ys,f,zs ? map f (ys ++ zs) = map f ys ++ map f zs)
= "(? x,y ? ...) = (?x ? (? y ? ...))"
(? ys ? (? f,zs ? map f (ys ++ zs) = map f ys ++ map f zs))
And now you can see that you want a proof of a one-variable theorem
Of course at this stage you might ask "Why did you choose to pull ys out
and not zs (or f for that matter)?"
One possible answer: Experience!
Another: Recursion in definitions and induction in proofs go hand in hand.
Clearly the recursion is happening on the first list. So we may expect the
induction to focus there
>
> Attempt:
>
> -- ---------------
> -- 1. Proposition:
> -- ---------------
> --
> -- map f (ys ++ zs) = map f ys ++ map f zs
> --
> --
> -- Proof By Structural Induction:
> -- ------------------------------
> --
> --
> -- 1. Induction Beginning (1. I.B.):
> -- ---------------------------------
> --
> --
> -- (Base case 1.) :<=> ys := []
> --
> -- => (left) := map f (ys ++ zs)
> -- | (Base case 1.)
> -- = map f ([] ++ zs)
> -- | ++
> -- = map f zs
> --
> --
> -- (right) := map f ys ++ map f zs
> -- | (Base case 1.)
> -- = map f [] ++ map f zs
> -- | map
> -- = map f zs
> --
> --
> -- => (left) = (right)
> --
> -- ?
> --
> --
> -- 1. Induction Hypothesis (1. I.H.):
> -- ----------------------------------
> --
> -- For an arbitrary, but fixed list "ys", the statement ...
> --
> -- map f (ys ++ zs) = map f ys ++ map f zs
> --
> -- ... holds.
> --
> --
> -- 1. Induction Step (1. I.S.):
> -- ----------------------------
> --
> --
> -- (left) := map f ( (y : ys) ++ zs )
> -- | ++
> -- = map f ( y : ( ys ++ zs ) )
> -- | map
> -- = f y : map f ( ys ++ zs )
> -- | (1. I.H.)
> -- = f y : map f ys ++ map f zs
> -- | map
> -- = map f (y : ys) ++ map f zs
> --
> --
> -- (right) := map f (y : ys) ++ map f zs
> --
> --
> -- => (left) = (right)
> --
> --
> -- ??? (1. Proof)
>
>
> But in this 'proof attempt' only "ys" was considered (1. I.H.).
> What do I miss?
>
> Pascal
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
--
http://www.the-magus.in
http://blog.languager.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141215/298e9ee6/attachment-0001.html>
------------------------------
Message: 2
Date: Mon, 15 Dec 2014 21:46:27 +0100
From: Carl Eyeinsky <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] exercises/examples for streams
Message-ID:
<cadkv3ae+uzdhm0bn_a6usbhkxedwny_2kgpmom89qzvadlg...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi Pascal,
for the 2., yes, the first member of the tuple is the list index in the
list-of-lists (i.e for [[1], [2,3], [4,5,6]], the 0th is [1], and 2nd is
[4,5,6]).
The other questions in order:
* Yes the sublists themselves have ascending order elements in themselves
(you can just 'map sort' if otherwise).
* I think the computation is non-blocking, even if the sublists themselves
are infinite. The conditions for non-blocking'ness are that (1) the
sublists are in ascending oreder, and (2) the outer list is finite. I think
these are enough.
* The list-of-lists (=outer list) is not sorted. I presume you mean by its
sub-lists' heads?
The main idea (which you probably get, but to spell it out :) ) is that in
previously we had Left for index 0 and Right for index 1, but now we use
tuples as it fits better than using nested Either's.
And on the typing of 'sorts ls rs = ls ++ rs' -- yes, its about types.
There was a simila remark some moths ago in the lines of if say you have a
function:
f :: Either Int Integer -> Either Int String
then why doesn't this work:
f (Right x) = Right (show x)
f left = left
The trouble is the second definition where 'left' on both sides of the
definition is a Left with an Int in it, but the types the lhs and rhs are
different. The solution is to spell out both the input and output Left's:
f (Left i) = Left i
The same would go for the lists -- if you expect both of them to be empty,
then 'sorts ls rs = []' would work.
Happy hacking,
On Sun, Dec 14, 2014 at 11:52 PM, Pascal Knodel <[email protected]>
wrote:
>
> Hi Carl,
>
> --------------------------------------- snip
> ---------------------------------------
> module BeginnerStreams where
>
> -- 1. First try:
>
> -- Contract: Input lists are sorted.
> --
> -- Notes:
> --
> -- (!) Duplicate elements are allowed.
> -- (!) Sort `Left` before `Right`.
>
>
> sorts :: Ord a => [a] -> [a] -> [Either a a]
> sorts (l : ls) (r : rs)
>
> | l <= r = Left l : sorts ls (r : rs)
>
> | otherwise = Right r : sorts (l : ls) rs
> -- l > r
>
> sorts [] (r : rs) = Right r : sorts' Right rs
> sorts (l : ls) [] = Left l : sorts' Left ls
> sorts [] [] = []
>
> sorts' e (i : is) = e i : sorts' e is
> sorts' _ [] = []
>
>
> -- The difficulty for me was: "Either".
> -- I forgot about it while defining and
> -- did wrong in defining the empty list
> -- cases in my first definition:
> --
> -- sorts ls rs = ls ++ rs
> --
> -- That isn't possible without constructor application,
> -- because of the output type "[Either a a]". Is it?
> --
> -- Wish there would be GHCi in the exam.
>
> -- Where else did I fail and didn't notice it?
> -- What higher order functions would you use to define "sorts"?
>
>
> -- 2. First try:
>
> -- I'm not sure, what do you mean by 'value itself'?
> -- Why is the second tuple (2,1)? Ah, I see, is it sth. like:
> --
> -- [1,3] is index 0 and becomes (0,1), (03)
> -- [2,3] 1 (1,2), (1,3)
> -- ...
> --
> -- And those sorted in ascending order by the sum of the components?
> -- Is it possible to stream this computation without blocking?
> -- Is the list-of-lists sorted?
> --------------------------------------- snip
> ---------------------------------------
>
> The exercises from old exams that I have solved are at:
> https://github.com/pascal-knodel/Programming-Paradigms-
> KIT-2014-2015/tree/master/3
>
>
>
> Pascal
>
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
--
Carl Eyeinsky
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141215/e6a2199c/attachment-0001.html>
------------------------------
Message: 3
Date: Mon, 15 Dec 2014 19:38:19 -0500
From: Zach Moazeni <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: [Haskell-beginners] Why does Haskell PVP have two values for
the major version? "A.B..." and a couple other questions
Message-ID:
<ca+60nj6p_zteqxcp-rzhopxq1mwxds4okgqs5ahdn5u_d2j...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hello,
Forgive me if this is a frequently asked question, I've searched the web
and can't find an answer.
What is the history that led up to the PVP
<https://www.haskell.org/haskellwiki/Package_versioning_policy> specifying
two values as the major version?
I come from other tools that primarily use http://semver.org/ (or a
variant) and I'm confused in what cases I should bump "A" but not "B" (or
bump "B" but not "A")?
A concrete example: If I make backwards incompatible changes to a package
whose latest version is 1.0.x, should the next version be 2.0.x or 1.1.x?
What sorts of things should I consider for choosing 2.0 over 1.1 and vice
versa?
Another question, by far most packages I have encountered either lead with
a 0 or a 1 for "A". Does that have some bearing on the long term stability
that package users should expect in the future?
Finally, if "1.0.x.." is meant to convey a level of long term support, does
"B" get rarely used? Since "C" version bumps to include backwards
compatible additions, and "D"+ for backwards compatible bug fixes. (I know
"D" isn't technically a PVP category, I'm just relating it to the patch
version of semver).
Thanks for your help!
-Zach
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141215/858c0f25/attachment.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 78, Issue 13
*****************************************
