On Thu, 27 Oct 2011, Lukas Bulwahn wrote:
On 10/27/2011 04:38 PM, Florian Haftmann wrote:
Nonetheless, we still have the real-based Library.random from "ML for
the working programmer", because without it quickcheck performs really
bad.
AFAIR this has only been the case for the ancient SML qui
On 10/27/2011 04:38 PM, Florian Haftmann wrote:
Nonetheless, we still have the real-based Library.random from "ML for
the working programmer", because without it quickcheck performs really
bad.
AFAIR this has only been the case for the ancient SML quickcheck,
whereas my quickcheck implementatio
> Nonetheless, we still have the real-based Library.random from "ML for
> the working programmer", because without it quickcheck performs really
> bad.
AFAIR this has only been the case for the ancient SML quickcheck,
whereas my quickcheck implementation comes with a random generator in
HOL based
On Thu, 27 Oct 2011, Lawrence Paulson wrote:
If my memory is correct, quicksort was the clear winner in the
performance tests that I undertook for my book.
I can confirm it for some later measurements of the refined implementation
-- data from 2005..2007, IIRC.
There are some anecdotes abo
If my memory is correct, quicksort was the clear winner in the performance
tests that I undertook for my book.
Larry
On 27 Oct 2011, at 13:50, Florian Haftmann wrote:
> interesting to read that comment. The exiting quicksort implementation
> in HOL is indeed taken from Isabelle's ML library. D
On Thu, 27 Oct 2011, Florian Haftmann wrote:
The exiting quicksort implementation in HOL is indeed taken from
Isabelle's ML library. Don't know what the ancient motivation for
quicksort has been (maybe others can comment on this).
In ancient times, the Isabelle/ML library had a really slow i
> Indeed, that would be the obvious next step. I have not tried yet but
> would not expect too hard difficulties. If this is of general interest I
> can try.
Well, if you want to superseed the existing quicksort, you have to
provide the same generality ;-)
Florian
--
Home:
http://www.i
On 10/27/2011 02:50 PM, Florian Haftmann wrote:
Hi Christian,
please find attached the formalization of the merge-sort algorithm as
used in GHC's standard library. See also:
http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
interesting to read that comm
Hi Christian,
> please find attached the formalization of the merge-sort algorithm as
> used in GHC's standard library. See also:
>
> http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
interesting to read that comment. The exiting quicksort implementation
i
Hi all,
please find attached the formalization of the merge-sort algorithm as
used in GHC's standard library. See also:
http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
Due to experiments and comments found there, I suggest that this
implementation is
10 matches
Mail list logo
