Re: [Haskell-cafe] Combining State and List Monads

2012-08-25 Thread Edward Z. Yang
Ah, egg in my face, I appear to have misremembered how ListT is implemented ^_^
http://www.haskell.org/haskellwiki/ListT_done_right may be relevant.

Edward

Excerpts from Edward Z. Yang's message of Sat Aug 25 01:51:40 -0400 2012:
 Hello Henry,
 
 In such cases, it is often worth thinking about how you would implement
 such a scheme manually, without using pre-existing monads.  You will
 quickly see that the two candidate types:
 
 s - ([a], s)
 [s - (a, s)]
 
 both will not work (exercise: what semantics do they give?)  In fact,
 you must use continuation passing style, and you must resume the
 computation with the latest state value you would extracted from the
 last run.  See the LogicT monad for how to implement list-like monads in
 continuation passing style.
 
 Cheers,
 Edward
 
 Excerpts from Henry Laxen's message of Sat Aug 25 00:35:37 -0400 2012:
  Dear Cafe,
  
  It seems to me there should be some simple way of doing this, but thus
  far it eludes me.  I am trying to combine the State and List monads to
  do the following:
  
  countCalls = do
a - [1..2]
b - [1..2]
modify (+1)
return (a,b)
  
  
  where with some combination of ListT, StateT, List, State, or who
  knows what would result in:
  
  ([(1,1),(1,2),(2,1),(2,2)],4)
  
  assuming we initialize the state to 0
  
  Is there any way to make this happen?
  Thanks in advance.
  
  Henry Laxen
  

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Dealing poker hands, redux

2012-08-25 Thread Matthew
So I've finally got some code which shuffles a deck of cards and deals
out an arbitrary number of hands.

https://gist.github.com/19916435df2b116e0edc

type DealerState = State [Card] [[Card]]

deck :: [Card]
deck = [ (s, r) | s - suits, r - ranks ]

shuffleDeck :: Int - RVar [Card]
shuffleDeck n = shuffle $ concat $ replicate n deck

deal :: Int - ([[Card]] - DealerState)
deal n = \xs - state $ \s - (xs ++ [take n s], drop n s)

-- |Deal a number of hands a number of cards each.
dealHands :: Int - Int - ([[Card]] - DealerState)
dealHands hs cs = foldr1 (=) $ replicate hs (deal cs)

First of all, I have no idea if this is any good. The way I end up
calling dealHands and getting a real result is `runState (dealHands
3 7 []) deck`. And I see that I've got nested lambdas all in `deal`.
But hey it took me forever to figure it out and it works.

I'm using `shuffle` from Data.Random.Extras, which results in an RVar,
and thus the beginning of my perplexity. I'm happy to end up with RVar
inside a State monad, but I'm not sure where to start. To be honest,
I'm only barely understanding what I'm doing with the State monad as
it is. :)

Happy for any help whatsoever!

- Matthew

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] haskell cryptogaphic libraries

2012-08-25 Thread Vincent Hanquez

On 08/24/2012 04:20 PM, marcmo wrote:

You have done quite some work on the crypto front...cool!

since you are the owner of cryptocipher and your new package cipher-aes:
is cryptocipher now deprecated?


cryptocipher itself is not deprecated as it contains much more than just AES.
The haskell AES will probably going to be replaced by a stub layer to call into 
cipher-aes, and i'm also mulling splitting the package into many per-feature 
packages with cryptocipher binding them together, but it should affect any users.



the certificate library fits my needs perfectly!
snip
so let's just hope you stick around for some time Vince, my code now fully 
depends on you ;)


Well i have no plan to go anywhere and want to bring the tls stack to 
completion; although it's only on my free time for now..


--
Vincent

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Darcs fetches too little files

2012-08-25 Thread Henk-Jan van Tuyl

On Fri, 24 Aug 2012 23:14:05 +0200, Gwern Branwen gwe...@gmail.com wrote:

On Fri, Aug 24, 2012 at 4:47 PM, Henk-Jan van Tuyl hjgt...@chello.nl  
wrote:

I am trying to fetch wxHaskell with the command
  darcs get --lazy http://code.haskell.org/wxhaskell/
but there are much too little files downloaded; what could be the  
problem?


I'm working on Windows XP, both in an MS-DOS shell and an MSYS shell.
Installed Darcs version: 2.8.1


Could you be more specific? The point of --lazy *is* to fetch very few
files, so as described, it's working as it should...



I get the same files, with or without --lazy, they are:

wxhaskell_3dir /s/b
wxhaskell_3\darcs916
wxhaskell_3\darcs916-new_be8f187acbc53e7192167af035fde402
wxhaskell_3\_darcs
wxhaskell_3\_darcs\format
wxhaskell_3\_darcs\hashed_inventory
wxhaskell_3\_darcs\patches
wxhaskell_3\_darcs\prefs
wxhaskell_3\_darcs\pristine.hashed
wxhaskell_3\_darcs\prefs\binaries
wxhaskell_3\_darcs\prefs\boring
wxhaskell_3\_darcs\prefs\defaultrepo
wxhaskell_3\_darcs\prefs\motd
wxhaskell_3\_darcs\prefs\repos
wxhaskell_3\_darcs\pristine.hashed\e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855

Regards,
Henk-Jan van Tuyl


--
http://Van.Tuyl.eu/
http://members.chello.nl/hjgtuyl/tourdemonad.html
Haskell programming
--

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Kristopher Micinski
On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar
ramana.ku...@cl.cam.ac.uk wrote:
 Dear Haskell Cafe

 I'm looking for information on past and current attempts to write semantics
 for Haskell.
 Features I'm particularly interested in are:

 formal
 mechanised
 maintainable
 up to date

 Of course, if nothing like that exists then partial attempts towards it
 could still be useful.

 My ultimate aims include:

 Make it viable to define Haskell formally (i.e. so mechanised semantics can
 take over the normative role of the Haskell reports).
 Write a verified (or verify an existing) Haskell compiler (where verified
 means semantics preserving).

 Cheers,
 Ramana


Ramana,

If you look through the Haskell reports, you'll see that the language
is typically explained by its desugaring to a core language which
has the semantics you'd expect, in the sense that it's a call by
need abstract machine implemented by means of graph reduction in form
of the STG machine.

Thus, you typically want to think about the semantics of core
Haskell, in which you might try understanding the semantics of the
STG machine.

You can certainly look at the classic article [1] that describes the
behavior, at a high level.  You might ask whether the high level
description of the STG machine really makes sense, at which point
I'd direct you to a number of other articles (the one that sticks in
my memory, but I haven't really read deeply, is [2]).

It sounds, however, that you are looking for a more full description
of the language's semantics in a formal manner, going from real
Haskell to core Haskell, I feel such a reduction must surely exist but
I'm not sure I can recall one.

If you were to write a verified compiler, you would need a semantics
for the STG machine and show that it obeyed the rules you'd expect (a
call by name semantics), and then compose your proof for that with
your reduction of real Haskell to core Haskell..

kris

[1] Implementing lazy functional languages on stock hardware: the
Spineless Tagless G-machine, Simon L. Peyton Jones,
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729
[2] The Spineless Tagless G-machine, naturally, Jon Mountjoy,
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.8726

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Dealing poker hands, redux

2012-08-25 Thread Paolino
hello matthew,

I commented your gist on github adding the missing pieces with minor fixes.

Anyway, I suggest giving up RVar's which are overkill for your task. You
could implement your shuffle as an exercise, or use random-shuffle package
as I do in the code below.

Also I'd avoid State monad for such a simple task of remembering the
remaining deck after each deal.  You should switch to using a monad after
you are comfortable with pure code.


import Control.Arrow
import System.Random.Shuffle
import Control.Monad.Random.Class

-- |Cards.
data Suit = Hearts | Diamonds | Clubs | Spades deriving (Enum, Bounded,
Show)

data Rank = Ace | Two | Three | Four | Five | Six | Seven | Eight | Nine |
Ten | Jack | Queen | King deriving (Enum, Bounded, Show)

data Card = Flat Rank Suit | Jolly deriving Show

type Deck = [Card]
type Hand = [Card]

deck :: Deck
deck = [ Flat s r | s - [minBound .. maxBound] , r - [minBound ..
maxBound]]++ [Jolly,Jolly]

-- deal n cards m times from the given deck and return the rest along the
hands
dealHands :: Int - Int - Deck - ([Hand],Deck)
dealHands n m  = (map (take n) *** head) . splitAt m . iterate (drop n)

-- same as dealHands, but shuffle the deck before
randomDealHands :: (Functor m, MonadRandom m) = Int - Int - Deck - m
([Hand],Deck)
randomDealHands n m xs = dealHands n m `fmap` shuffleM xs

test :: IO ([Hand],Deck)
test = randomDealHands 5 4 $ deck ++ deck

You can run randomDealHands in IO (ghci prompt) as IO is both a Functor and
a MonadRandom instance

regards
paolino
2012/8/25 Matthew wonderzom...@gmail.com

 So I've finally got some code which shuffles a deck of cards and deals
 out an arbitrary number of hands.

 https://gist.github.com/19916435df2b116e0edc

 type DealerState = State [Card] [[Card]]

 deck :: [Card]
 deck = [ (s, r) | s - suits, r - ranks ]

 shuffleDeck :: Int - RVar [Card]
 shuffleDeck n = shuffle $ concat $ replicate n deck

 deal :: Int - ([[Card]] - DealerState)
 deal n = \xs - state $ \s - (xs ++ [take n s], drop n s)

 -- |Deal a number of hands a number of cards each.
 dealHands :: Int - Int - ([[Card]] - DealerState)
 dealHands hs cs = foldr1 (=) $ replicate hs (deal cs)

 First of all, I have no idea if this is any good. The way I end up
 calling dealHands and getting a real result is `runState (dealHands
 3 7 []) deck`. And I see that I've got nested lambdas all in `deal`.
 But hey it took me forever to figure it out and it works.

 I'm using `shuffle` from Data.Random.Extras, which results in an RVar,
 and thus the beginning of my perplexity. I'm happy to end up with RVar
 inside a State monad, but I'm not sure where to start. To be honest,
 I'm only barely understanding what I'm doing with the State monad as
 it is. :)

 Happy for any help whatsoever!

 - Matthew

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Gershom Bazerman

On 8/25/12 6:48 AM, Kristopher Micinski wrote:

Thus, you typically want to think about the semantics of core
Haskell, in which you might try understanding the semantics of the
STG machine.



Along those lines, there's Pirog and Biernacki's A Systematic 
Derivation of the STG Machine

Verified in Coq: http://www.cs.ox.ac.uk/files/3858/pirog-biernacki-hs10.pdf

Googling for that to find the pdf also led me to this page of the 
Haskell Wiki, which has some good resources, but is, I'm sure, 
incomplete: 
http://www.haskell.org/haskellwiki/Language_and_library_specification


Perhaps as material is assembled on the state of Haskell semantics, it 
can be added there as well to help others in the future.


Cheers,
Gershom

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Kristopher Micinski
On Sat, Aug 25, 2012 at 9:33 AM, Gershom Bazerman gersh...@gmail.com wrote:
 On 8/25/12 6:48 AM, Kristopher Micinski wrote:

 Thus, you typically want to think about the semantics of core
 Haskell, in which you might try understanding the semantics of the
 STG machine.


 Along those lines, there's Pirog and Biernacki's A Systematic Derivation of
 the STG Machine
 Verified in Coq: http://www.cs.ox.ac.uk/files/3858/pirog-biernacki-hs10.pdf

 Googling for that to find the pdf also led me to this page of the Haskell
 Wiki, which has some good resources, but is, I'm sure, incomplete:
 http://www.haskell.org/haskellwiki/Language_and_library_specification

 Perhaps as material is assembled on the state of Haskell semantics, it can
 be added there as well to help others in the future.


Thanks for the pointers, Gershom, it seems reasonable that such a
thing would exist, but I hadn't been aware of it,

kris

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Aaron Tomb
Hi,

Last summer, as part of the Summer of Code, David Lazar formalized a
significant portion of Haskell 98 in the K framework. You can find the
code here:

https://github.com/davidlazar/haskell-semantics

And there's a talk about it here:


http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskell-98-in-the-k-semantic.html

I think David is working from essentially the same goals you have in mind.

Aaron

On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote:
 Dear Haskell Cafe

 I'm looking for information on past and current attempts to write semantics
 for Haskell.
 Features I'm particularly interested in are:

 formal
 mechanised
 maintainable
 up to date

 Of course, if nothing like that exists then partial attempts towards it
 could still be useful.

 My ultimate aims include:

 Make it viable to define Haskell formally (i.e. so mechanised semantics can
 take over the normative role of the Haskell reports).
 Write a verified (or verify an existing) Haskell compiler (where verified
 means semantics preserving).

 Cheers,
 Ramana


 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Jay Sulzberger



On Sat, 25 Aug 2012, Kristopher Micinski krismicin...@gmail.com wrote:


On Thu, Aug 23, 2012 at 12:23 PM, Ramana Kumar
ramana.ku...@cl.cam.ac.uk wrote:

Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics
for Haskell.
Features I'm particularly interested in are:

formal
mechanised
maintainable
up to date

Of course, if nothing like that exists then partial attempts towards it
could still be useful.

My ultimate aims include:

Make it viable to define Haskell formally (i.e. so mechanised semantics can
take over the normative role of the Haskell reports).
Write a verified (or verify an existing) Haskell compiler (where verified
means semantics preserving).

Cheers,
Ramana



Ramana,

If you look through the Haskell reports, you'll see that the language
is typically explained by its desugaring to a core language which
has the semantics you'd expect, in the sense that it's a call by
need abstract machine implemented by means of graph reduction in form
of the STG machine.

Thus, you typically want to think about the semantics of core
Haskell, in which you might try understanding the semantics of the
STG machine.

You can certainly look at the classic article [1] that describes the
behavior, at a high level.  You might ask whether the high level
description of the STG machine really makes sense, at which point
I'd direct you to a number of other articles (the one that sticks in
my memory, but I haven't really read deeply, is [2]).

It sounds, however, that you are looking for a more full description
of the language's semantics in a formal manner, going from real
Haskell to core Haskell, I feel such a reduction must surely exist but
I'm not sure I can recall one.

If you were to write a verified compiler, you would need a semantics
for the STG machine and show that it obeyed the rules you'd expect (a
call by name semantics), and then compose your proof for that with
your reduction of real Haskell to core Haskell..

kris

[1] Implementing lazy functional languages on stock hardware: the
Spineless Tagless G-machine, Simon L. Peyton Jones,
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729
[2] The Spineless Tagless G-machine, naturally, Jon Mountjoy,
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.8726


I do not know Haskell.  It looks to me as though there are
several pieces of the mechanism:

1. There is, once the extensions are specified, a particular Type
System, that is, a formal system with, on the syntactic side, at
least, assumptions, judgements, rules of inference, terms lying
in some lambda calculus, etc..

2. The Type Inference Subsystem, which using some constraint
solver calculates the type to be assigned to the value of Haskell
expressions.

3. The machine which does reduction, perhaps execution, on
the value of Haskell expressions.  This is, by your account, the
STG machine.

There is a textual version of Haskell's Core.  If it were
executable and the runtime were solid and very simple and clear
in its design, I think we would have something close to a formal
semantics.  We'd also require that the translation to STG code
be very simple.

I think I have now mostly just repeated what you said.

oo--JS.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Kristopher Micinski

 I do not know Haskell.  It looks to me as though there are
 several pieces of the mechanism:

 1. There is, once the extensions are specified, a particular Type
 System, that is, a formal system with, on the syntactic side, at
 least, assumptions, judgements, rules of inference, terms lying
 in some lambda calculus, etc..


That's right.  Extensions get complex too, however, and can't be
necessarily easily dismissed (not to imply you were doing so),
RankNTypes, for example,

 2. The Type Inference Subsystem, which using some constraint
 solver calculates the type to be assigned to the value of Haskell
 expressions.


Yes, that's right, for core haskell this is typically damas milner
(let bound) polymorphism

 3. The machine which does reduction, perhaps execution, on
 the value of Haskell expressions.  This is, by your account, the
 STG machine.


Yes, notably graph reduction allows sharing, which is an important
part of Haskell's semantics,

 There is a textual version of Haskell's Core.  If it were
 executable and the runtime were solid and very simple and clear
 in its design, I think we would have something close to a formal
 semantics.  We'd also require that the translation to STG code
 be very simple.


Yes, that's right.  The translation to STG (or something like it,
another core language) can be found in many books and articles,

But others here have also specified some good references for
executable versions of Core.  Still unsure if the translation from
Haskell to Core has been verified, I would suspect not, as I haven't
heard of any such thing.

kris

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Ramana Kumar
Thanks much Kristopher, Gershom, and Aaron, for the excellent pointers.
(Keep them coming, anyone else - maybe we can update the wiki..)
I will look into them in more detail soon.

On Sat, Aug 25, 2012 at 5:12 PM, Aaron Tomb aaront...@gmail.com wrote:

 Hi,

 Last summer, as part of the Summer of Code, David Lazar formalized a
 significant portion of Haskell 98 in the K framework. You can find the
 code here:

 https://github.com/davidlazar/haskell-semantics

 And there's a talk about it here:


 http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskell-98-in-the-k-semantic.html

 I think David is working from essentially the same goals you have in mind.

 Aaron

 On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar ramana.ku...@cl.cam.ac.uk
 wrote:
  Dear Haskell Cafe
 
  I'm looking for information on past and current attempts to write
 semantics
  for Haskell.
  Features I'm particularly interested in are:
 
  formal
  mechanised
  maintainable
  up to date
 
  Of course, if nothing like that exists then partial attempts towards it
  could still be useful.
 
  My ultimate aims include:
 
  Make it viable to define Haskell formally (i.e. so mechanised semantics
 can
  take over the normative role of the Haskell reports).
  Write a verified (or verify an existing) Haskell compiler (where verified
  means semantics preserving).
 
  Cheers,
  Ramana
 
 
  ___
  Haskell-Cafe mailing list
  Haskell-Cafe@haskell.org
  http://www.haskell.org/mailman/listinfo/haskell-cafe
 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Ramana Kumar
On Sat, Aug 25, 2012 at 8:17 PM, Kristopher Micinski krismicin...@gmail.com
 wrote:

 Still unsure if the translation from
 Haskell to Core has been verified, I would suspect not, as I haven't
 heard of any such thing.


If it is only Core that has semantics, then it wouldn't make sense to
verify the translation from Haskell to Core. Rather, the translation itself
would be the semantics of (sugared) Haskell.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Jay Sulzberger



On Sat, 25 Aug 2012, Kristopher Micinski krismicin...@gmail.com wrote:



I do not know Haskell.  It looks to me as though there are
several pieces of the mechanism:

1. There is, once the extensions are specified, a particular Type
System, that is, a formal system with, on the syntactic side, at
least, assumptions, judgements, rules of inference, terms lying
in some lambda calculus, etc..



That's right.  Extensions get complex too, however, and can't be
necessarily easily dismissed (not to imply you were doing so),
RankNTypes, for example,


I suspected that some of these extensions might cause Haskell
expressions to be hard to type.  One thing I am not clear on is
whether any standard extensions require modifications to
(internal) Core.




2. The Type Inference Subsystem, which using some constraint
solver calculates the type to be assigned to the value of Haskell
expressions.



Yes, that's right, for core haskell this is typically damas milner
(let bound) polymorphism


Ah, yes, thank you.  I almost believe in Hindley-Damas-Milner but
have not yet attempted the standard initiation course.




3. The machine which does reduction, perhaps execution, on
the value of Haskell expressions.  This is, by your account, the
STG machine.



Yes, notably graph reduction allows sharing, which is an important
part of Haskell's semantics,


Ah, thanks!




There is a textual version of Haskell's Core.  If it were
executable and the runtime were solid and very simple and clear
in its design, I think we would have something close to a formal
semantics.  We'd also require that the translation to STG code
be very simple.



Yes, that's right.  The translation to STG (or something like it,
another core language) can be found in many books and articles,


This is good.  I will look at the references given in this
thread.  The account at

  
http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/TypingHaskellInHaskell.html

is, I think, one part of what I was looking for.



But others here have also specified some good references for
executable versions of Core.  Still unsure if the translation from
Haskell to Core has been verified, I would suspect not, as I haven't
heard of any such thing.

kris


This part of the project I am less interested in, due to my fear,
I am an old Lisper, that the luxuriant syntactic undergrowth
might be hard to hack through.  If we had an executable Core,
which might have to be extended (after perhaps some subtraction)
with a simple notation for type annotations, and the rest of the
apparatus, I think this would be very useful.  Even though we
would not gain one of the claimed advantages of
rigor-all-the-way, that is, better bug suppression for ordinary
Haskell as she is spoke.

oo--JS.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Kristopher Micinski
On Sat, Aug 25, 2012 at 3:38 PM, Jay Sulzberger j...@panix.com wrote:
 This is good.  I will look at the references given in this
 thread.  The account at


 http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/TypingHaskellInHaskell.html

 is, I think, one part of what I was looking for.


The book I recommend (although now I feel like a bad person because I
haven't read all of it :-(.., is The Implementation of Functional
Languages,

http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/index.htm

I remember finding it quite approachable, although for the immediate
need of trying to implement *Haskell* in a verified environment, it
might not be immediately helpful, it's really good background reading
on the subject that will be imperative should you want to do such
things (and written around the time when Haskell was congealing, so
should be representative-ish of the attitudes underlying Haskell's
design at the time: graph reduction, compiling pattern matching,
translating high level lamda languages to core semantics).

kris

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] formal semantics

2012-08-25 Thread Jay Sulzberger



On Sat, 25 Aug 2012, Kristopher Micinski krismicin...@gmail.com wrote:


On Sat, Aug 25, 2012 at 3:38 PM, Jay Sulzberger j...@panix.com wrote:

This is good.  I will look at the references given in this
thread.  The account at


http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/TypingHaskellInHaskell.html

is, I think, one part of what I was looking for.



The book I recommend (although now I feel like a bad person because I
haven't read all of it :-(.., is The Implementation of Functional
Languages,

http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/index.htm

I remember finding it quite approachable, although for the immediate
need of trying to implement *Haskell* in a verified environment, it
might not be immediately helpful, it's really good background reading
on the subject that will be imperative should you want to do such
things (and written around the time when Haskell was congealing, so
should be representative-ish of the attitudes underlying Haskell's
design at the time: graph reduction, compiling pattern matching,
translating high level lamda languages to core semantics).

kris


I have read the book to page 12.  So far I am swimming in waters
known to me.  I think you are right: It looks to be slow and
careful, and thus just right for me.

oo--JS.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] ANN: Monad.Reader Issue 20

2012-08-25 Thread Edward Z. Yang
*It’s not dead, it’s resting!*

I am pleased to announce that Issue 20 of the Monad Reader is now available.

http://themonadreader.files.wordpress.com/2012/08/issue20.pdf

Issue 20 consists of the following three articles:

- Enumeration of Tuples with Hyperplanes by Tillmann Vogt
- Understanding Basic Haskell Error Messages by Jan Stolarek
- The MapReduce type of a Monad by Julian Porter

Feel free to browse the source files. You can check out the entire repository 
using Git:

git clone https://github.com/ezyang/tmr-issue20.git

If you’d like to write something for Issue 21, please get in touch!

Cheers,
Edward

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] When is a composition of catamorphisms a catamorphism?

2012-08-25 Thread wren ng thornton

On 8/24/12 3:44 AM, Sebastien Zany wrote:

More specifically (assuming I understood the statement correctly):

Suppose I have two base functors F1 and F2 and folds for each: fold1 :: (F1
a - a) - (μF1 - a) and fold2 :: (F2 a - a) - (μF2 - a).

Now suppose I have two algebras f :: F1 μF2 - μF2 and g :: F2 A - A.

When is the composition (fold2 g) . (fold1 f) :: μF1 - A a catamorphism?


From http://comonad.com/haskell/catamorphisms.html we have the law:

Given
F, a functor
G, a functor
e, a natural transformation from F to G
(i.e., e :: forall a. F a - G a)
g, a G-algebra
(i.e., f :: G X - X, for some fixed X)

it follows that

cata g . cata (In . e) = cata (g . e)

The proof of which is easy. So it's sufficient to be a catamorphism if 
your f = In . e for some e. I don't recall off-hand whether that's 
necessary, though it seems likely


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe