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: making translation from imperative code (Magnus Therning)
2. Re: making translation from imperative code (Heinrich Apfelmus)
3. Basic Parsec question (Zachary Turner)
4. Re: Basic Parsec question (Antoine Latter)
5. Re: Basic Parsec question (Zachary Turner)
6. Re: Re: making translation from imperative code (Michael Mossey)
7. Re: [Haskell-cafe] abou the Godel Numbering for untyped
lambda calculus (Dan Weston)
----------------------------------------------------------------------
Message: 1
Date: Tue, 31 Mar 2009 14:04:09 +0100
From: Magnus Therning <[email protected]>
Subject: Re: [Haskell-beginners] making translation from imperative
code
To: Michael Mossey <[email protected]>
Cc: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset=UTF-8
On Tue, Mar 31, 2009 at 1:54 PM, Michael Mossey <[email protected]> wrote:
> I'm translating a Python program into Haskell, and running into a
> problem---a type of code where I don't know how to make the conceptual
> shift.
>
> The Python code does a graphical layout of a music score. There is a loop in
> which it add items (chords, symbols, text, etc.) one at a time, moving to
> the right, until it reaches the end of the line. So in typical imperative
> code, we have a bunch of loop state, such as
>
> Â - xpos of last chord or symbol placed
> Â - time of last chord or symbol placed
> Â - several StaffData objects, each containing the symbols that went
> Â Â on that particular staff
> Â - a cache of miscellaneous information about each symbol for later
> Â Â reference
>
> So imperative code is pretty simple: loop, and each time update the state.
> Much of this state consists of lists  to which symbols are added once per
> loop.
>
> I'm not sure how to conceive of this problem in Haskell. Without using
> mutable variables, I would have to "rebuild" the state on each loop. I can
> do that, but I don't want to see an ugly proliferation of variables.
>
> I would like to encapsulate the state in a single object so I can pass it
> around as a single variable, like
>
> LoopState = LoopState {
> Â Â lastXPos :: Int,
> Â Â lastTime :: Double,
> Â Â staffDataLists :: [ ( String, StaffData ) ],
> Â Â chunkCache :: [ ( Double, Chunk ) ]
> Â Â }
>
> So lets say I have an instance of this call x. Let's say I want to create y,
> by "updating" lastXPos. Do I have to do something like this:
>
> newLastXPos = 25
> y = LoopState ( newLastXPos, lastTime x, staffDataLists x,
> Â Â Â Â Â Â Â Â chunkCache x )
>
> Obviously this is verbose compared to an imperative language in which one
> would say:
> newLastPos = 25
> x.setLastXPos( newLastXPos )
>
> I am aware that Haskell provides some mutable structures, but part of what
> drew me to Haskell was the benefit of avoiding mutable data (reducing bugs
> and making it easier to reason about my program's behavior). Are there any
> shortcuts for doing things like the above?
Have you considered the sort of named updates like the following?
data Foo = Foo { i :: Int, j :: Int } deriving (Show)
Loading that into ghci you can do things like this:
*Foo> let f = Foo 25 25
*Foo> f
Foo {i = 25, j = 25}
*Foo> f { i = 35 }
Foo {i = 35, j = 25}
That might be more to your liking.
/M
--
Magnus Therning (OpenPGP: 0xAB4DFBA4)
magnusï¼ therningï¼org Jabber: magnusï¼ therningï¼org
http://therning.org/magnus identi.ca|twitter: magthe
------------------------------
Message: 2
Date: Wed, 01 Apr 2009 04:20:28 +0200
From: Heinrich Apfelmus <[email protected]>
Subject: [Haskell-beginners] Re: making translation from imperative
code
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1
Michael Mossey wrote:
> I'm translating a Python program into Haskell, and running into a
> problem---a type of code where I don't know how to make the conceptual
> shift.
>
> The Python code does a graphical layout of a music score. There is a
> loop in which it add items (chords, symbols, text, etc.) one at a time,
> moving to the right, until it reaches the end of the line. So in typical
> imperative code, we have a bunch of loop state, such as
>
> - xpos of last chord or symbol placed
> - time of last chord or symbol placed
> - several StaffData objects, each containing the symbols that went
> on that particular staff
> - a cache of miscellaneous information about each symbol for later
> reference
>
> So imperative code is pretty simple: loop, and each time update the
> state. Much of this state consists of lists to which symbols are added
> once per loop.
Can you elaborate on what exactly the algorithm is doing? Does it just
emit notes/chords/symbols at given positions or does it also try to
arrange them nicely? And most importantly, "where" does it emit them to,
i.e. what's the resulting data structure?
So far, the problem looks like a basic fold to me.
Regards,
apfelmus
--
http://apfelmus.nfshost.com
------------------------------
Message: 3
Date: Tue, 31 Mar 2009 23:16:57 -0500
From: Zachary Turner <[email protected]>
Subject: [Haskell-beginners] Basic Parsec question
To: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
Hi,
I downloaded the package lispparser to, well, parse lisp code. I really
have absolutely no idea what I'm doing though. I can look at the source of
the module and see that it's exporting a single data type called LispVal and
a single function called parseExpr, so somehow I should be able to pass an
arbitrary block of lisp code into this function and get back a LispVal. But
for the life of me I can't figure out how. I've looked at the documentation
but I get even more confused because it links me to the Parsec documentation
which is probably way over my head. Basically I just want a simple
function:
parse :: String -> LispVal
parse expr = ???
presumably by making some use of the exported 'thing' (since I'm not really
sure how to interpret its type)
parseExpr :: Parser LispVal
Thanks for any help
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20090331/3f884cb0/attachment-0001.htm
------------------------------
Message: 4
Date: Tue, 31 Mar 2009 23:34:16 -0500
From: Antoine Latter <[email protected]>
Subject: Re: [Haskell-beginners] Basic Parsec question
To: Zachary Turner <[email protected]>
Cc: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset=ISO-8859-1
2009/3/31 Zachary Turner <[email protected]>:
> Hi,
>
> I downloaded the package lispparser to, well, parse lisp code. I really
> have absolutely no idea what I'm doing though. I can look at the source of
> the module and see that it's exporting a single data type called LispVal and
> a single function called parseExpr, so somehow I should be able to pass an
> arbitrary block of lisp code into this function and get back a LispVal. But
> for the life of me I can't figure out how. I've looked at the documentation
> but I get even more confused because it links me to the Parsec documentation
> which is probably way over my head. Basically I just want a simple
> function:
>
> parse :: String -> LispVal
> parse expr = ???
>
> presumably by making some use of the exported 'thing' (since I'm not really
> sure how to interpret its type)
>
> parseExpr :: Parser LispVal
>
> Thanks for any help
>
You should be able to use the function "parse" from the parsec package like so:
> parse parseExp "name of source for error reporting" "(some lisp expression")
The function "parse" returns a value of type (Either ParseError a),
where in this case the type-var 'a' wil be a LispVal.
Does that help?
Antoine
------------------------------
Message: 5
Date: Wed, 1 Apr 2009 00:50:59 -0500
From: Zachary Turner <[email protected]>
Subject: Re: [Haskell-beginners] Basic Parsec question
To: Antoine Latter <[email protected]>
Cc: [email protected]
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
On Tue, Mar 31, 2009 at 11:34 PM, Antoine Latter <[email protected]> wrote:
> You should be able to use the function "parse" from the parsec package like
> so:
>
> > parse parseExp "name of source for error reporting" "(some lisp
> expression")
>
> The function "parse" returns a value of type (Either ParseError a),
> where in this case the type-var 'a' wil be a LispVal.
>
> Does that help?
>
That was perfect, thanks.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20090401/215831d0/attachment-0001.htm
------------------------------
Message: 6
Date: Tue, 31 Mar 2009 23:33:27 -0700
From: Michael Mossey <[email protected]>
Subject: Re: [Haskell-beginners] Re: making translation from
imperative code
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Heinrich Apfelmus wrote:
> Michael Mossey wrote:
>> I'm translating a Python program into Haskell, and running into a
>> problem---a type of code where I don't know how to make the conceptual
...
>
> Can you elaborate on what exactly the algorithm is doing? Does it just
> emit notes/chords/symbols at given positions or does it also try to
> arrange them nicely? And most importantly, "where" does it emit them to,
> i.e. what's the resulting data structure?
>
> So far, the problem looks like a basic fold to me.
Here is some Haskell code that explains the problem in
more detail.
-------------------------------------------------------------
-------------------------------------------------------------
-- layoutSystem
--------------------------------------------------------------
--------------------------------------------------------------
-- A "system" in musical typesetting terminology is a
-- collection of staves that are all played simultaneously;
-- that is, they are aligned in time and space. This is a
-- simple layout algorithm that uses the concept of
-- "chunk"--- a chunk is a set of events (notes, dynamic
-- changes, etc.) that occur on a subset of the staves, and
-- occur at the same time and therefore need to be aligned
-- vertically. Each item has a width and items must be
-- placed so they don't overlap. (There is no attempt to
-- align them in an aesthetically pleasing way; they simply
-- must not collide.)
--
-- We presume that something called a "score" exists, which
-- is an object representing the underlying music data, from
-- which can be extracted a list of chunks, each
-- associated with the time at which it is played. We
-- don't show the structure of a score here; we just
-- assume that we can operate on a score via two
-- functions:
--
-- A function to grab a chunk:
-- scoreGetChunkData :: Score -> Time -> ChunkData
-- A function to get time of next chunk:
-- scoreNextTime :: Score -> Time -> Time
--
-- This basic structure of this algorithm is a loop with state.
-- Here's the state.
-- 'time' :: Double -- is the time of next chunk to layout.
-- 'staffLayouts' :: [( String, StaffLayout)] -- is an
-- association list of staff names and StaffLayout
-- objects. Each StaffLayout object accumulates the chunks
-- that belong to that staff.
-- 'val' :: Int -- This is the next x-position that is
-- available for placing a new chunk (this
-- is an abbreviation for vertical
-- alignment line).
-- 'chunkDataMem' This is a cache or memory of all chunks
-- we have encountered in this system, for
-- lookup later.
data SystemLayoutState = SystemLayoutState
{ time :: Double,
staffLayouts :: [ ( String, StaffLayout ) ],
val :: Int,
chunkDataMem :: [ ChunkData ]
}
layoutSystem Double -> Score -> Int -> Config -> SystemLayoutState
layoutSystem firstTime score rightBorder config =
-- Work is done by helper function layoutSystem',
-- after giving it the initial state.
layoutSystem' initialState
-- Construct initial state.
where initialState = SystemLayoutState
{ time = firstTime,
staffLayouts = [],
val = getConfig config "prefixWidth",
storedChunkData = [] }
-- Define the helper function layoutSystem'
layoutSystem' :: SystemLayoutState -> SystemLayoutState
layoutSystem' state =
-- Get ChunkData from the score at the time
-- associated with the current state.
let chunkData = scoreGetChunkData score (time state)
-- Call 'incorporateChunkData' to try to add
-- it to the score. This will return a
-- tuple, the first member being the status
-- (True means we can add no more chunks
-- because we ran out of horizontal space)
-- and the second is updated state.
case
incorporateChunkData state chunkData rightBorder
of
( True, state' ) -> state'
( False, state' ) -> tryAgain state'
-- We separate the definition of tryAgain just to make
-- the structure of this whole function a little
-- clearer. tryAgain asks the score for the next
-- time at which a chunk exists. In the case there
-- *are no more* chunks, it terminates the
-- recursion, while also modifying the state in
-- some way to communicate that the recursion
-- terminated *because of running out of chunks*
-- instead of running out of horizontal
-- space. Otherwise it calls back to layoutSystem'.
tryAgain state =
case scoreNextTime score (time state) of
-1 -> indicateNoMoreChunks state
t -> layoutSystem' (setTime state t)
------------------------------
Message: 7
Date: Tue, 31 Mar 2009 12:48:23 -0700
From: Dan Weston <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] abou the Godel
Numbering for untyped lambda calculus
To: Algebras Math <[email protected]>
Cc: beginners <[email protected]>, "[email protected]"
<[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="ISO-8859-1"; format=flowed
DISCLAIMER: The last I studied this was over 20 years ago, so my brain
is seriously rusty. You are warned...
> you mean the godel function (denoted by # and generally will be in type,
> #:term -> number ?) is a kind of functions instead of a particular
> function?
No. The Godel mirror function (as defined by Godel) is a single
function, the product of primes (whose ordering gives the position in
the string) with exponents (giving the symbol at that position).
However, I think any total injective function with partial injective
inverse will do. Don't get hung up on the details of the mirroring
(Godel doesn't). Once you accept that it can be done, there is no need
to actually do it.
There is nothing magic about integers, beyond the fact that elementary
arithmetic is "well understood" by humans and should not have
inconsistencies (it probably doesn't, but we can't prove it within any
language more intuitive than arithmetic, so why should be believe the
proof in that language?). Importantly, all but the last step of the
proof can be encoded as primitive recursive functions, meaning that they
always halt within a predetermined number of steps (satisfying the
Finitists). Only the last step cannot be so limited. This is a clear
example where non-finite mathematics has demonstrably more power in a
fundamentally important way.
Why bother going through this encoding? The main reason for the encoding
is to overcome the fundamental limitation of structural induction
whereby there is no "this" smaller than this. I.e. quoting a sentence
only makes it longer. With functions on integers, this limitation is
removed, so that although there is no string saying "This statement is
not true", (since "This statement" != "\"This statement is not true\""),
there *is* some function taking the Godel number of the unquoted This to
the Godel number of the string to which it refers. Doing so takes some
bit of cleverness, but the original proof in German is only about 8
pages long, as I recall.
If we don't go with mirroring and just use strings, we need to introduce
some equivalent trick, namely named functions. In a language without
pointers and only lambda expressions, there is no way to refer to
oneself without repeating the quote in infinite regression. For instance
"\x -> 3333333" is longer than "333333". You cannot talk about a string
without embedding it as a substring. However, once you add named
functions to your metalanguage (Haskell):
f 3 = 33333333
Then the string "f 3" is shorter than the string "xxxxxxx". Suppose f 4
= "~xxxxxxx". Now one can talk about the other with the shorter string
on the left: length "f 3" < length "~xxxxxxx" but also length "f 4" <
length "xxxxxxx". A longer string can talk about a shorter string (but
not vice versa), so this mapping is critical to overcoming the
limitation about talking about oneself.
After that, the rest is easy: encode the Liar's Paradox and voila. once
we have the encoding of a language, and construct functions to encode
proof transformations, we can reduce derivability to a simple predicate
derivable :: String -> Bool and look for some formula f such that
derivable (f) == False and derivable("~" ++ f) == False.
Godel's First Incompleteness Theorem merely says that there is some
integer (which mirrors some well-formed formula) not in the set of
integers that mirror "derivable theorems", making your system
incomplete. Moreover, if you remedy this situation by adding this
integer to the set as an axiom, you immediately can derive another
integer which mirrors its negated formula, making your system inconsistent.
The metasystem (with symbols for derivable, transformation rules like
modus ponens, and the like), are not part of the formal system, but in
the metalanguage. By encoding this metalanguage as well and redoing the
above, you get Godel's Second Incompleteness Theorem, which says that no
system can prove its own consistency, and if an axion is added to assert
consistency, you can immediately also prove its negation, making it
unsound.
Don't look for a hat trick. Encoding the meta-meta-system buys you
nothing extra.
That's about all I can remember without hypnosis, and I'm afraid of what
I might say under hypnosis... :)
Dan
Algebras Math wrote:
> you mean the godel function (denoted by # and generally will be in type,
> #:term -> number ?) is a kind of functions instead of a particular
> function? If so, what kind of property this kinds of functions have? any
> limitation? how capable they will be?
>
> Thanks
>
> alg
>
> On Tue, Mar 31, 2009 at 4:01 AM, Dan Weston <[email protected]
> <mailto:[email protected]>> wrote:
>
> I can't tell exactly what you're asking, but I'll give it a try! :)
>
> primes :: [Integer]
> primes = [2,3,5,7,11,13,17,19,23,29,31,undefined]
>
> godel :: String -> Integer
> godel = product . zipWith (^) primes . map (toInteger . ord)
>
> -- Here is the identity function (note that double backslash is a
> single character
> godel "\\x -> x"
>
> 1629920514342441477851613634029704631135430980107335428017064836156091059806450516131002598452000651374890570022191128551421788559667251656959733380229796871976693176094558797489489057311763922507760911447493016261397754567695234219623056037447490713525815311253273691703346455275115486717580778238094808661626709709766328915159206002675716287759792707200037683200000000000000000000000000000000
>
> -- = 2^92 * 3^120 * 5^32 * 7^45 * 11^62 * 13^32 * 17^120
>
> ungodel :: Integer -> String
> -- ungodel . godel = id
>
> (See http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic
> for why this works).
>
> These numbers get large quickly, but are finite for any finite
> string of finite alphabet.
>
> godel is a total function (every string has a unique integer), and
> its inverse (an exercise to the reader involving prime factor
> decomposition) would also be total if the alphabet were infinite (so
> that ord would be total).
>
> Frankly, I wouldn't know how to begin encoding the godel numbering
> in the type system (shudder!), but being that it is a total
> primitive recursive function, I suppose there is no theoretical
> impediment.
>
> In contrast, Godel's Theorems themselves cannot be so encoded
> because the last step involves a general recursive function.
>
> Dan
>
>
> Algebras Math wrote:
>
> Hi all,
>
> I am reading the book "The lambda calculus: Its syntax and
> Semantics" in the chapter about Godel Numbering but I am
> confused in some points.
>
> We know for Church Numerals, we have Cn = \fx.f^n(x) for some
> n>=0, i.e. C0 = \fx.x and C1 = \fx.fx.
>
> From the above definition, I could guess the purpose of this
> kind of encoding is trying to encode numeral via terms.
>
> How about the Godel Numbering? From definition we know people
> say #M is the godel number of M and we also have [M] = C#M to
> enjoy the second fixed point theorem : for all F there exists X
> s.t. F[X] = X.
>
> What the mapping function # is standing for? How could I use it?
> What the #M will be? How to make use of the Godel Numbering?
>
> Thank you very much!
>
> alg
>
>
>
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 10, Issue 1
****************************************
