[Haskell-cafe] statistics package and randomness
I'm trying to learn how to use randomness in Haskell and it seems very non-straightforward and complex. I could do a lot of things using 'split' from System.Random, but apparently it's broken. There is the statistics package here: http://hackage.haskell.org/package/statistics Is this a better solution? It uses the ST monad in the RandomVariate module. Can someone point me to a tutorial explaining ST, and/or a tutorial in the RandomVariate module? Pseudorandomness seems like one case where it would just be a hell of a lot simpler to have a global generator--never split the state. Is the ST monad some way to accomplish this? Thanks, Mike ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-level naturals multiplication
On Sat, Oct 10, 2009 at 02:59:37PM -0400, Brad Larsen wrote: Suppose we implement type-level naturals as so: data Zero data Succ a Then, we can reflect the type-level naturals into a GADT as so (not sure if ``reflect'' is the right terminology here): data Nat :: * - * where Zero :: Nat Zero Succ :: Nat a - Nat (Succ a) Using type families, we can then proceed to define type-level addition: type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) Is there any way to define type-level multiplication without requiring undecidable instances? I hesitate to contradict Manuel Chakravarty on this subject... but I posted a type-level multiplication program without undecidable instances on this list in June: http://www.haskell.org/pipermail/haskell-cafe/2009-June/062452.html If you prefer to use EmptyDataDecls, you can replace the first four lines by data Z data S n data Id :: * - * data (:.) :: (* - *) - (* - *) - (* - *) And I still don't understand why that definition works while the obvious one doesn't :) Regards, Reid Barton ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] statistics package and randomness
i'll try a very non-technical explanation that has worked for me so far. (is it correct? does it make sense?) IO and ST are quite similar. the difference is that whereas IO gives you a concept of time in the world surrounding your code, ST lets you create a little bubble inside your code in which you can maintain state, while the bubble as a whole acts all pure and lazy. for example, if you want to implement an algorithm that writes to and reads from a matrix, you use ST: you want to control the order in which you read from and write to it, but not the order in which access events to that data structure mixes with user interaction events. -matthias On Mon, Oct 12, 2009 at 12:25:43AM -0700, Michael Mossey wrote: To: Haskell Cafe Haskell-Cafe@haskell.org Cc: From: Michael Mossey m...@alumni.caltech.edu Date: Mon, 12 Oct 2009 00:25:43 -0700 Subject: [Haskell-cafe] statistics package and randomness I'm trying to learn how to use randomness in Haskell and it seems very non-straightforward and complex. I could do a lot of things using 'split' from System.Random, but apparently it's broken. There is the statistics package here: http://hackage.haskell.org/package/statistics Is this a better solution? It uses the ST monad in the RandomVariate module. Can someone point me to a tutorial explaining ST, and/or a tutorial in the RandomVariate module? Pseudorandomness seems like one case where it would just be a hell of a lot simpler to have a global generator--never split the state. Is the ST monad some way to accomplish this? Thanks, Mike ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ** ACCEPT: CRM114 PASS osb unique microgroom Matcher ** CLASSIFY succeeds; success probability: 1. pR: 5.5394 Best match to file #0 (nonspam.css) prob: 1. pR: 5.5394 Total features in input file: 2960 #0 (nonspam.css): features: 758386, hits: 2888631, prob: 1.00e+00, pR: 5.54 #1 (spam.css): features: 1683715, hits: 3150692, prob: 2.89e-06, pR: -5.54 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] a library for control of terminal driver modes?
On 11 Oct 2009, at 15:30, Andrew Coppin wrote: Iain Barnett wrote: I'm looking for a library like Perl's Term-Readkey, so that I can turn on and off the echo for secure password input from a terminal. Anyone know which library I need to use for this? The package ansi-terminal allows you to do various things to the terminal; I think it might include turning local echo on/off. Alternatively, there was an announcement recently about a text-mode UI package, which might do what you want. (I don't recall the name...) Thanks Iain ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] safe way to use Rand?
I'm looking at Control.Monad.Random which provides the Rand monad. I would like to know how to use this for generating multiple infinite series, while trusting that the implementation never uses split behind the scenes. (Note: I'm on Windows XP, and there appears to be a bug in getStdGen. It does NOT return an arbitrary generator, but rather the same one every time I run the program. However, newStdGen DOES return an arbitrary generator. So I'm using that, even though I know it accesses split behind the scenes. My thinking is that this only happens once so it is okay.) For example, is this code split-free? simple :: Rand StdGen [Int] simple = getRandomRs (0::Int, 10) main1 = do gen - newStdGen let answer = (flip evalRand) gen $ do xs - simple ys - simple return $ (take 5 xs) ++ (take 3 ys) print answer Then, to elaborate on my specific problem, I need to create special types of infinite series. For example, I might need to create one that looks like this: 0 0 5 0 0 0 2 0 0 0 0 0 5 0 9 0 0 8 ... The pattern here is that there is some random number of zeros followed by a single non-zero value, followed again by a random number of zeros, etc. forever. This is one way to implement this. Does all look well here? makeSeries :: [Int] - [a] - a - [a] makeSeries (i:is) (f:fs) zero = replicate i zero ++ [f] ++ makeSeries is fs zero lessSimple :: Rand StdGen [Int] lessSimple = do counts - getRandomRs (1::Int , 5 ) values - getRandomRs (1::Int , 9 ) return $ makeSeries counts values 0 main2 = do gen - newStdGen let answer = evalRand lessSimple gen print . take 20 $ answer We could even have several of these series zipped together. Is this split-free? main3 = do gen - newStdGen let fs = (flip evalRand) gen $ do s1 - lessSimple s2 - lessSimple return $ zip s1 s2 print . take 20 $ fs ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What *is* a DSL?
Hi Bob, I tried to understand this by applying what you said here to your deep embedding of a parsing DSL. But I can't figure out how to do that. What things become the type class T? greetings, Sjoerd On Oct 7, 2009, at 9:18 PM, Robert Atkey wrote: What is a DSL? How about this as a formal-ish definition, for at least a pretty big class of DSLs: A DSL is an algebraic theory in the sense of universal algebra. I.e. it is an API of a specific form, which consists of: a) a collection of abstract types, the carriers. Need not all be of kind *. b) a collection of operations, of type t1 - t2 - ... - tn where tn must be one of the carrier types from (a), but the others can be any types you like. c) (Optional) a collection of properties about the operations (e.g. equations that must hold) Haskell has a nice way of specifying such things (except part (c)): type classes. Examples of type classes that fit this schema include Monad, Applicative and Alternative. Ones that don't include Eq, Ord and Show. The Num type class would be, if it didn't specify Eq and Show as superclasses. An implementation of a DSL is just an implementation of corresponding type class. Shallowly embedded DSLs dispense with the type class step and just give a single implementation. Deeply embedded implementations are *initial* implementations: there is a unique function from the deep embedding to any of the other implementations that preserves all the operations. The good thing about this definition is that anything we do to the deep embedding, we can do to any of the other implementations via the unique map. Thanks to Church and Reynolds, we can always get a deep embedding for free (free as in Theorems for Free). If our DSL is defined by some type class T, then the deep embedding is: type DeepT = forall a. T a = a (and so on, for multiple carrier types, possibly with type parameterisation). Of course, there is often an easier and more efficient way of representing the initial algebra using algebraic data types. Conor McBride often goes on about how the initial algebra (i.e. the deep embedding) of a given specification is the one you should be worrying about, because it often has a nice concrete representation and gives you all you need to reason about any of the other implementations. Bob -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Sjoerd Visscher sjo...@w3future.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: What *is* a DSL?
This problem of dynamically transforming grammars and bulding parsers
out of it is addressed in:
@inproceedings{1411296,
author = {Viera, Marcos and Swierstra, S. Doaitse and Lempsink,
Eelco},
title = {Haskell, do you read me?: constructing and composing
efficient top-down parsers at runtime},
booktitle = {Haskell '08: Proceedings of the first ACM SIGPLAN
symposium on Haskell},
year = {2008},
isbn = {978-1-60558-064-7},
pages = {63--74},
location = {Victoria, BC, Canada},
doi = {http://doi.acm.org/10.1145/1411286.1411296},
publisher = {ACM},
address = {New York, NY, USA},
}
and the code can be found on hackage under the name ChristmasTree
The left-factorisation is explained in a paper we presented at the
last LDTA and which will appear in ENTCS. Since we have signed some
copyright form I do notthink I can attach it here, but if you send me
a mail, I can definitely send you the paper.
Doaitse
On 11 okt 2009, at 21:54, Ben Franksen wrote:
Ben Franksen wrote:
Next thing I'll try is to transform such a grammar into an actual
parser...
Which I also managed to get working. However, this exposed yet another
problem I am not sure how to solve.
The problem manifests itself with non-left-factored rules like
Number ::= Digit Number | Digit
Translating such a grammar directly into a Parsec parser leads to
parse
errors because Parsec's choice operator is predictive: if a
production has
consumed any input the whole choice fails, even if alternative
productions
would not:
*Main P.parseTest (parseGrammar myGrm) 2
parse error at (line 1, column 2):
unexpected end of input
expecting Number
Of course, one solution is to apply Parsec's try combinator to all
choices
in a rule. But this rather defeats the purpose of using a (by default)
predictive parser in the first place which is to avoid unnecessary
backtracking.
So, a better solution is to left-factor the grammar before
translating to
Parsec. Since we have a data representation of the grammar that we can
readily analyse and transform, this should be possible given some
suitable
algorithm. But how is this transformation to be typed?
My first naive attempt was to define (recap: nt :: * - * is the
type of
nonterminals, t :: * is the type of terminals a.k.a. tokens, and a
is the
result type):
leftFactor :: Grammar nt t a - Grammar nt t a
Of course, this is wrong: Left-factoring is expected to introduce new
nonterminals, so on the right-hand side of the type we should not
have the
same 'nt' as on the left. Instead we shoudl have some other type that
is 'nt' extended with new constructors. Moreover, we cannot
statically
know how many new nonterminals are added, so we cannot simply apply
a type
function to nt. Is this solvable at all in Haskell or do I need proper
dependent types to express this?
I have very vague ideas that revolve around setting up some
recursive type
function that on each level adds one constructor, define a common
interface
with a (multiparam) type class and then use existential
quantification in
the result type to hide the resulting type of nonterminals.
The next question is: Even if this turns out to be possible, isn't it
overkill? Maybe it is better to use an infinite type for the
nonterminals
in the first place and let the grammar be a partial function? OTOH,
the
formulation of the grammar as a function that pattern matches on the
nonterminals is very elegant.
Cheers
Ben
___
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
[Haskell-cafe] ** for nested applicative functors?
Does anyone know if it's possible to write the following: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) Clearly, if m and n were monads, it would be trivial. Rereading the original paper, I didn't see much discussion about such nested app. functors. Any help appreciated. -- View this message in context: http://www.nabble.com/%3C**%3E-for-nested-applicative-functors--tp25858792p25858792.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Documentation (was: ANN: text 0.5, a major revision of the Unicode text library)
From: Derek Elkins derek.a.elk...@gmail.com On Sun, Oct 11, 2009 at 8:55 AM, Iain Barnett iainsp...@gmail.com wrote: On 11 Oct 2009, at 13:58, John Lato wrote: For anyone writing introductions to generic programming, take this as a plea from Haskellers everywhere. If one of the RWH authors can't understand how to make use of these techniques, what hope do the rest of us have? John Lato P.S. Some might wryly note that I'm the maintainer of a package which is also known for incomprehensible documentation. To which I would reply that our effort is much newer, I consider it a problem, and it's being worked on, contrasted to the state of GP where similarly impenetrable documentation has been and continues to be the norm. You could say that about most documentation (for Haskell and beyond). Apparently, programmers like programming better than documenting. The effect of this is that less people use their programming, making their efforts redundant. Silly really, considering programmers are (allegedly:) intelligent. Apparently, programmers like programming better than reading as well... in my experience. I won't disagree. But I think the real difficulty is that the intersection of programmers who can come up with really good ways to solve problems (not even all programmers, unfortunately) and people who are good at writing documentation is vanishingly small. It seems to me that when someone works in a problem domain (e.g. Generic Programming), they gain a very deep understanding of that area and are used to working at a certain level within it. When introducing the topic to newcomers (even ostensibly smart programmers) the introduction can't assume prior knowledge of the problem domain, but the authors are so used to thinking at one level they often take for granted knowledge that the audience doesn't have. I don't think this problem is particular to programming, but it is common in Haskell. Most likely because Haskell, with a reputation as a research language, has a lot of computer science types doing research in wide-ranging topics. Somebody's expertise in category theory, for example, might not directly carry over to generic programming (or maybe it does; I'm not an expert in either). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ** for nested applicative functors?
On Mon, Oct 12, 2009 at 6:22 PM, Kim-Ee Yeoh a.biurvo...@asuhan.com wrote: Does anyone know if it's possible to write the following: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) Clearly, if m and n were monads, it would be trivial. Rereading the original paper, I didn't see much discussion about such nested app. functors. Any help appreciated. How about m ** n = pure (*) * m * n Hth, Josef ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ** for nested applicative functors?
This looks like what is described in Section 4 to me: http://www.haskell.org/haskellwiki/Applicative_functor#Applicative_transfomers - jeremy On Oct 12, 2009, at 11:22 AM, Kim-Ee Yeoh wrote: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Can type be changed along a = chain?
The first of these works, but not the second. It would seem that the type
cannot change along a = chain, but I may be missing something in the code.
Is the second example illegal? If so, is there a different way to change a
String to an Int along the = chain?
Michael
===
import Data.Char
{-
transform :: IO ()
transform = putStrLn What is your word?
getLine
= \str - return ('Q':str)
= \str - return ('Z':str)
= \str - putStrLn $ Transformed word is ++ show str
-}
transform :: IO ()
transform = putStrLn What is your digit string?
getLine
= \str - return ('9':str)
= \str - return (read str :: Int)
= \i - putStrLn $ The number is ++ show i
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can type be changed along a = chain?
On Mon, Oct 12, 2009 at 6:37 PM, michael rice nowg...@yahoo.com wrote:
transform :: IO ()
transform = putStrLn What is your digit string?
getLine
= \str - return ('9':str)
= \str - return (read str :: Int)
= \i - putStrLn $ The number is ++ show i
This code works perfectly for me. What problem are you seeing specifically?
Cheers,
/Niklas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can type be changed along a = chain?
2009/10/12 michael rice nowg...@yahoo.com
The first of these works, but not the second. It would seem that the type
cannot change along a = chain, but I may be missing something in the code.
Is the second example illegal? If so, is there a different way to change a
String to an Int along the = chain?
Michael
===
import Data.Char
{-
transform :: IO ()
transform = putStrLn What is your word?
getLine
= \str - return ('Q':str)
= \str - return ('Z':str)
= \str - putStrLn $ Transformed word is ++ show str
-}
transform :: IO ()
transform = putStrLn What is your digit string?
getLine
= \str - return ('9':str)
= \str - return (read str :: Int)
= \i - putStrLn $ The number is ++ show i
Both seem good to me and my old ghci (6.6.1)...
Thu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ** for nested applicative functors?
That's it: liftA2 (*), so obvious in hindsight. Mustn't ... code ... when ... drained Thanks to Jeremy and Josef. Jeremy Shaw-3 wrote: This looks like what is described in Section 4 to me: http://www.haskell.org/haskellwiki/Applicative_functor#Applicative_transfomers - jeremy On Oct 12, 2009, at 11:22 AM, Kim-Ee Yeoh wrote: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) -- View this message in context: http://www.nabble.com/%3C**%3E-for-nested-applicative-functors--tp25858792p25859274.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ** for nested applicative functors?
fmap (*) :: m (n (a - b)) - m (n a - n b) so f ** x = (fmap (*) f) * x On Mon, Oct 12, 2009 at 9:22 AM, Kim-Ee Yeoh a.biurvo...@asuhan.com wrote: Does anyone know if it's possible to write the following: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) Clearly, if m and n were monads, it would be trivial. Rereading the original paper, I didn't see much discussion about such nested app. functors. Any help appreciated. -- View this message in context: http://www.nabble.com/%3C**%3E-for-nested-applicative-functors--tp25858792p25858792.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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] Can type be changed along a = chain?
Dumb! I just figured out I was entering the input string in quotes.
So, I suppose the answer to my question is yes, type CAN be changed along a =
chain. I was having trouble doing it in a different problem, created this small
example to illustrate the problem, and then screwed it up putting quotes around
my input string.
Thanks!
Michael
--- On Mon, 10/12/09, Niklas Broberg niklas.brob...@gmail.com wrote:
From: Niklas Broberg niklas.brob...@gmail.com
Subject: Re: [Haskell-cafe] Can type be changed along a = chain?
To: michael rice nowg...@yahoo.com
Cc: haskell-cafe@haskell.org
Date: Monday, October 12, 2009, 12:43 PM
On Mon, Oct 12, 2009 at 6:37 PM, michael rice nowg...@yahoo.com wrote:
transform :: IO ()
transform = putStrLn What is your digit
string?
getLine
= \str - return ('9':str)
= \str - return (read str :: Int)
= \i - putStrLn $ The number is ++ show i
This code works perfectly for me. What problem are you seeing specifically?
Cheers,/Niklas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can type be changed along a = chain?
I hope you're not building some unneeded rules in your head. There is no
reason to believe there is something to be remembered about whether or not
types can change along a = chain. That chain has nothing special in
Haskell. = is just an operator, much like ++, ! or .
ghci :t (=)
(=) :: (Monad m) = m a - (a - m b) - m b
This says that, you provide an a and you get a b. Nothing says the a and b
have to be the same upon successive uses.
Likewise,
ghci :t (+)
(+) :: (Num a) = a - a - a
fromIntegral ((1 :: Int) + 2) + (3 :: Integer)
6
This shows clearly that the types are not the same along the + chain.
2009/10/12 michael rice nowg...@yahoo.com
Dumb! I just figured out I was entering the input string in quotes.
So, I suppose the answer to my question is yes, type CAN be changed along a
= chain. I was having trouble doing it in a different problem, created
this small example to illustrate the problem, and then screwed it up putting
quotes around my input string.
Thanks!
Michael
--- On *Mon, 10/12/09, Niklas Broberg niklas.brob...@gmail.com* wrote:
From: Niklas Broberg niklas.brob...@gmail.com
Subject: Re: [Haskell-cafe] Can type be changed along a = chain?
To: michael rice nowg...@yahoo.com
Cc: haskell-cafe@haskell.org
Date: Monday, October 12, 2009, 12:43 PM
On Mon, Oct 12, 2009 at 6:37 PM, michael rice
nowg...@yahoo.comhttp://mc/compose?to=nowg...@yahoo.com
wrote:
transform :: IO ()
transform = putStrLn What is your digit string?
getLine
= \str - return ('9':str)
= \str - return (read str :: Int)
= \i - putStrLn $ The number is ++ show i
This code works perfectly for me. What problem are you seeing specifically?
Cheers,
/Niklas
___
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] What *is* a DSL?
On Mon, 2009-10-12 at 15:49 +0200, Sjoerd Visscher wrote: Hi Bob, I tried to understand this by applying what you said here to your deep embedding of a parsing DSL. But I can't figure out how to do that. What things become the type class T? Here's the API version of the grammar DSL: class GrammarDSL grammar where type Rule grammar :: (* - *) - * - * pure:: a - Rule grammar nt a (*) :: Rule grammar nt (a - b) - Rule grammar nt a - Rule grammar nt b empty :: Rule grammar nt a (|) :: Rule grammar nt a - Rule grammar nt a - Rule grammar nt a char:: Char - Rule grammar nt () nt :: nt a - Rule grammar nt a grammar :: forall nt a. nt a - (forall a. nt a - Rule grammar nt a) - grammar nt a The language of typed-grammars-with-actions is composed of: * two sorts: grammars and rules * rules support the applicative and alternative interfaces, and also two special operators for incorporating terminals and nonterminals into rules. * grammars support a single operation: taking a nonterminal-indexed collection of rules, and a starting non-terminal (as Ben Franksen pointed out), producing a grammar. Basically, the idea is to think 1) what are the syntactic categories of my DSL?, these become the sorts; 2) what are the basic syntactic constructions of my DSL?, these become the operations of the type class. Because we are embedded in Haskell, we can have infinite syntax, as demonstrated by the grammar operation. WRT the recipe for getting deep embeddings in my previous post, it isn't quite true that the type Grammar nt a = forall grammar. GrammarDSL grammar = grammar nt a is isomorphic to the deep embedding I posted before, because it doesn't guarantee that the applicative functor or alternative laws hold, while the deep embedding does (and it also ensures that * and | distribute). It isn't hard to come up with a deep embedding that is initial for the completely free version though. The deep embedding from the previous post is an instance of this type class. So is, as Ben Franksen showed, a Parsec parser. I ended up having to inline the applicative and alternative interfaces into the class definition above. I wanted to write: class (Applicative (Rule grammar nt), Alternative (Rule grammar nt)) = Grammar grammar where ... but GHC wouldn't let me, complaining that 'nt' wasn't bound. Is there any reason this couldn't be made to work? Bob -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] is proof by testing possible?
Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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] is proof by testing possible?
It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
For example, it is possible to prove correctness of a function negatedHead :: [Bool] - Bool by testing it on True:undefined and False:undefined. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Really? How? That sounds very interesting, I've got a fair knowledge of basic topology, I'd love to see an application to programming... On Oct 12, 2009, at 1:55 PM, Eugene Kirpichov wrote: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Also google seemingly impossible functional programs. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: For example, it is possible to prove correctness of a function negatedHead :: [Bool] - Bool by testing it on True:undefined and False:undefined. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Oh- thanks for the example, I suppose you can disregard my other message. I suppose this is a bit like short-circuiting. No? On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: For example, it is possible to prove correctness of a function negatedHead :: [Bool] - Bool by testing it on True:undefined and False:undefined. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. not True==False not False==True Done. Tested :-) Less trivially, consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) - (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) - (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.) -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] statistics package and randomness
On Mon, Oct 12, 2009 at 12:25 AM, Michael Mossey m...@alumni.caltech.eduwrote: I'm trying to learn how to use randomness in Haskell and it seems very non-straightforward and complex. I could do a lot of things using 'split' from System.Random, but apparently it's broken. There is the statistics package here: http://hackage.haskell.org/package/statistics Is this a better solution? Yes, as it's much faster, more robust, and (depending on your perspective) easier to use, provided you understand the ST monad. It uses the ST monad in the RandomVariate module. Can someone point me to a tutorial explaining ST, and/or a tutorial in the RandomVariate module? For a tutorial on grokking ST, I'd suggest chapter 26 of Real World Haskell, but I'm biased, since I wrote it: http://book.realworldhaskell.org/read/advanced-library-design-building-a-bloom-filter.html Note that this already assumes that you understand monads pretty well. Pseudorandomness seems like one case where it would just be a hell of a lot simpler to have a global generator--never split the state. Is the ST monad some way to accomplish this? Having ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. /Joe On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. not True==False not False==True Done. Tested :-) Less trivially, consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) - (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) - (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.) -- Dan ___ 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] statistics package and randomness
On Mon, Oct 12, 2009 at 11:01 AM, Bryan O'Sullivan b...@serpentine.comwrote: Pseudorandomness seems like one case where it would just be a hell of a lot simpler to have a global generator--never split the state. Is the ST monad some way to accomplish this? Having [...] Feh, gmail fail. Having a global generator is not actually a good thing, since it has to live *somewhere*. If you keep its existence implicit, it becomes slow, since you have to lock it against concurrent use by multiple threads. If you make it explicit, you have to plumb the thing all over the place by hand, which is also nasty. The advantage of putting the PRNG in the ST monad is that you can seed a new PRNG close to the point where you'll need it, and not need to pass around so much state. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Joe, On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette jfred...@gmail.com wrote: I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. There is Wadler's paper but I do find it tricky: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 You can play with the generator here: http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ The results can look unreadable at first, but I find that if I copy them onto paper and do all of the remaining substitutions manually (like I had to do with (a,b) - (b,a)) you end up with something readable. If you keep doing this you'll get a good intuition for what the free theorem for a type will look like. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
What do you mean under short-circuiting here, and what is the connection? The property that allows to deduce global correctness from correctness on under-defined inputs is just continuity in the topological sense. 2009/10/12 Joe Fredette jfred...@gmail.com: Oh- thanks for the example, I suppose you can disregard my other message. I suppose this is a bit like short-circuiting. No? On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: For example, it is possible to prove correctness of a function negatedHead :: [Bool] - Bool by testing it on True:undefined and False:undefined. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
I'm making the same mistake repeatedly. In both my mails there are places where I said (a,b) or (b,a) when I meant (a,a). -- Dan On Mon, Oct 12, 2009 at 11:09 AM, Dan Piponi dpip...@gmail.com wrote: Joe, On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette jfred...@gmail.com wrote: I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. There is Wadler's paper but I do find it tricky: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 You can play with the generator here: http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ The results can look unreadable at first, but I find that if I copy them onto paper and do all of the remaining substitutions manually (like I had to do with (a,b) - (b,a)) you end up with something readable. If you keep doing this you'll get a good intuition for what the free theorem for a type will look like. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
I mean that, like in the definition of `||` True || _ = True False || x = x If you generalize this to `or`-ing a list of inputs, eg: foldr (||) False list_of_bools you can 'short-circuit' the test as soon as you find a 'True' value. This is actually not the greatest example, since you can't actually test it in finite number of tests, but you can test half the function by testing a that lists like [True:undefined] or [False, False, False, ... , True , undefined] return True. It's short-circuiting in the sense that it (like the `||` function) doesn't need to see (necessarily) all of it's arguments to return a correct result. /Joe On Oct 12, 2009, at 2:11 PM, Eugene Kirpichov wrote: What do you mean under short-circuiting here, and what is the connection? The property that allows to deduce global correctness from correctness on under-defined inputs is just continuity in the topological sense. 2009/10/12 Joe Fredette jfred...@gmail.com: Oh- thanks for the example, I suppose you can disregard my other message. I suppose this is a bit like short-circuiting. No? On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: For example, it is possible to prove correctness of a function negatedHead :: [Bool] - Bool by testing it on True:undefined and False:undefined. 2009/10/12 Eugene Kirpichov ekirpic...@gmail.com: It is possible for functions with compact domain, not just finite. 2009/10/12 Joe Fredette jfred...@gmail.com: In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. -- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ 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 -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) swap = undefined Terminates and does not swap its arguments :-) What do free theorems say about this, exactly -- do they just implicitly exclude this possibility? Neil. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Sharing Subexpressions: Memoization of Fibonacci sequence
Hallo everyone, the last few weeks I was trying to get used to memoization in haskell. As I found out in a previous post, memoization in haskell is, due to the graph reduction strategy used in haskell, almost always implemented by sharing subexpressions in an expression. In examples as the following this is quite easy to see. fibs = 0:1:zipWith (+) fibs (tail fibs) But as I browsed through the search results from google for this topic, I encountered the following implementation: memoized_fib :: Int - Integer memoized_fib = let fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) in (map fib [0 ..] !!) You'll find it at Haskell.org. Here's the http://www.haskell.org/haskellwiki/Memoization link Let's assume we have the following implementation of the higher-order-function map: map :: (a - b) - [a] - [b] map _ [] = [] map f (x:xs) = f x : map f xs The reduction sequence of memoized_fib 5 would start as follows: //Reduction of memoized_fib 5 memoized_fib 5 = (map fib [0..] !!) 5 = (fib 0 : map fib [1..] !!) 5 = (0 : fib 1 : map fib [2..] !!) 5 = (0 : 1 : fib 2 : map fib [3..] !!) 5 = (0 : 1 : (memoized_fib 0 + memoized_fib 1) : fib 3 : map fib [4..] !!) 5 = (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) : (memoized_fib 1 + memoized_fib 2) : map fib [4..] !!) 5 . . . . and so on! I can't see where the sharing of subexpressions happens here. Any help is highly appreciated. Best regards Simon -- View this message in context: http://www.nabble.com/Sharing-Subexpressions%3A-Memoization-of-Fibonacci-sequence-tp25861134p25861134.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sharing Subexpressions: Memoization of Fibonacci sequence
**Edit: formatting was bad** Hallo everyone, the last few weeks I was trying to get used to memoization in haskell. As I found out in a previous post, memoization in haskell is, due to the graph reduction strategy used in haskell, almost always implemented by sharing subexpressions in an expression. In examples as the following this is quite easy to see. fibs = 0:1:zipWith (+) fibs (tail fibs) But as I browsed through the search results from google for this topic, I encountered the following implementation: memoized_fib :: Int - Integer memoized_fib = let fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) in (map fib [0 ..] !!) You'll find it at Haskell.org. Here's the http://www.haskell.org/haskellwiki/Memoization link Let's assume we have the following implementation of the higher-order-function map: map :: (a - b) - [a] - [b] map _ [] = [] map f (x:xs) = f x : map f xs The reduction sequence of memoized_fib 5 would start as follows: //Reduction of memoized_fib 5 memoized_fib 5 = (map fib [0..] !!) 5 = (fib 0 : map fib [1..] !!) 5 = (0 : fib 1 : map fib [2..] !!) 5 = (0 : 1 : fib 2 : map fib [3..] !!) 5 = (0 : 1 : (memoized_fib 0 + memoized_fib 1) : fib 3 : map fib [4..] !!) 5 = (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) : (memoized_fib 1 + memoized_fib 2) : map fib [4..] !!) 5 . . . . and so on! I can't see where the sharing of subexpressions happens here. Any help is highly appreciated. Best regards Simon -- View this message in context: http://www.nabble.com/Sharing-Subexpressions%3A-Memoization-of-Fibonacci-sequence-tp25861134p25861177.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Neil Brown wrote: Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) swap = undefined Terminates and does not swap its arguments :-) What do free theorems say about this, exactly -- do they just implicitly exclude this possibility? Normally, one presumes that undefined (id est, calling error) is equivalent to looping, except that calling error is pragmatically speaking better: it is nicer to the caller of your function (they/you get to see a somewhat more descriptive error message instead of 100% CPU without any results). Regards, Jochem -- Jochem Berndsen | joc...@functor.nl | joc...@牛在田里.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown nc...@kent.ac.uk wrote: swap = undefined Terminates and does not swap its arguments :-) What do free theorems say about this, exactly -- do they just implicitly exclude this possibility? I'm terrible at reasoning about functions with bottoms (ie. undefined or non-termination). But I suspect that a property like this holds: if the type signature of a function f is polymorphic in a, and it doesn't produce bottom for one particular value x of type a, for some particular type a, f can never produce bottom for any choice of x in any choice of type a. (Which is not to say it might not fail, but that the failure will be an issue with x, not f.) The intuition behind this is that if a function is polymorphic in a then it never examines the a. So even if a is bottom, the function can never know it. But it could fail because f additionally accepts as argument a polymorphic function that itself accepts a's, and that fails. But then it wouldn't be f's fault, it'd be the fault of the function you passed in. This is very poor of me. There's probably a nice precise formulation of what I've just said :-) -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sharing Subexpressions: Memoization of Fibonacci sequence
2009/10/12 SimonK77 simonkaltenbac...@googlemail.com: **Edit: formatting was bad** Hallo everyone, the last few weeks I was trying to get used to memoization in haskell. As I found out in a previous post, memoization in haskell is, due to the graph reduction strategy used in haskell, almost always implemented by sharing subexpressions in an expression. In examples as the following this is quite easy to see. fibs = 0:1:zipWith (+) fibs (tail fibs) But as I browsed through the search results from google for this topic, I encountered the following implementation: memoized_fib :: Int - Integer memoized_fib = let fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) in (map fib [0 ..] !!) You'll find it at Haskell.org. Here's the http://www.haskell.org/haskellwiki/Memoization link Let's assume we have the following implementation of the higher-order-function map: map :: (a - b) - [a] - [b] map _ [] = [] map f (x:xs) = f x : map f xs The reduction sequence of memoized_fib 5 would start as follows: //Reduction of memoized_fib 5 memoized_fib 5 = (map fib [0..] !!) 5 = (fib 0 : map fib [1..] !!) 5 = (0 : fib 1 : map fib [2..] !!) 5 = (0 : 1 : fib 2 : map fib [3..] !!) 5 = (0 : 1 : (memoized_fib 0 + memoized_fib 1) : fib 3 : map fib [4..] !!) 5 = (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) : (memoized_fib 1 + memoized_fib 2) : map fib [4..] !!) 5 . . . . and so on! Hi, Instead of repeating as-is map fib [0..] consider it as a single list that is always reused. Since the list maps the input of the fib function to the result of the function and that list is always reused, the recursive calls have immediately the answer (i.e. at the cost of the lookup). So your fragment (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) ... should look like lst = (0 : 1 : (lst !! 0 + lst !! 1) ... which is similar to the zipWith (+) version. Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can type be changed along a = chain?
minh thu not...@gmail.com writes: ghci :t (=) (=) :: (Monad m) = m a - (a - m b) - m b This says that, you provide an a and you get a b. Nothing says the a and b have to be the same upon successive uses. (But note that the monad 'm' has to be the same all the way. You can't switch from, say, IO to ST in the middle of the computation.) Likewise, Contrariwise, I'd say. ghci :t (+) (+) :: (Num a) = a - a - a I.e. (+) requires the same type on both sides... fromIntegral ((1 :: Int) + 2) + (3 :: Integer) 6 ...but 'fromIntegral' converts it. Did I miss some subtle point here? -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: is proof by testing possible?
Joe Fredette wrote: Really? How? That sounds very interesting, I've got a fair knowledge of basic topology, I'd love to see an application to programming... Compactness is one of the most powerful concepts in mathematics, because on the one hand it makes it possible to reduce many infinite problems to finite ones (inherent in its definition: for every open cover there is a finite subcover), on the other hand it is often easy to prove compactness due to Tychonoff's theorem (any product of compact spaces is compact). The connection to computing science is very nicely explained in http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ I found this paragraph particularly enlightening: modulus :: (Cantor - Integer) - Natural modulus f = least(\n - forevery(\a - forevery(\b - eq n a b -- (f a == f b This [...] finds the modulus of uniform continuity, defined as the least natural number `n` such that `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` where `alpha =_n beta iff forall i n. alpha_i = beta_i.` What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). Cheers ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can type be changed along a = chain?
2009/10/12 Ketil Malde ke...@malde.org: minh thu not...@gmail.com writes: ghci :t (=) (=) :: (Monad m) = m a - (a - m b) - m b This says that, you provide an a and you get a b. Nothing says the a and b have to be the same upon successive uses. (But note that the monad 'm' has to be the same all the way. You can't switch from, say, IO to ST in the middle of the computation.) Likewise, Contrariwise, I'd say. ghci :t (+) (+) :: (Num a) = a - a - a I.e. (+) requires the same type on both sides... fromIntegral ((1 :: Int) + 2) + (3 :: Integer) 6 ...but 'fromIntegral' converts it. Did I miss some subtle point here? I was talking about the types of the two + applications. They have a different types, just like the = in the parent's message can have different types. My fromIntegral has a role similar to the read s :: Int of the original question. Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: is proof by testing possible?
That has got to be the single awesomest thing I have ever seen ever... The first time I tried to read through the Seemingly Impossible Functional Programs post, I understood none of it. Now it seems obviously. I Love Math... Thanks for the explanation! /Joe On Oct 12, 2009, at 3:22 PM, Ben Franksen wrote: Joe Fredette wrote: Really? How? That sounds very interesting, I've got a fair knowledge of basic topology, I'd love to see an application to programming... Compactness is one of the most powerful concepts in mathematics, because on the one hand it makes it possible to reduce many infinite problems to finite ones (inherent in its definition: for every open cover there is a finite subcover), on the other hand it is often easy to prove compactness due to Tychonoff's theorem (any product of compact spaces is compact). The connection to computing science is very nicely explained in http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ I found this paragraph particularly enlightening: modulus :: (Cantor - Integer) - Natural modulus f = least(\n - forevery(\a - forevery(\b - eq n a b -- (f a == f b This [...] finds the modulus of uniform continuity, defined as the least natural number `n` such that `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` where `alpha =_n beta iff forall i n. alpha_i = beta_i.` What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). Cheers ___ 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] is proof by testing possible?
Neil Brown nc...@kent.ac.uk writes: swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) swap = undefined Terminates and does not swap its arguments :-) I think this counts as non-termination, and that for semantic purposes, any bottom value -- infinite loops, exceptions, undefined -- is treated equally. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Could that nice precise formulation simply be Scott continuity, which in turn preserves compactness through composition and under application? Dan Piponi wrote: On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown nc...@kent.ac.uk wrote: swap = undefined Terminates and does not swap its arguments :-) What do free theorems say about this, exactly -- do they just implicitly exclude this possibility? I'm terrible at reasoning about functions with bottoms (ie. undefined or non-termination). But I suspect that a property like this holds: if the type signature of a function f is polymorphic in a, and it doesn't produce bottom for one particular value x of type a, for some particular type a, f can never produce bottom for any choice of x in any choice of type a. (Which is not to say it might not fail, but that the failure will be an issue with x, not f.) The intuition behind this is that if a function is polymorphic in a then it never examines the a. So even if a is bottom, the function can never know it. But it could fail because f additionally accepts as argument a polymorphic function that itself accepts a's, and that fails. But then it wouldn't be f's fault, it'd be the fault of the function you passed in. This is very poor of me. There's probably a nice precise formulation of what I've just said :-) -- Dan ___ 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] Sharing Subexpressions: Memoization of Fibonacci sequence
On Mon, Oct 12, 2009 at 11:52:30AM -0700, SimonK77 wrote: **Edit: formatting was bad** Hallo everyone, the last few weeks I was trying to get used to memoization in haskell. As I found out in a previous post, memoization in haskell is, due to the graph reduction strategy used in haskell, almost always implemented by sharing subexpressions in an expression. In examples as the following this is quite easy to see. fibs = 0:1:zipWith (+) fibs (tail fibs) But as I browsed through the search results from google for this topic, I encountered the following implementation: memoized_fib :: Int - Integer memoized_fib = let fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) in (map fib [0 ..] !!) ... I can't see where the sharing of subexpressions happens here. Any help is highly appreciated. This is an excellent and subtle question. The sharing behavior of the code depends on the desugaring of the syntax (map fib [0 ..] !!): is it (!!) (map fib [0 ..]) or (\x - map fib [0 ..] !! x) I suggest, as an exercise, tracing the evaluation of memoized_fib using each of these desugarings, and then trying them out in ghci. Then you'll be able to tell which desugaring ghc is using. (It's not the one used in the Report! In principle this is a bug since we can distinguish them using seq.) Regards, Reid Barton ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sharing Subexpressions: Memoization of Fibonacci sequence
Am Montag 12 Oktober 2009 21:09:38 schrieb minh thu: 2009/10/12 SimonK77 simonkaltenbac...@googlemail.com: **Edit: formatting was bad** Hallo everyone, the last few weeks I was trying to get used to memoization in haskell. As I found out in a previous post, memoization in haskell is, due to the graph reduction strategy used in haskell, almost always implemented by sharing subexpressions in an expression. In examples as the following this is quite easy to see. fibs = 0:1:zipWith (+) fibs (tail fibs) But as I browsed through the search results from google for this topic, I encountered the following implementation: memoized_fib :: Int - Integer memoized_fib = let fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) in (map fib [0 ..] !!) You'll find it at Haskell.org. Here's the http://www.haskell.org/haskellwiki/Memoization link Let's assume we have the following implementation of the higher-order-function map: map :: (a - b) - [a] - [b] map _ [] = [] map f (x:xs) = f x : map f xs The reduction sequence of memoized_fib 5 would start as follows: //Reduction of memoized_fib 5 memoized_fib 5 = (map fib [0..] !!) 5 = (fib 0 : map fib [1..] !!) 5 = (0 : fib 1 : map fib [2..] !!) 5 = (0 : 1 : fib 2 : map fib [3..] !!) 5 = (0 : 1 : (memoized_fib 0 + memoized_fib 1) : fib 3 : map fib [4..] !!) 5 = (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) : (memoized_fib 1 + memoized_fib 2) : map fib [4..] !!) 5 . . . . and so on! Hi, Instead of repeating as-is map fib [0..] consider it as a single list that is always reused. Since the list maps the input of the fib function to the result of the function and that list is always reused, the recursive calls have immediately the answer (i.e. at the cost of the lookup). Yes, since memoized_fib is bound by a simple pattern binding and not a function binding, the list is shared among different invocations of memoized_fib, same as if it was given an explicit name. You can see it by adding tracing output: import Debug.Trace tfib :: Int - Integer tfib = let fib 0 = 0 fib 1 = 1 fib n = trace (eval fib ++ show n) $ tfib (n-2) + tfib (n-1) in (map fib [0 .. ] !!) *MFib tfib 6 eval fib 6 eval fib 4 eval fib 2 eval fib 3 eval fib 5 8 (0.00 secs, 538564 bytes) *MFib tfib 10 eval fib 10 eval fib 8 eval fib 7 eval fib 9 55 (0.00 secs, 0 bytes) So your fragment (0 : 1 : (map fib [0..] !! 0 + map fib [0..] !! 1) ... should look like lst = (0 : 1 : (lst !! 0 + lst !! 1) ... which is similar to the zipWith (+) version. Except it's much slower. Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple program. Simple problem?
On Mon, Oct 12, 2009 at 1:08 AM, Felipe Lessa felipe.le...@gmail.comwrote: On Mon, Oct 12, 2009 at 12:42:16AM +0200, Peter Verswyvelen wrote: btw I always find it amusing to play with interact and lazy IO: I always find it frightening to play with lazy IO :). yes, I guess that's why I like it, because I'm still an imperative / OO programmer ;-) -- Felipe. ___ 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
[Haskell-cafe] Re: Re: is proof by testing possible?
Joe Fredette wrote: That has got to be the single awesomest thing I have ever seen ever... I was dumbfounded, too, when I first read about this. BTW, and completely off-topic: if you like this, you might have fun too with Conor McBride's discovery that data types can be differentiated, and the result is even useful: it corresponds to what is known (to some) as a Zipper: http://www.cs.nott.ac.uk/~ctm/diff.pdf Moreover, we can also give a sensible and useful interpretation to finite difference quotients of types: http://blog.sigfpe.com/2009/09/finite-differences-of-types.html which McBride calls dissections and discusses in some depth here: http://strictlypositive.org/CJ.pdf What is most astonishing to me is that these constructions work even though there is neither subtraction nor division defined on data types, only addition and multiplication (there are neutral elements for both, but not necessarily inverses). Cheers Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Re: What *is* a DSL?
S. Doaitse Swierstra wrote:
This problem of dynamically transforming grammars and bulding parsers
out of it is addressed in:
@inproceedings{1411296,
author = {Viera, Marcos and Swierstra, S. Doaitse and Lempsink,
Eelco},
title = {Haskell, do you read me?: constructing and composing
efficient top-down parsers at runtime},
[...]
}
Indeed, it looks as if you solved exactly the problem that vexed me! I had
just found the presentation that corresponds to the paper you mention, and
I also found a preprint for Typed transformations of Typed Abstract
Syntax which I am studying at the moment. I must say your construction is,
well, involved...
Not that I want to belittle this really astounding and clever achievement...
but one disadvantage of your approach (which it shares with almost all
examples I have seen for dependently typed or heterogeneous collections) is
that (IIUC) the typed map from references to abstract syntactic terms is
operationally an association list, indexed by unary numbers. I would expect
this to scale poorly if the number of references (e.g. nonterminals) gets
large.
I think it would make for quite an interesting research project to study
whether it is possible to achieve the same level of precise static typing
with more efficient data structures. I imagine that using some 'fake
dependent type' variant of [Bit] for the key and the equivalent of a
patricia tree for the map could perhaps be made to work???
Cheers
Ben
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Re: is proof by testing possible?
I read about differentiating and differences for types, that was awesome, but when I read the seemingly-impossible post the first time, I didn't have enough background in topology to understand what was going on. Differentiating types is usually how I introduce the power of haskell's type system to the other students in my Math department. I actually showed my algebra professor how non-recursive datatypes in n-variables are just multinomials over a commutative (up to isomorphism) ring and how you can use that to reason about equivalences between types based on the polynomial they're isomorphic too. My Algebra Professor, who does not program and knows very little about it, sat back in his chair and say, So that's what all the fuss is about? Programming is easy! Really, all this goes to show that a rich, algebraic type system like Haskell's is invaluable because it harnesses the power of mathematics that we've been working at for years. Free Theorems indeed! On Oct 12, 2009, at 4:45 PM, Ben Franksen wrote: Joe Fredette wrote: That has got to be the single awesomest thing I have ever seen ever... I was dumbfounded, too, when I first read about this. BTW, and completely off-topic: if you like this, you might have fun too with Conor McBride's discovery that data types can be differentiated, and the result is even useful: it corresponds to what is known (to some) as a Zipper: http://www.cs.nott.ac.uk/~ctm/diff.pdf Moreover, we can also give a sensible and useful interpretation to finite difference quotients of types: http://blog.sigfpe.com/2009/09/finite-differences-of-types.html which McBride calls dissections and discusses in some depth here: http://strictlypositive.org/CJ.pdf What is most astonishing to me is that these constructions work even though there is neither subtraction nor division defined on data types, only addition and multiplication (there are neutral elements for both, but not necessarily inverses). Cheers Ben ___ 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
[Haskell-cafe] Need help with ghc static compile for cgi using mysql
I'm trying to host a cgi I've written. It uses Database.HDBC, Database.HDBC.MySQL, Network.CGI, and Text.XHtml.Transitional Here is the command I'm using to compile ghc --make -optl-static -optl-pthread -static -o test.cgi -package cgi -package xhtml -package HDBC-mysql -package HDBC -optl -lz Main.hs and I get (.text+0x120): undefined reference to `compress' Searching around I found that mysql recommended passing lz to the linker... so I added -optl -lz Complete command and output: ghc --make -optl-static -optl-pthread -static -o test.cgi -package cgi -package xhtml -package HDBC-mysql -package HDBC -optl -lz Main.hs [1 of 5] Compiling Config ( Config.hs, Config.o ) [2 of 5] Compiling Model( Model.hs, Model.o ) [3 of 5] Compiling View ( View.hs, View.o ) [4 of 5] Compiling Controller ( Controller.hs, Controller.o ) [5 of 5] Compiling Main ( Main.hs, Main.o ) Linking test.cgi ... /opt/ghc-6.10.4/lib/ghc-6.10.4/network-2.2.1.2/libHSnetwork-2.2.1.2.a(HsNet.o): In function `my_inet_ntoa': HsNet.c:(.text+0x20): multiple definition of `my_inet_ntoa' /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(my_net.o):(.text+0x0): first defined here /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(mf_pack.o): In function `unpack_dirname': (.text+0x75b): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(libmysql.o): In function `read_user_name': (.text+0x6081): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(mf_pack.o): In function `unpack_dirname': (.text+0x76a): warning: Using 'endpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /opt/ghc-6.10.4/lib/ghc-6.10.4/network-2.2.1.2/libHSnetwork-2.2.1.2.a(HsNet.o): In function `hsnet_getaddrinfo': HsNet.c:(.text+0x15): warning: Using 'getaddrinfo' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(ssl.o): In function `yaSSL::read_file(yaSSL::SSL_CTX*, char const*, int, yaSSL::CertType)': (.text+0x29f3): warning: memset used with constant zero length parameter; this could be due to transposed parameters /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(my_gethostbyname.o): In function `my_gethostbyname_r': (.text+0x3c): warning: Using 'gethostbyname_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /opt/ghc-6.10.4/lib/ghc-6.10.4/network-2.2.1.2/libHSnetwork-2.2.1.2.a(BSD__213.o): In function `s9bc_info': (.text+0x55): warning: Using 'getprotobyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(libmysql.o): In function `mysql_server_init': (.text+0x6b22): warning: Using 'getservbyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(my_compress.o): In function `my_uncompress': (.text+0x6b): undefined reference to `uncompress' /usr/lib/gcc/i486-linux-gnu/4.3.3/../../../../lib/libmysqlclient.a(my_compress.o): In function `my_compress_alloc': (.text+0x120): undefined reference to `compress' collect2: ld returned 1 exit status I'm using ghc 6.10.4 on Ubuntu 9.04 i386 I have libmysqlclient15-dev installed Thanks, Austin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Stupid error, probably
I can't get the following to work in Leksah - but it works OK in GHC. Can anyone spot the error? I wondered if it was becasue the libraries loaded are different - but I'm just a Haskell beginner ... I have: myGroupBy :: Int→ [a]→ [[a]] myGroupBy = takeWhile not . null . (unfoldr (Just . (splitAt 3))) and I am getting the error: Couldn't match expected type `Int' against inferred type `[a]' In the second argument of `(.)', namely `(splitAt 3)' In the first argument of `unfoldr', namely `(Just . (splitAt 3))' In the second argument of `(.)', namely `(unfoldr (Just . (splitAt 3)))' But I think that splitAt :: Int-[a]-([a],[a]) so: splitAt 3 :: [a]-([a], [a]) and: Just.(splitAt 3) :: [a]-Maybe ([a], [a]) which seems OK as the first argument of unfoldr: unfoldr :: (b- Maybe(a,b))-b-[a] with the a and b of unfoldr being [a] and [a]. The mention of Int in the error makes me wonder if I've got the wrong splitAt - with the arguments reversed maybe. Any ideas? Thanks. N ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Stupid error, probably
Am Dienstag 13 Oktober 2009 01:03:24 schrieb b1g3ar5: I can't get the following to work in Leksah - but it works OK in GHC. Can anyone spot the error? I wondered if it was becasue the libraries loaded are different - but I'm just a Haskell beginner ... I have: myGroupBy :: Int→ [a]→ [[a]] ^^ That Int isn't used in the definition of myGroupBy perhaps you intended to write myGroupBy k = takeWhile (not . null) . unfoldr (Just . splitAt k) ? myGroupBy = takeWhile not . null . (unfoldr (Just . (splitAt 3))) and I am getting the error: Couldn't match expected type `Int' against inferred type `[a]' In the second argument of `(.)', namely `(splitAt 3)' In the first argument of `unfoldr', namely `(Just . (splitAt 3))' In the second argument of `(.)', namely `(unfoldr (Just . (splitAt 3)))' But I think that splitAt :: Int-[a]-([a],[a]) so: splitAt 3 :: [a]-([a], [a]) and: Just.(splitAt 3) :: [a]-Maybe ([a], [a]) which seems OK as the first argument of unfoldr: unfoldr :: (b- Maybe(a,b))-b-[a] with the a and b of unfoldr being [a] and [a]. The mention of Int in the error makes me wonder if I've got the wrong splitAt - with the arguments reversed maybe. Any ideas? Thanks. N ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: What *is* a DSL?
On Sun, Oct 11, 2009 at 06:29:58PM -0400, Brandon S. Allbery KF8NH wrote: On Oct 11, 2009, at 18:00 , Ben Franksen wrote: Ben Franksen wrote: Ben Franksen wrote: Next thing I'll try is to transform such a grammar into an actual parser... Which I also managed to get working. First, before all this talking to myself here is boring you to death, please shout and I'll go away. Anyway, at least one person has privately expressed interest, so I'll post my code for the translation.(*) It's -cafe, so let 'er rip. And maybe write it up for TMR, if you don't Yes please! =) -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Do you know any category theory? What helped me finally grok free theorems is that in the simplest cases, the free theorem for a polymorphic function is just a naturality condition. For example, the free theorem for flatten :: Tree a - [a] is precisely the statement that flatten is a natural transformation from the Tree functor to the list functor: fmap_[] g . flatten == flatten . fmap_Tree g It gets more complicated than this, of course, but that's the basic idea. -Brent On Mon, Oct 12, 2009 at 02:03:11PM -0400, Joe Fredette wrote: I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. /Joe On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. not True==False not False==True Done. Tested :-) Less trivially, consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) - (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) - (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.) -- Dan ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] MTL vs Transformers?
Hi all, I've just received the following error message: headers.hs:6:7: Could not find module `Control.Monad.Identity': it was found in multiple packages: transformers-0.1.4.0 mtl-1.1.0.2 I'm trying to use the Iteratee module which depends on Transformers but I use MTL in other stuff. Whats the preferred solution here? Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] MTL vs Transformers?
ghc-pkg hide transformers On Oct 12, 2009, at 5:46 PM, Erik de Castro Lopo wrote: Hi all, I've just received the following error message: headers.hs:6:7: Could not find module `Control.Monad.Identity': it was found in multiple packages: transformers-0.1.4.0 mtl-1.1.0.2 I'm trying to use the Iteratee module which depends on Transformers but I use MTL in other stuff. Whats the preferred solution here? Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ 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] MTL vs Transformers?
Erik de Castro Lopo wrote: Gregory Crosswhite wrote: ghc-pkg hide transformers Here's an example. CGI uses MTL, Iteratee uses Transformers. So, how do you use CGI and Iteratee in the same program? CGI is just one of many examples. Text.Regex, Network.HTTP, Database.HDBS.Sqlite, Tagsoup are others. Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
Sadly not enough, I understand the basics, but the whole proof = this diagram commutes thing still seems like voodoo to me. There is a section coming up in my Topology ISP that will be on CT. So I hope that I will be able to gain some purchase on the subject, at least enough to build up a working understanding on my own. I have a practical understanding of Functors and Natural Transformations, so working a bit with these free theorem things is kind of fun. Actually, another germane-if-random question, why isn't there a natural transformation class? Something like: class Functor f, Functor g = NatTrans g f a where trans :: f a - g a So your flatten function becomes a `trans` a la instance NatTrans Tree [] a where trans = flatten In fact, I'm going to attempt to do this now... Maybe I'll figure out why before you reply. :) /Joe On Oct 12, 2009, at 8:41 PM, Brent Yorgey wrote: Do you know any category theory? What helped me finally grok free theorems is that in the simplest cases, the free theorem for a polymorphic function is just a naturality condition. For example, the free theorem for flatten :: Tree a - [a] is precisely the statement that flatten is a natural transformation from the Tree functor to the list functor: fmap_[] g . flatten == flatten . fmap_Tree g It gets more complicated than this, of course, but that's the basic idea. -Brent On Mon, Oct 12, 2009 at 02:03:11PM -0400, Joe Fredette wrote: I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. /Joe On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. not True==False not False==True Done. Tested :-) Less trivially, consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) - (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) - (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.) -- Dan ___ 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 ___ 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] MTL vs Transformers?
Ugh, I'm not as sure about that... it took me long enough just to figure out ghc-pkg hide transformers! :-) Are running into problems because you need to refer to both packages (e.g., mtl and transformers) within your code, or because you are using packages that refer to each? Because as long as you only need to refer to one of them in your own code, GHC should be able to handle the dependencies for the other packages correctly. (Hiding the package only removes it from being automatically imported by your own code, it doesn't prevent it from being used by other packages that link to it.) Cheers, Greg On Oct 12, 2009, at 6:08 PM, Erik de Castro Lopo wrote: Gregory Crosswhite wrote: ghc-pkg hide transformers Here's an example. CGI uses MTL, Iteratee uses Transformers. So, how do you use CGI and Iteratee in the same program? Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ 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] is proof by testing possible?
I fiddled with my previous idea -- the NatTrans class -- a bit, the results are here[1], I don't know enough really to know if I got the NT law right, or even if the class defn is right. Any thoughts? Am I doing this right/wrong/inbetween? Is there any use for a class like this? I listed a couple ideas of use-cases in the paste, but I have no idea of the applicability of either of them. /Joe http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10679#a10679 On Oct 12, 2009, at 8:41 PM, Brent Yorgey wrote: Do you know any category theory? What helped me finally grok free theorems is that in the simplest cases, the free theorem for a polymorphic function is just a naturality condition. For example, the free theorem for flatten :: Tree a - [a] is precisely the statement that flatten is a natural transformation from the Tree functor to the list functor: fmap_[] g . flatten == flatten . fmap_Tree g It gets more complicated than this, of course, but that's the basic idea. -Brent On Mon, Oct 12, 2009 at 02:03:11PM -0400, Joe Fredette wrote: I completely forgot about free theorems! Do you have some links to resources -- I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. /Joe On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote: On Mon, Oct 12, 2009 at 10:42 AM, muad muad.dib.sp...@gmail.com wrote: Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition. not True==False not False==True Done. Tested :-) Less trivially, consider a function of signature swap :: (a,b) - (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) - (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) - (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.) -- Dan ___ 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 ___ 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] is proof by testing possible?
On Mon, Oct 12, 2009 at 8:15 PM, Joe Fredette jfred...@gmail.com wrote: Sadly not enough, I understand the basics, but the whole proof = this diagram commutes thing still seems like voodoo to me. There is a section coming up in my Topology ISP that will be on CT. So I hope that I will be able to gain some purchase on the subject, at least enough to build up a working understanding on my own. I have a practical understanding of Functors and Natural Transformations, so working a bit with these free theorem things is kind of fun. Actually, another germane-if-random question, why isn't there a natural transformation class? Something like: class Functor f, Functor g = NatTrans g f a where trans :: f a - g a So your flatten function becomes a `trans` a la instance NatTrans Tree [] a where trans = flatten In fact, I'm going to attempt to do this now... Maybe I'll figure out why before you reply. :) Diagrams are just a graphical depiction of systems of equations. Every pair of paths with the same start and end point are equal. I don't care for diagrams that much and that graphical depiction isn't that important for CT, though it has some mnemonic value. As for a NatTrans class, your example is broken in several ways. Natural transformations, though, are trivial in Haskell. type NatTrans f g = forall a. f a - g a flatten :: NatTrans Tree [] I.e. a natural transformation between Haskell Functors are just polymorphic functions between them. In general, a polymorphic function is a dinatural transformation and the dinaturality conditions are the free theorems (or at least, special cases of the free theorem for the type, which I believe, but haven't proven, implies the full free theorem.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] MTL vs Transformers?
Gregory Crosswhite wrote: Are running into problems because you need to refer to both packages (e.g., mtl and transformers) within your code, or because you are using packages that refer to each? The later. Iteratee uses Transformers and just about everything else I want to use uses MTL. Because as long as you only need to refer to one of them in your own code, GHC should be able to handle the dependencies for the other packages correctly. (Hiding the package only removes it from being automatically imported by your own code, it doesn't prevent it from being used by other packages that link to it.) That all seems a little hackish. However after reading the hackage descriptions of both Transformers and MTL, it seems that they share a very similar heritage. I therefore hacked the iteratee.cabal file and replaced the build-depends on transformers with one on mtl and the package built quite happily. I'll play with it a bit to see if its working correctly. Cheers, Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Parsec bug, or...?
a brain fart? Hi, cafe, I've been playing a little bit with a small command processor, and I decided it'd be nice to allow the user to not have to enter a complete command, but to recognize a unique prefix of it. So I started with the list of allowed commands, used filter and isPrefixOf, and was happy. But then I increased the complexity a little bit and it got hairier, so I decided to rewrite the parser for this bit in parsec. The function I came up with is parsePrefixOf n str = string (take n str) opts (drop n str) return str where opts [] = return () opts (c:cs) = optional (char c opts cs) which I call as parseFoo = parsePrefixOf 1 foo and it recognizes all of f, fo, and foo as foo. OK so far, this also seems to work fine. But during the course of writing this, I made a stupid mistake at one point, and the result of that seemed odd. Consider the following program. It's stupid because the required prefix of frito is only 2 characters, which isn't enough to actually distinguish this from the next one, fromage. (And if I change that to 2 to 3 characters, everything works fine.) So here's the complete program module Main where import Prelude import System import Text.ParserCombinators.Parsec as TPCP myPrefixOf n str = string (take n str) opts (drop n str) return str where opts [] = return () opts (c:cs) = optional (char c opts cs) myTest = myPrefixOf 1 banana | myPrefixOf 1 chocolate | TPCP.try (myPrefixOf 2 frito) | myPrefixOf 3 fromage myBig = spaces myTest = (\g - spaces eof return g) parseTry input = case parse myBig test input of Left err - return (show err) Right val - return (success: ' ++ val ++ ') main = getArgs = (\a - parseTry (a !! 0)) = putStrLn If I compile this, say as program opry, and run it as shown below, I expect the results I get for all but the last one: % ./opry b success: 'banana' % ./opry c success: 'chocolate' % ./opry fr success: 'frito' % ./opry fri success: 'frito' % ./opry fro test (line 1, column 3): unexpected o expecting i, white space or end of input Sooo... why do I get that last one? My expectation was that parsec would try the string fro with the parser for frito, it would fail, having consumed 2 characters, but then the TPCP.try which is wrapped around all of that should restore everything, and then the final parser for fromage should succeed. The same reasoning seems to me to apply if I specify 3 characters as the required initial portion for frito, and if I do that it does succeed as I expect. So is this a bug in parsec, or a bug in my brain? thanks... Uwe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] QuickCheck2 question
I'm having some trouble with QuickCheck2 and Control.Applicative.
Specifically, I have the following functions (slightly simplified):
copyVector :: IOVector - Vector - IO ()
freezeVector :: IOVector - IO (Vector)
I have a test, part of which looks like
monadicIO $ do
run $ copyVector $ pure dst * freezeVector src
-- more stuff...
When I try running the test (using test-framework-quickcheck2), the
`copyVector` function never gets called.
If I re-write the test as
monadicIO $ do
src' - run $ freezeVector
run $ copyVector dst src'
-- etc.
then everything works fine (i.e., the call to `copyVector` gets executed).
Does anyone have any clues as to what is going on? I suspect the problem is
related to Test.QuickCheck.Monadic using `unsafePerformIO` without a `{-#
NOINLINE -#}` pragma [1], but I'm not completely sure. Adding such a pragma to
`monadicIO` and `run` in Monadic.hs does not fix the problem.
I'm using Quickcheck-2.1.0.2 and GHC 6.10.1.
Thanks in advance for any help,
Patrick
[1]
http://hackage.haskell.org/packages/archive/QuickCheck/2.1.0.2/doc/html/src/Test-QuickCheck-Monadic.html
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec bug, or...?
On Oct 12, 2009, at 22:28 , Uwe Hollerbach wrote: parsePrefixOf n str = string (take n str) opts (drop n str) return str where opts [] = return () opts (c:cs) = optional (char c opts cs) Seems to me this will succeed as soon as it possibly can... myTest = myPrefixOf 1 banana | myPrefixOf 1 chocolate | TPCP.try (myPrefixOf 2 frito) | myPrefixOf 3 fromage ...so the frito branch gets committed as soon as fr is read/parsed (myTest returns)... % ./opry fro test (line 1, column 3): unexpected o expecting i, white space or end of input ...which is why this is looking for white space or end of input. My fix would be to have myPrefixOf require the prefix be terminated in whatever way is appropriate (end of input, white space, operator?) instead of simply accepting as soon as it gets a prefix match regardless of what follows. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec bug, or...?
On 10/12/09, Derek Elkins derek.a.elk...@gmail.com wrote: On Mon, Oct 12, 2009 at 9:28 PM, Uwe Hollerbach uhollerb...@gmail.com wrote: a brain fart? Hi, cafe, I've been playing a little bit with a small command processor, and I decided it'd be nice to allow the user to not have to enter a complete command, but to recognize a unique prefix of it. So I started with the list of allowed commands, used filter and isPrefixOf, and was happy. But then I increased the complexity a little bit and it got hairier, so I decided to rewrite the parser for this bit in parsec. The function I came up with is parsePrefixOf n str = string (take n str) opts (drop n str) return str where opts [] = return () opts (c:cs) = optional (char c opts cs) which I call as parseFoo = parsePrefixOf 1 foo and it recognizes all of f, fo, and foo as foo. OK so far, this also seems to work fine. But during the course of writing this, I made a stupid mistake at one point, and the result of that seemed odd. Consider the following program. It's stupid because the required prefix of frito is only 2 characters, which isn't enough to actually distinguish this from the next one, fromage. (And if I change that to 2 to 3 characters, everything works fine.) So here's the complete program module Main where import Prelude import System import Text.ParserCombinators.Parsec as TPCP myPrefixOf n str = string (take n str) opts (drop n str) return str where opts [] = return () opts (c:cs) = optional (char c opts cs) myTest = myPrefixOf 1 banana | myPrefixOf 1 chocolate | TPCP.try (myPrefixOf 2 frito) | myPrefixOf 3 fromage myBig = spaces myTest = (\g - spaces eof return g) parseTry input = case parse myBig test input of Left err - return (show err) Right val - return (success: ' ++ val ++ ') main = getArgs = (\a - parseTry (a !! 0)) = putStrLn If I compile this, say as program opry, and run it as shown below, I expect the results I get for all but the last one: % ./opry b success: 'banana' % ./opry c success: 'chocolate' % ./opry fr success: 'frito' % ./opry fri success: 'frito' % ./opry fro test (line 1, column 3): unexpected o expecting i, white space or end of input Sooo... why do I get that last one? My expectation was that parsec would try the string fro with the parser for frito, it would fail, having consumed 2 characters, but then the TPCP.try which is wrapped around all of that should restore everything, and then the final parser for fromage should succeed. The same reasoning seems to me to apply if I specify 3 characters as the required initial portion for frito, and if I do that it does succeed as I expect. So is this a bug in parsec, or a bug in my brain? Move the try to the last alternative. No, that doesn't do it... I get the same error (and also the same if I wrap both alternatives in try). Uwe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Why MTL and Transformers?
Something that I have been wondering for a while is: why are there *still* two monad transformer libraries with seemingly identical functionality, especially given that they have conflicting namespaces? It creates stupid problems like the one that Erik encountered and had to work around. I recognize that this situation most likely came about via historical accident rather than by intention, but why does it continue to be true? Cheers, Greg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-level naturals multiplication
Reid Barton: On Sat, Oct 10, 2009 at 02:59:37PM -0400, Brad Larsen wrote: Suppose we implement type-level naturals as so: data Zero data Succ a Then, we can reflect the type-level naturals into a GADT as so (not sure if ``reflect'' is the right terminology here): data Nat :: * - * where Zero :: Nat Zero Succ :: Nat a - Nat (Succ a) Using type families, we can then proceed to define type-level addition: type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) Is there any way to define type-level multiplication without requiring undecidable instances? I hesitate to contradict Manuel Chakravarty on this subject... but I posted a type-level multiplication program without undecidable instances on this list in June: http://www.haskell.org/pipermail/haskell-cafe/2009-June/062452.html If you prefer to use EmptyDataDecls, you can replace the first four lines by data Z data S n data Id :: * - * data (:.) :: (* - *) - (* - *) - (* - *) And I still don't understand why that definition works while the obvious one doesn't :) Ok, I should have been more precise. It's not that anything about multiplication as such is a problem. However, when you look at the standard definitions for addition type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) and multiplication type family Mul a b :: * type instance Mul Zero b = Zero type instance Mul (Succ a) b = Add (Mul a b) b then the difference is that multiplication uses nested applications of type families (namely, Add (Mul a b) b). It is this nested application of type families that can be abused to construct programs that lead to non-termination of type checking (by exploiting the openness of type families in combination with local equalities introduced either by equality constraints in type signatures or GADT pattern matches). Unfortunately, there doesn't seem to be a simple syntactic criterion that would let GHC decide between harmless and problematic uses of nested *open* family applications in family instances. Hence, we need to rule them all out. You circumvent that problem cleverly by the use of higher-kinded types. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Graph Library Using Associated Types
Lajos Nagy: I understand that one of the original motivations for introducing associated types to Haskell was the survey of support for generic programming done by Garcia et al. where they compared the implementation of the Boost Graph Library in various languages (C++, Java, Haskell, ML, C#, Eiffel). Haskell got full marks in all categories, except for associated types which made the resulting implementations more verbose than necessary (and exposed implementation details). Since then GHC added support for associated types but I was wondering if anybody re-did the experiment with the new features enabled (the original code is available at: http://www.osl.iu.edu/research/comparing/). No, we actually didn't do that. It would be interesting, though. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
