Re: [Haskell-cafe] Why cannot i add the `let` declaration ?
zaxis z_a...@163.com writes: find_the_day sDay 0 = sDay find_the_day sDay nDay = let nextDay = addDays 1 sDay if (is_trade_day $ nextDay) then find_the_day nextDay (nDay - 1) else find_the_day nextDay nDay The correct syntax is let ... in ...; you've forgotten the in, so something like this: , | find_the_day sDay 0 = sDay | find_the_day sDay nDay = | let nextDay = addDays 1 sDay | in if (is_trade_day $ nextDay) |then find_the_day nextDay (nDay - 1) |else find_the_day nextDay nDay ` Note that in do-blocks you don't need the `in'; in normal code you do. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the example posted earlier: it is precisely the
impredicative polymorphism that causes the paradox. As everybody
noticed, the example was an implementation of the Russell paradox
(whose elimination was the goal for the introduction of
predicativity).
Here is how the `absurd' example was derived. Our goal is to define a
recursive (rather than a mere inductive) data type, such as
data R = MkR (R - False)
If we have this data type, we can easily obtain the fixpoint
combinator, and hence logical inconsistency. But we want to avoid
overt recursive type. Therefore, we break the recursive knot, by
parameterizing R:
data R c = MkR (c - False)
The hope is that we can instantiate the type variable c with R and
recover the desired recursive type. The type variable c is thus
quantified over the set of types that include the type R being
defined. This impredicative polymorphism is essential for the trick.
However, instantiating the type variable c with R would be a kind
error: c has the kind * and R has the kind *-*. The obvious
work-around
data R c = MkR (c () - False)
fails: now c has the kind (*-*) but R has the kind
(*-*)-*. Again, R is not substitutable for c. If all we have are
ordinary data types, we are stuck -- for exactly the same reason that
self-application is not expressible in simply-typed lambda-calculus.
GADTs come to the rescue, giving us the needed `phase shift'. We can
define the datatype as (in pseudo-normal notation)
data R (c ()) = MkR (c () - False)
Now we can substitute R for c; alas, the result
data R (R ()) = MkR (R () - False)
is not the recursive type. The fix is trivial though:
data R (c ()) = MkR (c (c ()) - False)
Now that the method is clear, we derive the absurd term using type
functions (lest one thinks we are picking on GADTs). Type families too
let us introduce the `phase shift' (on the other side of the equation)
and thus bring about the destructive power of impredicativity.
Here is the complete code:
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data False-- No constructors
data I c = I (c ())
type family Interpret c :: *
type instance Interpret (I c) = c (I c)
data R c = MkR (Interpret c - False)
cond_false :: R (I R) - False
cond_false x@(MkR f) = f x
{- This diverges
absurd :: False
absurd = cond_false (MkR cond_false)
-}
-- Thanks to Martin Sulzmann
absurd2 :: False
absurd2 = let x = MkR cond_false in cond_false x
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
Dan Doel wrote:
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x - x x) (\x - x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least).
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why cannot i add the `let` declaration ?
thanks! Ivan Lazar Miljenovic wrote: zaxis z_a...@163.com writes: find_the_day sDay 0 = sDay find_the_day sDay nDay = let nextDay = addDays 1 sDay if (is_trade_day $ nextDay) then find_the_day nextDay (nDay - 1) else find_the_day nextDay nDay The correct syntax is let ... in ...; you've forgotten the in, so something like this: , | find_the_day sDay 0 = sDay | find_the_day sDay nDay = | let nextDay = addDays 1 sDay | in if (is_trade_day $ nextDay) |then find_the_day nextDay (nDay - 1) |else find_the_day nextDay nDay ` Note that in do-blocks you don't need the `in'; in normal code you do. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe - fac n = foldr (*) 1 [1..n] -- View this message in context: http://old.nabble.com/Why-cannot-i-add-the-%60let%60-declaration---tp27381811p27382334.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] Re: where is the eros distribution
Odd. Looks like most of the packages on d.h.o evaporated. I'll push the repo to a new location. In the move between servers, we took the opportunity to clean up some historical accidents. Many of the repositories formerly on d.h.o could equally live on community.h.o, which offers more precisely tailored access rights to contributors. In the meantime, those repositories which were not moved to the new d.h.o have temporary copies at http://old-darcs.well-typed.com/ Regards, Malcolm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
Thanks for the clear explanation, oleg.
-- ryan
On Sat, Jan 30, 2010 at 12:44 AM, o...@okmij.org wrote:
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the example posted earlier: it is precisely the
impredicative polymorphism that causes the paradox. As everybody
noticed, the example was an implementation of the Russell paradox
(whose elimination was the goal for the introduction of
predicativity).
Here is how the `absurd' example was derived. Our goal is to define a
recursive (rather than a mere inductive) data type, such as
data R = MkR (R - False)
If we have this data type, we can easily obtain the fixpoint
combinator, and hence logical inconsistency. But we want to avoid
overt recursive type. Therefore, we break the recursive knot, by
parameterizing R:
data R c = MkR (c - False)
The hope is that we can instantiate the type variable c with R and
recover the desired recursive type. The type variable c is thus
quantified over the set of types that include the type R being
defined. This impredicative polymorphism is essential for the trick.
However, instantiating the type variable c with R would be a kind
error: c has the kind * and R has the kind *-*. The obvious
work-around
data R c = MkR (c () - False)
fails: now c has the kind (*-*) but R has the kind
(*-*)-*. Again, R is not substitutable for c. If all we have are
ordinary data types, we are stuck -- for exactly the same reason that
self-application is not expressible in simply-typed lambda-calculus.
GADTs come to the rescue, giving us the needed `phase shift'. We can
define the datatype as (in pseudo-normal notation)
data R (c ()) = MkR (c () - False)
Now we can substitute R for c; alas, the result
data R (R ()) = MkR (R () - False)
is not the recursive type. The fix is trivial though:
data R (c ()) = MkR (c (c ()) - False)
Now that the method is clear, we derive the absurd term using type
functions (lest one thinks we are picking on GADTs). Type families too
let us introduce the `phase shift' (on the other side of the equation)
and thus bring about the destructive power of impredicativity.
Here is the complete code:
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data False -- No constructors
data I c = I (c ())
type family Interpret c :: *
type instance Interpret (I c) = c (I c)
data R c = MkR (Interpret c - False)
cond_false :: R (I R) - False
cond_false x@(MkR f) = f x
{- This diverges
absurd :: False
absurd = cond_false (MkR cond_false)
-}
-- Thanks to Martin Sulzmann
absurd2 :: False
absurd2 = let x = MkR cond_false in cond_false x
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
Dan Doel wrote:
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x - x x) (\x - x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least).
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] C functional programming techniques?
2010/1/29 Maurício CA: Sorry if this looks weird, but do you know of experiences with functional programming, or type programming, with C? Using macro tricks or just good specifications? This is probably not what you're looking for, but it's related: Single-Assignment C (Functional Array Programming for High-Performance Computing) http://www.sac-home.org/ From the website: SaC is an array programming language predominantly suited for application areas such as numerically intensive applications and signal processing. Its distinctive feature is that it combines high-level program specifications with runtime efficiency similar to that of hand-optimized low-level specifications. Key to the optimization process that facilitates these runtimes is the underlying functional model which also constitutes the basis for implicit parallelization. This makes SaC ideally suited for utilizing the full potential of modern CMP architectures such as multi-cores or the Cell processor. Regards, Sean ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why cannot i add the `let` declaration ?
On Sat, Jan 30, 2010 at 8:39 AM, zaxis z_a...@163.com wrote: fac n = foldr (*) 1 [1..n] fac n = product [1..n] ;) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why cannot i add the `let` declaration ?
Szekeres István wrote: On Sat, Jan 30, 2010 at 8:39 AM, zaxis z_a...@163.com mailto:z_a...@163.com wrote: fac n = foldr (*) 1 [1..n] fac n = product [1..n] ;) fac n = product [2..n] :-D ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why cannot i add the `let` declaration ?
Andrew Coppin andrewcop...@btinternet.com writes: fac n = product [2..n] Nobody likes a show-off... -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANN: hakyll-1.3
Hello, Today I'd like to announce the release of hakyll-1.3. Changes since 1.2: - Categories were added (as opposed to tags). You can find some information in this tutorial[1]. - createListing and createListingWith functions were added, as a way of having a more high-level way to create listings. All tutorials have been updated to work with listings now, a short explanation is available here[2]. In short, this basically replaces the old and verbose renderAndConcat/createCustomPage workflow. Changes since 1.1: - Rewrote caching system. - Rewrote templating system. - 4x speed improvement, mostly because of the Data.Binary library. You can get the latest version from hackage[3]. All feedback/criticism/comments are welcome. Kind regards, Jasper Van der Jeugt [1]: http://jaspervdj.be/hakyll/tutorial6.html [2]: http://jaspervdj.be/hakyll/tutorial3.html#custom-pages [3]: http://hackage.haskell.org/package/hakyll ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
On Saturday 30 January 2010 3:44:35 am o...@okmij.org wrote:
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
I've even observed your prior code hang when loading into GHCi, though. Does
inlining get done even for byte code, with no -O?
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
Coq has an impredicative universe of propositions, and Agda has a --type-in-
type option (which is definitely inconsistent), allowing both to encode your
systematically derived type. However, neither allow one to actually well type
(\x - x x) (\x - x x) by this method. In Agda:
{-# OPTIONS --type-in-type --injective-type-constructors #-}
module Stuff where
data False : Set where
data Unit : Set where
unit : Unit
data R : Set → Set where
r : (F : Set → Set) → (F (F Unit) → False) → R (F Unit)
w : R (R Unit) → False
w x with R Unit | x
... | ._ | r F f = {! !}
The with stuff can be ignored; that's required get Agda to allow matching on
x for some reason. Anyhow, we need to fill in the hole delimited by the {! !}
with something of type False, but what we have are:
x : R (R Unit)
f : F (F Unit) - False
And I'm pretty sure that there's no way to convince Agda that F = R, or
something similar, because, despite the fact that Agda has injective type
constructors like GHC (R x = R y = x = y), it doesn't let you make the
inference R Unit = F Unit = R = F. Of course, in Agda, one could arguably say
that it's true, because Agda has no type case, so there's (I'm pretty sure) no
way to write an F such that R T = F T, but R U /= F U, for some U /= T.
But, in GHC, where you *do* have type case, and *can* write functions like the
above, GHC lets you infer that R = F anyway, and throws type errors when
trying to build elements of R (T ()) for T () = R () but T /= R.
I'm relatively sure Coq is in the same boat as Agda. I've successfully defined
R above as a Prop, using impredicativity, but I'm pretty sure you'll run into
the same difficulty trying to write w there (but I don't know Coq well enough
to give a demonstration).
Coq doesn't give injectivity of type constructors by fiat, which is good,
because it can be used with impredicativity to write other paradoxes (just not
the one above). Agda has the injectivity,* but not the impredicativity. Also,
this all originally came (I believe) from the Agda mailing list, where someone
demonstrated that injectivity of type constructors is inconsistent with a
certain version of the law of the excluded middle.** However, the paradox
above seems to be unique to GHC (among the three), which is rather odd.
-- Dan
* Injectivity of type constructors is now optional in Agda, turned on by the
flag you can see above.
** Injectivity of type constructors allows you to write a proof of:
¬ (∀ (P : Set1) → P ∨ ¬ P)
there was some concern raised, because in intuitionistic logic, one can prove:
∀ (P : Set1) → ¬ ¬ (P ∨ ¬ P)
But, the above two propositions aren't contradictory, because one can't move
the quantifier past the negations as one could in classical logic. Coq in fact
allows one to prove something similar to the first proposition with --
impredicative-set, which led to that being off by default (so that one could
take excluded middle as an axiom and do classical reasoning without
(hopefully) introducing inconsistency).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Strange random choice algorithm
I'm not sure where I got this PICK function from, and don't understand why it's written as it is, so I wanted to test it for randomness. It seems random enough. But if I understand the algorithm correctly, instead of selecting one of the elements from the list, it eliminates all the elements but one and that's the value it returns. Seems like a roundabout way of doing it. Comments? Also, is there a more direct way of printing an array? Output below. Michael = import System.Random import Data.Array.IO pick :: [a] - IO a pick [] = undefined pick [x] = do return x pick (x:xs) = pick' x xs (2 :: Int) pick' :: (Num p, Random p) = t - [t] - p - IO t pick' curr [] _ = do return curr pick' curr (next:rest) prob = do r - getStdRandom (randomR (1,prob)) let curr' = if r == 1 then next else curr pick' curr' rest (prob+1) main = do arr - newArray (1,9) 0 :: IO (IOArray Int Int) doLoop arr [1,2,3,4,5,6,7,8,9] 0 doLoop arr z k = do p - pick z a - readArray arr p writeArray arr p (a+1) if k 1 then do v - readArray arr 1 print v v - readArray arr 2 print v v - readArray arr 3 print v v - readArray arr 4 print v v - readArray arr 5 print v v - readArray arr 6 print v v - readArray arr 7 print v v - readArray arr 8 print v v - readArray arr 9 print v else do doLoop arr z (k+1) === [mich...@localhost ~]$ runhaskell array1.hs 1110 1117 1080 1169 1112 1119 1137 1084 1074 [mich...@localhost ~]$ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange random choice algorithm
Am Samstag 30 Januar 2010 20:59:08 schrieb michael rice: I'm not sure where I got this PICK function from, and don't understand why it's written as it is, so I wanted to test it for randomness. It seems random enough. But if I understand the algorithm correctly, instead of selecting one of the elements from the list, it eliminates all the elements but one and that's the value it returns. Yep. Seems like a roundabout way of doing it. Comments? Indeed. Also, is there a more direct way of printing an array? Sure, printing immutable arrays: print arr ~ array (lo,hi) [(lo,arr!lo), ... , (hi,arr!hi)] print (assocs arr) ~ [(lo,arr!lo), ... , (hi,arr!hi)] print (elems arr) ~ [(arr!lo), ... , (arr!hi)] printing IO[U]Arrays: do immArr - freeze arr print (immArr :: [U]Array ix el) do ass - getAssocs arr print ass (getAssocs arr = print) do els - getElems arr print els (getElems arr = print) or, to get output like below: getElems arr = mapM_ print Printing ST[U]Arrays would need an unsafeIOToST, but reasonably, you wouldn't want to print them before you've left ST. Output below. Michael = import System.Random import Data.Array.IO pick :: [a] - IO a pick [] = undefined pick [x] = do return x pick (x:xs) = pick' x xs (2 :: Int) pick' :: (Num p, Random p) = t - [t] - p - IO t pick' curr [] _ = do return curr pick' curr (next:rest) prob = do r - getStdRandom (randomR (1,prob)) let curr' = if r == 1 then next else curr pick' curr' rest (prob+1) main = do arr - newArray (1,9) 0 :: IO (IOArray Int Int) doLoop arr [1,2,3,4,5,6,7,8,9] 0 doLoop arr z k = do p - pick z a - readArray arr p writeArray arr p (a+1) if k 1 then do v - readArray arr 1 print v v - readArray arr 2 print v v - readArray arr 3 print v v - readArray arr 4 print v v - readArray arr 5 print v v - readArray arr 6 print v v - readArray arr 7 print v v - readArray arr 8 print v v - readArray arr 9 print v else do doLoop arr z (k+1) === [mich...@localhost ~]$ runhaskell array1.hs 1110 1117 1080 1169 1112 1119 1137 1084 1074 [mich...@localhost ~]$ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange random choice algorithm
On 30 Jan 2010, at 20:59, michael rice wrote: I'm not sure where I got this PICK function from, and don't understand why it's written as it is, so I wanted to test it for randomness. It seems random enough. But if I understand the algorithm correctly, instead of selecting one of the elements from the list, it eliminates all the elements but one and that's the value it returns. Seems like a roundabout way of doing it. Comments? Below is a function draw() that shuffles an interval, and prints it out. Hans import Random getRandomIndex :: [a] - IO(Int) getRandomIndex ls = getStdRandom(randomR(0, (length ls) - 1)) remove:: Int - [a] - [a] remove 0 (x:xs) = xs remove n (x:xs) | n0 = x: remove (n-1) xs remove _ (_:_)= error remove: negative argument remove _ [] = error remove: too large argument shuffle :: [a] - IO [a] shuffle [] = return [] shuffle ls = do i - getRandomIndex ls do l - shuffle (remove i ls) return ((ls !! i) : l) draw ls = do k - shuffle ls putStr (show k) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange random choice algorithm
On Jan 30, 2010, at 8:59 PM, michael rice wrote: I'm not sure where I got this PICK function from, and don't understand why it's written as it is, so I wanted to test it for randomness. It seems random enough. We can convince ourselves using reason instead of tests. An element is selected by the algorithm if it is picked and no later element is picked afterwards. It doesn't matter which elements are picked before. The n-th element of the given list replaces the current selection with probability (1/n). Hence, the probability that the n-th element is selected in the end is (1/n)*(1-1/(n+1))*...*(1-1/m) if there are m elements. For example, if there are 9 elements, the probability of selecting the 7th is 1/7 * 7/8 * 8/9 which is 1/9 because the 7 and 8 are canceled out. This happens for all elements and, thus, every element is selected with probability 1/9. Anyway, pick xs = do n - randomRIO (1,length xs) return (xs!!(n-1)) would have been clearer.. It queries the random number generator only once but walks through the list twice. Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] C functional programming techniques?
On Jan 29, 2010, at 9:11 AM, Maurí cio CA wrote: Sorry if this looks weird, but do you know of experiences with functional programming, or type programming, with C? Using macro tricks or just good specifications? I know this is not absurd to a small extent. I've heard of proof tool certificated C code on the net (although I don't understand that theory), and I was also able to use what I learned from Haskell in a few C-like tasks. [*] I would use a higher level language to emit valid C. Basically, use a strongly typed macro language. All you will have to prove is that your emitter produces type safe code, which you can do by induction and is straight forward. You can build up a small library of combinators for type safe units of C code. Haskell might be a good choice for writing your C pre-processor, but there are plenty of choices. Using something like ehaskell (or eruby) might be a good approach. http://hackage.haskell.org/package/ehaskell ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange random choice algorithm
Hi all, Very nice analysis, Sebastian. Thanks, Michael --- On Sat, 1/30/10, Sebastian Fischer s...@informatik.uni-kiel.de wrote: From: Sebastian Fischer s...@informatik.uni-kiel.de Subject: Re: [Haskell-cafe] Strange random choice algorithm To: haskell-cafe Cafe haskell-cafe@haskell.org Date: Saturday, January 30, 2010, 6:06 PM On Jan 30, 2010, at 8:59 PM, michael rice wrote: I'm not sure where I got this PICK function from, and don't understand why it's written as it is, so I wanted to test it for randomness. It seems random enough. We can convince ourselves using reason instead of tests. An element is selected by the algorithm if it is picked and no later element is picked afterwards. It doesn't matter which elements are picked before. The n-th element of the given list replaces the current selection with probability (1/n). Hence, the probability that the n-th element is selected in the end is (1/n)*(1-1/(n+1))*...*(1-1/m) if there are m elements. For example, if there are 9 elements, the probability of selecting the 7th is 1/7 * 7/8 * 8/9 which is 1/9 because the 7 and 8 are canceled out. This happens for all elements and, thus, every element is selected with probability 1/9. Anyway, pick xs = do n - randomRIO (1,length xs) return (xs!!(n-1)) would have been clearer.. It queries the random number generator only once but walks through the list twice. Sebastian --Underestimating the novelty of the future is a time-honored tradition. (D.G.) ___ 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: C functional programming techniques?
Sorry if this looks weird, but do you know of experiences with functional programming, or type programming, with C? I would use a higher level language to emit valid C. Basically, use a strongly typed macro language. All you will have to prove is that your emitter produces type safe code, which you can do by induction and is straight forward. This is interesting. I wasn't thinking at first about actual formal proofs, just some way to make small C posix-only programs easier to read an maintain by using a big picture functional look. But I would like to try that. Do you have some link to an example of such proof by induction of type safety? Thanks, Maurício ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: could we get a Data instance for Data.Text.Text?
On Tue, Jan 26, 2010 at 10:08 AM, Jeremy Shaw jer...@n-heptane.com wrote: I think so... none of the other instances do.. but I guess that is not a very good excuse :) Send me a final darcs patch, and I'll apply it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
