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: Deploying a haskell application (not a webapp)
(Mateusz Kowalczyk)
2. Re: Deploying a haskell application (not a webapp) (Alan Buxton)
3. Re: Deploying a haskell application (not a webapp)
(Michael Orlitzky)
4. Anyone here self-studying upenn's CIS 552 taught by Benjamin
Pierce (chao chu)
5. Re: Anyone here self-studying upenn's CIS 552 taught by
Benjamin Pierce (Nadir Sampaoli)
6. Re: Anyone here self-studying upenn's CIS 552 taught by
Benjamin Pierce (Dimitri DeFigueiredo)
7. Re: structural induction, two lists, simultaneous (Pascal Knodel)
----------------------------------------------------------------------
Message: 1
Date: Wed, 17 Dec 2014 14:16:54 +0000
From: Mateusz Kowalczyk <[email protected]>
To: [email protected]
Subject: Re: [Haskell-beginners] Deploying a haskell application (not
a webapp)
Message-ID: <[email protected]>
Content-Type: text/plain; charset=windows-1252
On 12/16/2014 03:24 PM, Michael Orlitzky wrote:
> On 12/16/2014 08:47 AM, Alan Buxton wrote:
>> Hiya
>>
>>
>>
>> It turned out that my issue was to do with the data files. When
>> compiling locally, cabal puts the files in /home/alan/.cabal/share and
>> the compiled application expects to find the files there. So when I
>> deploy my binary I have to also put some files into
>> /home/alan/.cabal/share which feels wrong.
>
> If you list the data files in Cabal's "data-files" field, and you use
> Cabal to build on the server, then you can ask Cabal where it put those
> files at runtime:
>
> https://www.haskell.org/cabal/users-guide/developing-packages.html#accessing-data-files-from-package-code
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
Pretty sure the whole point of this thread is that the OP does not want
to build on the server.
Personally I have inlined some data files into the source directly at
compile time with Template Haskell: no hassle at run-time about finding
the files, no hassle with copying them over to the target machine? Of
course this might not cut it if your files are huge or are meant to be
more dynamic. If that's the case then you should copy the data files
along with the binary and teach your program how to find them.
--
Mateusz K.
------------------------------
Message: 2
Date: Wed, 17 Dec 2014 14:24:38 +0000
From: Alan Buxton <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Deploying a haskell application (not
a webapp)
Message-ID:
<CAJCr4=4CNHv-YkpuFg14c=greephtahmnxrqxgdqm39pjdt...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi mateusz yes thanks for this. You've basically hit the nail on the head
with that summary "teach your program how to find them".
On 17 Dec 2014 14:17, "Mateusz Kowalczyk" <[email protected]> wrote:
> On 12/16/2014 03:24 PM, Michael Orlitzky wrote:
> > On 12/16/2014 08:47 AM, Alan Buxton wrote:
> >> Hiya
> >>
> >>
> >>
> >> It turned out that my issue was to do with the data files. When
> >> compiling locally, cabal puts the files in /home/alan/.cabal/share and
> >> the compiled application expects to find the files there. So when I
> >> deploy my binary I have to also put some files into
> >> /home/alan/.cabal/share which feels wrong.
> >
> > If you list the data files in Cabal's "data-files" field, and you use
> > Cabal to build on the server, then you can ask Cabal where it put those
> > files at runtime:
> >
> >
> https://www.haskell.org/cabal/users-guide/developing-packages.html#accessing-data-files-from-package-code
> >
> > _______________________________________________
> > Beginners mailing list
> > [email protected]
> > http://www.haskell.org/mailman/listinfo/beginners
> >
>
> Pretty sure the whole point of this thread is that the OP does not want
> to build on the server.
>
> Personally I have inlined some data files into the source directly at
> compile time with Template Haskell: no hassle at run-time about finding
> the files, no hassle with copying them over to the target machine? Of
> course this might not cut it if your files are huge or are meant to be
> more dynamic. If that's the case then you should copy the data files
> along with the binary and teach your program how to find them.
>
> --
> Mateusz K.
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141217/522bb6ee/attachment-0001.html>
------------------------------
Message: 3
Date: Wed, 17 Dec 2014 12:52:56 -0500
From: Michael Orlitzky <[email protected]>
To: [email protected]
Subject: Re: [Haskell-beginners] Deploying a haskell application (not
a webapp)
Message-ID: <[email protected]>
Content-Type: text/plain; charset=UTF-8
On 12/17/2014 09:16 AM, Mateusz Kowalczyk wrote:
>
> Pretty sure the whole point of this thread is that the OP does not want
> to build on the server.
>
Oh, sorry, I missed that. You can pass --datadir to Cabal's configure
step; e.g.
$ runghc Setup.hs configure --datadir=/usr/local/share/<your-app>
I believe it's using /home/alan/.cabal/share as the default, but if you
tell it to do otherwise, it will.
------------------------------
Message: 4
Date: Thu, 18 Dec 2014 01:55:33 +0800
From: chao chu <[email protected]>
To: [email protected]
Subject: [Haskell-beginners] Anyone here self-studying upenn's CIS 552
taught by Benjamin Pierce
Message-ID:
<caarvkb-q-cjf4j4sn74cu97pblrgmsx3afq_n2bk_es-msv...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi,
The course website: http://www.seas.upenn.edu/~cis552/
I found the lecture and lab materials are very good and I am self-studying
the course by reading the lecture notes and doing the labs on my own.
Just want to check if anyone is also following the course so that we can
form a study group to discuss whatever we want about the course and also
about learning haskell.
Thanks & Regards,
--
ChuChao
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141218/f7d3996e/attachment-0001.html>
------------------------------
Message: 5
Date: Wed, 17 Dec 2014 19:35:49 +0100
From: Nadir Sampaoli <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Anyone here self-studying upenn's CIS
552 taught by Benjamin Pierce
Message-ID:
<cafywtdqeotm__pyojvumww0smnbp+923oj4yz48drfmyuue...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
17/dec/2014 18:56 "chao chu" <[email protected]>
>
> Hi,
>
> The course website: http://www.seas.upenn.edu/~cis552/
>
> I found the lecture and lab materials are very good and I am
self-studying the course by reading the lecture notes and doing the labs on
my own.
>
> Just want to check if anyone is also following the course so that we can
form a study group to discuss whatever we want about the course and also
about learning haskell.
>
It would be great. I bookmarked it few months ago but never came around
starting it. I like the idea and would definitely benefit from other people
following along.
Last year I did cis194 and compared solutions week-by-week with another
person I met on IRC but somehow stopped at about 2 thirds.
Are you already much further into the course?
Side note about cis194: mr Pierce asked us to avoid publishing the
solutions so we set up private repos at bitbucket.
--
Nadir
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141217/e2894d8d/attachment-0001.html>
------------------------------
Message: 6
Date: Wed, 17 Dec 2014 17:11:47 -0200
From: Dimitri DeFigueiredo <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Anyone here self-studying upenn's CIS
552 taught by Benjamin Pierce
Message-ID: <[email protected]>
Content-Type: text/plain; charset="windows-1252"; Format="flowed"
Hi ChuChao,
I am going thru the lectures at a very slow pace (have other
commitments). I'm currently at Monad Transformers, but would like/be
willing to discuss the material. I think the class is *very good*, but
there are one or two lectures which should be avoided.
cheers,
Dimitri
On 17/12/14 15:55, chao chu wrote:
> Hi,
>
> The course website: http://www.seas.upenn.edu/~cis552/
> <http://www.seas.upenn.edu/%7Ecis552/>
>
> I found the lecture and lab materials are very good and I am
> self-studying the course by reading the lecture notes and doing the
> labs on my own.
>
> Just want to check if anyone is also following the course so that we
> can form a study group to discuss whatever we want about the course
> and also about learning haskell.
>
> Thanks & Regards,
>
> --
> ChuChao
>
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141217/2cedfc54/attachment-0001.html>
------------------------------
Message: 7
Date: Thu, 18 Dec 2014 07:58:48 +0100
From: Pascal Knodel <[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: <[email protected]>
Content-Type: text/plain; charset="utf-8"; Format="flowed"
> (? 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
Thank you, Rustom Mody, that's it, reordering of universal quantifiers.
By the way, I'm searching for a 'good' book about predicate logic for
quite some time now.
One with a strong link to mathematics and the quantification style
that is used there would be nice. By chance, is there a reference
(script/paper/book )
you would recommend?
I have rewritten my first proof a little. It mentions the other
variables now explicitly.
This way it should be cleaner:
-- 1. Induction Hypothesis (1. I.H.):
-- ----------------------------------
--
-- For an arbitrary but fixed list "ys", for all lists "zs" and for
all functions f the statement ...
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
-- ... holds.
When proving the proposition the first time I've used a different approach
(the chapter heavily promoted generalization and because I tried to get
around
the dilemma that I wasn't sure if I understood 'simultaneous induction'
correctly):
-- ---------------
-- 1. Proposition:
-- ---------------
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
--
--
-- Proof By Generalization:
-- ------------------------
--
--
-- ------------------------------
-- 1. Specialization Proposition:
-- ------------------------------
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
--
-- ------------------------------
-- 1. Generalization Proposition:
-- ------------------------------
--
-- map f (foldr (++) [] ls) = foldr ( (++) . (f `map`) ) [] ls
--
--
-- Proof By Structural Induction:
-- ------------------------------
--
--
-- 1. Induction Beginning (1. I.B.):
-- ---------------------------------
--
--
-- (Base case 1.) :<=> ls := []
--
-- => (left) := map f (foldr (++) [] ls)
-- | (Base case 1.)
-- = map f (foldr (++) [] [])
-- | foldr
-- = map f []
-- | map
-- = []
--
--
-- (right) := foldr ( (++) . (f `map`) ) [] ls
-- | (Base case 1.)
-- = foldr ( (++) . (f `map`) ) [] []
-- | foldr
-- = []
--
--
-- => (left) = (right)
--
-- ?
--
--
-- 1. Induction Hypothesis (1. I.H.):
-- ----------------------------------
--
-- For an arbitrary but fixed (list-of-)lists "ls" and ? functions f,
the statement ...
--
-- map f ( foldr (++) [] ls ) = foldr ( (++) . (f `map`) ) [] ls
--
-- ... holds.
--
--
-- 1. Induction Step (1. I.S.):
-- ----------------------------
--
--
-- (left) := map f ( foldr (++) [] (l : ls) )
-- | foldr
-- = map f ( l ++ foldr (++) [] ls )
-- | (Specialized 1. I.H.)
-- = map f l ++ map f ( foldr (++) [] ls )
-- | (1. I.H.)
-- = map f l ++ ( foldr ( (++) . (f `map`) ) [] ls )
--
--
-- (right) := foldr ( (++) . (f `map`) ) [] (l : ls)
-- | foldr
-- = ( (++) . (f `map`) ) l foldr ( (++) . (f `map`) ) [] ls
-- | General rule of function application (left associativity)
-- = ( ( (++) . (f `map`) ) l ) foldr ( (++) . (f `map`)
) [] ls
-- | (.)
-- = ( (++) ( (f `map`) l ) ) foldr ( (++) . (f `map`) )
[] ls
-- | (f `map`)
-- = ( (++) (map f l) ) foldr ( (++) . (f `map`) ) [] ls
-- | General rule of function application (left associativity)
-- = (++) (map f l) ( foldr ( (++) . (f `map`) ) [] ls )
-- | ++
-- = map f l ++ ( foldr ( (++) . (f `map`) ) [] ls )
--
--
-- => (left) = (right)
--
--
-- ??? (1. Generalization Proof)
--
--
-- (Generalization)
--
-- :<=> map f ( foldr (++) [] ls ) = foldr ( (++) . (f `map`) ) [] ls
-- | ls := [ys , zs]
-- |=> map f ( foldr (++) [] [ys , zs] ) = foldr ( (++) . (f
`map`) ) [] [ys , zs]
--
-- <=> map f (ys ++ zs) = map f ys ++ map f zs
--
-- <=>: (Specialization)
--
--
-- ? (1. Specialization Proof)
Is this also possible? Is it allowed to use a specialized induction
hypothesis like that ( see '| (Specialized 1. I.H.)' above )?
Pascal
>
>
> On Mon, Dec 15, 2014 at 7:12 AM, Pascal Knodel <[email protected]
> <mailto:[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] <mailto:[email protected]>
> http://www.haskell.org/mailman/listinfo/beginners
>
>
>
> --
> http://www.the-magus.in
> http://blog.languager.org
>
>
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20141218/7f5d3572/attachment.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 78, Issue 16
*****************************************
