Re: [Haskell-cafe] STM and random numbers
On Sat, Jan 13, 2007 at 01:49:36PM +1000, Matthew Brecknell wrote: Rather than having a separate thread computing the random numbers using IO, why not just stick an StdGen in a TVar and write a function like: type RandomVar = TVar StdGen rnd :: RandomVar - STM a rnd var = do g - readTVar var let (r,g') = random g writeTVar var g' return r The user of this approach should be aware that it may lead to non-determinism. That is, the sequence of psuedo-random numbers extracted by any one thread will depend on those extracted by other threads, which may in turn depend on the scheduling of those threads. The TVar approach might also lead to excessive STM transaction abort-retry cycles, if multiple threads are retrieving many pseudo-random numbers via a single TVar. As a workaround for these problems you can create a separate RandomVar for each atomically block. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Are GADTs expressive? Simple proof-carrying code in Haskell98
Inspired by the recent post by Jim Apple, we demonstrate a datatype
`Terminates' that can hold only an assuredly terminating (strongly
normalizable) term in untyped lambda-calculus. Furthermore, the values
of the datatype `Terminates' contain all and only those untyped
lambda-calculus terms with that property. As in Jim Apple's solution,
to create the value `Terminates', the user submits the term in
question and the proof of its termination. The proof will be verified
-- and if it holds, the Terminates certificate will be created. As in
Jim Apple's solution, verification of the submitted proof has to be
done at run-time, to make sure the proof is not fake, that is, has no
undefined values. Our solution uses neither GADTs nor typeclasses; in
fact, it is in Haskell98. Also, the required proof from the user
couldn't be simpler.
Jim Apple wrote:
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
The shown GADT encoding seems to be of the kind that is convertible to
typeclasses in the straightforward way, see for example,
http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs
Inn this particular example, GADT do not bring any
power. Incidentally, the typeclass encoding has an advantage: If the
submitted proof is invalid, the error will be reported at compile
time. There is not even a possibility of a run-time error. This is
because the typeclasses approach does only type-level computations and
does not look at values at all (which may as well be
undefined). Placing a value into a (rank-1) datatype forces the
typechecker to resolve any constraints associated with the value, or
report an error if constraints are not satisfiable.
However, it seems that the problem at hand admits a far simpler
solution -- in Haskell98. The solution is in spirit of lightweight
static capabilities. Here it is:
module PCC (Terminates, -- data constructor is not exported
make_terminates, get_term) where
import YourFavorite.Lambda_calc
data Terminates = Terminates{get_term::Term}
make_terminates :: Term - Integer - Maybe Terminates
make_terminates term limit =
case reduce_term_nsteps term limit of
Left _ - Nothing
Right normal_form - Just (Terminates term)
Because the data constructor is not exported, the only way to
construct a value `Terminates' from which a term can be extracted is
by invoking the function make_terminates. The function accepts a
lambda-term, and a proof of its termination. The proof takes the form
of the (upper bound of the) number of steps needed to normalize the
term. The function make_terminates checks the proof, by trying to
reduce the term that many steps. If the normal form is found in the
process, the term is normalizable and we create the
certificate. Otherwise, we conclude the termination proof does not
hold and we return Nothing. This proof checking is clearly decidable.
The module PCC constitutes the `trusted kernel' with respect to the
Terminates datatype. The function make_terminates must be rigorously
verified in order to deserve our trust. But the same should be said
for the GADT or any other solution: e.g., one can easily add a new
case alternative to the Normal datatype declaring Omega to be in the
normal form.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] strange performance of expression evaluators
On Sat, Jan 13, 2007 at 11:44:38AM +1000, Matthew Brecknell wrote:
So my advice here would be: always try the optimiser before you worry
too much about strange performance!
Thanks for help!
I've done some more experiments. The following program defines simple
arithmetic expression with indexed variables. I've written four
different ways to evaluate them:
- eval1 is simple monadic evaluator
- eval2 is the obvious straight-forward implentation
- compile1 is attempt to perform compilation
- compile2 is refined compile1 with sub-expressions explicitely
separated via let binding.
Test evaluates the same expression in 100 different environments.
The results are:
- eval1 - 17.47 sec
- eval2 - 3.71 sec
- compile1 - 3.79 sec
- compile2 - 3.74 sec
This figures are completely mysterious for me.
1) I expected eval1 and eval2 to perform equally. In fact, eval1 is
4.7 times slower for eval2.
2) I expected compile{1,2} to perform much faster then eval{1,2}.
However, the compilation attempt does not give any speed up at
all.
Can anyone explain these results?
Program was compiled with ghc -O3 -fexcess-precision command.
For comparison, I wrote simple straight-forward implementation of
compile2 in C++. It runs approximately 1.04 sec (3.57 better than
Haskell).
import Data.Array.Unboxed
import Data.Array.Base
import Control.Monad.Reader
import Data.Int
foldl' f z [] = z
foldl' f z (x:xs) = (foldl' f $! f z x) xs
type Value = Int32
data Expr = Const !Value | Var !Int | Add !Expr !Expr | Sub !Expr !Expr | Mul
!Expr !Expr
type Env = UArray Int Value
eval1 :: Expr - Reader Env Value
eval1 e =
case e of
Const c - return c
Var n - do { env - ask; return $ env ! n }
Add e1 e2 - do
v1 - eval1 e1
v2 - eval1 e2
return $ v1 + v2
Sub e1 e2 - do
v1 - eval1 e1
v2 - eval1 e2
return $ v1 - v2
Mul e1 e2 - do
v1 - eval1 e1
v2 - eval1 e2
return $ v1 * v2
eval2 :: Expr - Env - Value
eval2 e env =
case e of
Const c - c
Var n - env ! n
Add e1 e2 - eval2 e1 env + eval2 e2 env
Sub e1 e2 - eval2 e1 env - eval2 e2 env
Mul e1 e2 - eval2 e1 env * eval2 e2 env
compile1 :: Expr - (Env - Value)
compile1 e =
case e of
Const c - \env - c
Var n - \env - env ! n
Add e1 e2 - \env - (compile1 e1) env + (compile1 e2) env
Sub e1 e2 - \env - (compile1 e1) env - (compile1 e2) env
Mul e1 e2 - \env - (compile1 e1) env * (compile1 e2) env
compile2 :: Expr - (Env - Value)
compile2 e =
case e of
Const c - \env - c
Var n - \env - env ! n
Add e1 e2 - let c1 = compile2 e1 in
let c2 = compile2 e2 in
\env - c1 env + c2 env
Sub e1 e2 - let c1 = compile2 e1 in
let c2 = compile2 e2 in
\env - c1 env - c2 env
Mul e1 e2 - let c1 = compile2 e1 in
let c2 = compile2 e2 in
\env - c1 env * c2 env
test1 :: Expr
test1 = Add (Mul (Add (Var 0) (Var 1)) (Add (Var 0) (Var 1))) (Mul (Sub (Var 0)
(Var 1)) (Sub (Var 0) (Var 1)))
test :: Expr
test = Add (Mul test1 test1) (Add test1 test1)
do_test :: (Env - Value) - Value
do_test e =
foldl' (+) 0 (map (\n - e (array (0, 1) [(0, n), (1, n)])) [0..100])
main = do
putStrLn testing empty expr
let res0 = do_test (\env - 0)
putStrLn $ result is ++ show res0
putStrLn testing compile 1
let res1 = do_test (compile1 test)
putStrLn $ result is ++ show res1
putStrLn testing compile 2
let res2 = do_test (compile2 test)
putStrLn $ result is ++ show res2
putStrLn testing eval 1
let res3 = do_test (runReader (eval1 test))
putStrLn $ result is ++ show res3
putStrLn testing eval 2
let res4 = do_test (eval2 test)
putStrLn $ result is ++ show res4
return ()
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: different performance of equivalent expression
I've run into strange effect that I can not explain. I have simple expression that can be written by two equivalent ways. However one way give much performance gain over another. Here is an example: -- apply function many times (tail-recursive) many n f x = if n == 0 then x else many (n-1) f $! (f x) -- first adder function adder1 = let r = many 500 sin 1.0 in \x - x + r -- second adder function adder2 = \x - x + many 500 sin 1.0 If you run program it think some seconds performing math, and them prints 4 results immediately. But with adder2 function, it perform calculation in every call, which can be seen visually. It seems that compiler is able to cache in some way long computation in first case, but not in second. This is indeed the case and entirely reasonable. The effect is called memoization, a key ingredient to lazy evaluation. To simplify the explanation, let's take the examples adder1 = let r = many 5000 (1+) 0 in \x - x + r adder2 = \x - let s = many 5000 (1+) 0 in x + s The evaluation of (adder1 3) proceeds as follows: adder1 3 = (let r = many 5000 (1+) 0 in \x - x + r) 3 = let r = many 5000 (1+) 0 in 3 + r = let r = 5000 in 3 + r = 5003 Now, (r) will be updated with the result (5000) after it has been calculated and subsequent access to (r) will retrieve the updated value as in adder1 4 = (let r = 5000 in \x - x + r) 4 = let r = 5000 in 4 + r = 5004 Every incarnation of (adder1) shares the same r. For (adder2), things are different. Here, (s) will be updated as well, but different incarnations of (adder2) do not share the same (s) because (s) is only in scope after supplying some argument (x). Hence, every (adder2 3) and (adder3 4) (re)calculates its own (s). I always thought that let a = b in x + a is just a syntactic sugar for x + b. Is it wrong? This is correct but doesn't apply to the case above. The question here is whether let a = b in \x - x + a and \x - let a = b in x + a are equivalent. Considering the result, they are. But considering running time and memory footprint, they are not. The first trades memory for speed, the second trades speed for memory. In general, the compiler is reluctant to switch between those two versions, i.e. it does not perform much common subexpression elimination or let floating (see GHC manual). The choice must be up to the programmer. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: strange performance of expression evaluators
I've done some more experiments. The following program defines simple
arithmetic expression with indexed variables. I've written four
different ways to evaluate them:
- eval1 is simple monadic evaluator
- eval2 is the obvious straight-forward implentation
- compile1 is attempt to perform compilation
- compile2 is refined compile1 with sub-expressions explicitely
separated via let binding.
Test evaluates the same expression in 100 different environments.
The results are:
- eval1 - 17.47 sec
- eval2 - 3.71 sec
- compile1 - 3.79 sec
- compile2 - 3.74 sec
This figures are completely mysterious for me.
1) I expected eval1 and eval2 to perform equally. In fact, eval1 is
4.7 times slower for eval2.
2) I expected compile{1,2} to perform much faster then eval{1,2}.
However, the compilation attempt does not give any speed up at
all.
Your intention is that (compile2 test) should analyze the expression
tree of (test) only once when evaluating it for different environments.
I'm not sure whether the constructors (Add), (Mul) etc. get replaced
once and for all by (+) and (*) or whether this really matters, because
(eval2), (compile1) and (compile2) have the same running time. I think
that memoization (as explained in my previous post) only takes place for
values not of function type, i.e. partially evaluated functions aren't
memoized. It may also be that the compiler optimizes things for the
concrete expression (test) you gave in your code. So supplying the
expression interactively could show a difference between (eval2),
(compile1) and (compile2).
Ironically, (eval1) does compile as much as you intend (compile2) to
do. But it looks like the overhead imposed by appealing to
Control.Monad.Reader doesn't get inlined away completely.
Currently, you don't do much work per expression, it just gets
evaluated. To take advantage of memoization, you need to do more
expensive analysis on a per expression basis. For example, you might
want to precalculate stuff that doesn't depend on the environment:
data ConstVar a = Const a | Var (Env - a)
eval :: ConstVar a - Env - a
eval (Const x) = const x
eval (Var f) = f
-- addition, multiplication etc. do precalculation
-- when the constituents are known beforehand
instance Num a = ConstVar a where
(Const x) + (Const y) = Const (x + y)
x + y = Var (\e - eval x e + eval y e)
...
data Expr a = Value a | Variable Name
| Add (Expr a) (Expr a) | Mul (Expr a) (Expr a)
compile :: Num a = Expr a - ConstVar a
compile (Value c)= Const c
compile (Variable v) = Var (\e - e ! v)
compile (Add x y)= (compile x) + (compile y)
compile (Mul x y)= (compile x) * (compile y)
testexpr = (Mul (Value 1) (Value 2)) `Add` (Variable 1)
test = eval . compile $ testexpr
Of course, this can be improved. For instance, it currently does not
know about the associative law like in
(Add (Value 1) (Add (Value 2) (Variable 1)))
Now, it is clear that analyzing the expression again and again every
time it needs to be evaluated (interpretation) is wasted work.
Regards,
apfelmus
PS:
data Expr = Const !Value | Var !Int
| Add !Expr !Expr | Sub !Expr !Expr | Mul !Expr !Expr
You'd better leave out the strictness annotations (!).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Are GADTs expressive? Simple proof-carrying code inHaskell98
Hi, Oleg.
It is nice to see how the eval function is encoded with type classes. I
always wonder whether the HOAS example from Xi's POPL 03 paper can be
programmed this way. In particular, it appears to me that the Fix clause
requires non-inductive derivation of the form
instance Eval (f e) a = Eval e a where
eval e@(Fix f) = eval (f e)
Any trick on getting this work?
Meng
-Original Message-
From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of [EMAIL PROTECTED]
Sent: 13 January 2007 09:20
To: haskell-cafe@haskell.org
Subject: [Haskell-cafe] Are GADTs expressive? Simple proof-carrying code
inHaskell98
Inspired by the recent post by Jim Apple, we demonstrate a datatype
`Terminates' that can hold only an assuredly terminating (strongly
normalizable) term in untyped lambda-calculus. Furthermore, the values
of the datatype `Terminates' contain all and only those untyped
lambda-calculus terms with that property. As in Jim Apple's solution,
to create the value `Terminates', the user submits the term in
question and the proof of its termination. The proof will be verified
-- and if it holds, the Terminates certificate will be created. As in
Jim Apple's solution, verification of the submitted proof has to be
done at run-time, to make sure the proof is not fake, that is, has no
undefined values. Our solution uses neither GADTs nor typeclasses; in
fact, it is in Haskell98. Also, the required proof from the user
couldn't be simpler.
Jim Apple wrote:
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
The shown GADT encoding seems to be of the kind that is convertible to
typeclasses in the straightforward way, see for example,
http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs
Inn this particular example, GADT do not bring any
power. Incidentally, the typeclass encoding has an advantage: If the
submitted proof is invalid, the error will be reported at compile
time. There is not even a possibility of a run-time error. This is
because the typeclasses approach does only type-level computations and
does not look at values at all (which may as well be
undefined). Placing a value into a (rank-1) datatype forces the
typechecker to resolve any constraints associated with the value, or
report an error if constraints are not satisfiable.
However, it seems that the problem at hand admits a far simpler
solution -- in Haskell98. The solution is in spirit of lightweight
static capabilities. Here it is:
module PCC (Terminates, -- data constructor is not exported
make_terminates, get_term) where
import YourFavorite.Lambda_calc
data Terminates = Terminates{get_term::Term}
make_terminates :: Term - Integer - Maybe Terminates
make_terminates term limit =
case reduce_term_nsteps term limit of
Left _ - Nothing
Right normal_form - Just (Terminates term)
Because the data constructor is not exported, the only way to
construct a value `Terminates' from which a term can be extracted is
by invoking the function make_terminates. The function accepts a
lambda-term, and a proof of its termination. The proof takes the form
of the (upper bound of the) number of steps needed to normalize the
term. The function make_terminates checks the proof, by trying to
reduce the term that many steps. If the normal form is found in the
process, the term is normalizable and we create the
certificate. Otherwise, we conclude the termination proof does not
hold and we return Nothing. This proof checking is clearly decidable.
The module PCC constitutes the `trusted kernel' with respect to the
Terminates datatype. The function make_terminates must be rigorously
verified in order to deserve our trust. But the same should be said
for the GADT or any other solution: e.g., one can easily add a new
case alternative to the Normal datatype declaring Omega to be in the
normal form.
___
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] mapTuple
I knew there must be a way in GHC to do that second example!
As for the third example, it might be a slick way to do some
super-hyper-refactoring, but I admit I can't think of anything it
would be actually necessary for offhand.
--Grady
On 1/12/07, Cale Gibbard [EMAIL PROTECTED] wrote:
On 12/01/07, Grady Lemoine [EMAIL PROTECTED] wrote:
Is there anything in particular you're trying to accomplish? It seems
like this is the type of thing you'd accomplish with typeclasses if
you had a less general problem than you've presented. For example,
mapShowTuple :: (Show a, Show b) = (a, b) - (String, String)
mapShowTuple (x, y) = (show x, show y)
That said, it would be nice do be able to do something a little more
general, but still with a specific typeclass, like
mapNumOpTuple :: (Num a, Num b) = (Num c = c - c) - (a, b) - (a, b)
mapNumOpTuple f (x, y) = (f x, f y)
(This unfortunately fails to typecheck; GHC chokes with Illegal
polymorphic or qualified type. On the other hand, I'm still pretty
new to Haskell myself, so maybe someone else knows how to write this
correctly without doing complex type hackery.)
It's close:
{-# OPTIONS_GHC -fglasgow-exts #-}
mapNumOpPair :: (Num a, Num b) = (forall c. Num c = c - c) - (a, b) - (a,b)
mapNumOpPair f (x,y) = (f x, f y)
It would also be nice to be able to generalize over all typeclasses,
e.g. (pseudo-code here)
mapTypeclassOpTuple :: for all typeclasses C ((C a, C b) = (C c = c
- c) - (a, b) - (a, b))
but I don't even know how that would fit into Haskell's syntax. I
suspect it's an idea that's been discussed, and I just don't know the
term for it.
That's an interesting idea, typeclass variables. It would require a
bit of a kind system for typeclasses, but that's not so hard. I
somehow doubt it would get used all *that* much though. Can anyone
think of a clever way to apply this?
- Cale
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Are GADTs expressive? Simple proof-carrying code in Haskell98
On 1/13/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: The shown GADT encoding seems to be of the kind that is convertible to typeclasses in the straightforward way, see for example, http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs See also Conor McBride's Faking It: Simulating Dependent Types in Haskell http://citeseer.ist.psu.edu/mcbride01faking.html Also, GADTs are extensible in GHC HEAD, though type classes are still necessary to write functions on them: http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations Incidentally, the typeclass encoding has an advantage: If the submitted proof is invalid, the error will be reported at compile time. [more snipped] I don't quite understand what you're getting at here. Is it that with the GADT approach, one could write Terminating (Apply omega omega) (undefined) (undefined) and the typechecker would not complain? That certainly is an issue, but I think you're saying something deeper that I'm not getting. However, it seems that the problem at hand admits a far simpler solution -- in Haskell98. The solution is in spirit of lightweight static capabilities. Here it is: module PCC (Terminates, -- data constructor is not exported make_terminates, get_term) where [snip] The module PCC constitutes the `trusted kernel' with respect to the Terminates datatype. The function make_terminates must be rigorously verified in order to deserve our trust. But the same should be said for the GADT or any other solution: e.g., one can easily add a new case alternative to the Normal datatype declaring Omega to be in the normal form. That's true, but there is at least one disadvantage to the PCC module: some functions manipulating terminating terms must be placed inside the trusted core. This is not the case with GADTs. For instance, we could write a term that takes a non-normalized (but terminating) term and beta-reduces it once to return a new normalizing term. We can't do this as a mere client of the PCC module without calling make_terminates again. Operations on types with hidden constructors sometimes have to be put in the trusted core. This was a small cost for terminating terms in the untyped lambda calculus, but it's a bigger cost for other structures. This is sort of like writing nested types for balanced trees vs. using Data.Set. Data.Set does guarantee that the tree is balanced, but we can only believe this after looking at each function in Data/Set.hs. Yes, the definition for balanced nested trees must be written with the same care as the functions in Data.Set, but there are a lot more functions in Data.Set Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Meaning abbreviations stat file GHC
Dear, I made a profile[1] of a test program: Where can I find documentation for the meaning of everything mentioned below? Or alternatively, can anyone explain them? Where can I see the effect of using the -xt option in this profile? Ron [1] /Main +RTS -p -s -xt -hc 1,372,408,024 bytes allocated in the heap 121,255,600 bytes copied during GC (scavenged) 6,584,692 bytes copied during GC (not scavenged) 2,768,896 bytes maximum residency (68 sample(s)) 2649 collections in generation 0 ( 1.11s) 68 collections in generation 1 ( 0.49s) 6 Mb total memory in use INIT time0.00s ( 0.00s elapsed) MUT time5.97s ( 6.63s elapsed) GCtime1.60s ( 1.88s elapsed) RPtime0.00s ( 0.00s elapsed) PROF time0.19s ( 0.20s elapsed) EXIT time0.00s ( 0.00s elapsed) Total time7.76s ( 8.71s elapsed) %GC time 20.6% (21.5% elapsed) Alloc rate229,946,873 bytes per MUT second Productivity 76.9% of total user, 68.5% of total elapsed Ron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
