ANN: deepseq-bounded, seqaid, leaky
This trio of related packages explores strictness control in a variety of ways. deepseq-bounded provides classes and generic functions to artificially force evaluation, to extents controlled by static or dynamic configuration. seqaid puts that into practise, providing a GHC plugin to auto-instrument your package with a strictness harness, which is dynamically optimisable during runtime. This is supported directly in the GHC compilation pipeline, without requiring (or performing!) any edits to your sources. leaky is a minimal, prototypic executable that leaks space under current state-of-the-art compilation (GHC 7.8.3 -O2, at the present time). deepseq-bounded hackage: https://hackage.haskell.org/package/deepseq-bounded homepage: http://www.fremissant.net/deepseq-bounded seqaid hackage: https://hackage.haskell.org/package/seqaid homepage: http://www.fremissant.net/seqaid leaky hackage: https://hackage.haskell.org/package/leaky homepage: http://www.fremissant.net/leaky Reddit discussion for the three together: http://www.reddit.com/r/haskell/comments/2ps8f5/ann_deepseqbounded_seqaid_leaky/ Easiest way to try them all, is to install seqaid and run the demo: cabal install seqaid seqaid demo This tests seqaid on a local copy of the leaky source package. It turned out to be routine to extend deepseq-bounded and seqaid to dynamically configurable parallelisation (paraid?). Many other wrappers could be explored, too! Maybe seqaid should be renamed to koolaid or something... It's a pretty complicated system, and just first release, so there's bound to be lots of problems. I've not set up a bug tracker, but will maintain a casual list of bugs and feature requests at http://www.fremissant.net/seqaid/trac and will set up a proper tracker if there's interest. Any isssues (or comments), I'm here, or on the reddit discussion (or email). Andrew Seniuk rasfar on #haskell ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANN: deepseq-bounded, seqaid, leaky
Sorry, that was my first Reddit post and I messed up. Please use this link http://www.reddit.com/r/haskell/comments/2pscxh/ann_deepseqbounded_seqaid_leaky/ -Andrew On Fri, Dec 19, 2014 at 7:07 AM, Andrew Seniuk ras...@gmail.com wrote: This trio of related packages explores strictness control in a variety of ways. deepseq-bounded provides classes and generic functions to artificially force evaluation, to extents controlled by static or dynamic configuration. seqaid puts that into practise, providing a GHC plugin to auto-instrument your package with a strictness harness, which is dynamically optimisable during runtime. This is supported directly in the GHC compilation pipeline, without requiring (or performing!) any edits to your sources. leaky is a minimal, prototypic executable that leaks space under current state-of-the-art compilation (GHC 7.8.3 -O2, at the present time). deepseq-bounded hackage: https://hackage.haskell.org/package/deepseq-bounded homepage: http://www.fremissant.net/deepseq-bounded seqaid hackage: https://hackage.haskell.org/package/seqaid homepage: http://www.fremissant.net/seqaid leaky hackage: https://hackage.haskell.org/package/leaky homepage: http://www.fremissant.net/leaky Reddit discussion for the three together: http://www.reddit.com/r/haskell/comments/2ps8f5/ann_deepseqbounded_seqaid_leaky/ Easiest way to try them all, is to install seqaid and run the demo: cabal install seqaid seqaid demo This tests seqaid on a local copy of the leaky source package. It turned out to be routine to extend deepseq-bounded and seqaid to dynamically configurable parallelisation (paraid?). Many other wrappers could be explored, too! Maybe seqaid should be renamed to koolaid or something... It's a pretty complicated system, and just first release, so there's bound to be lots of problems. I've not set up a bug tracker, but will maintain a casual list of bugs and feature requests at http://www.fremissant.net/seqaid/trac and will set up a proper tracker if there's interest. Any isssues (or comments), I'm here, or on the reddit discussion (or email). Andrew Seniuk rasfar on #haskell ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Proving properties of type-level natural numbers obtained from user input
Richard, Ranjit,
Thanks for providing your solutions.
--
Alexander.
On 8 December 2014 at 21:45, Ranjit Jhala jh...@cs.ucsd.edu wrote:
Dear Alexander,
FWIW, this sort of thing is quite straightforward with LiquidHaskell:
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1418064183.hs
or, the code below:
-
{-@ LIQUID --no-termination @-}
module Nat255 where
-- | Define a predicate for valid integers
{-@ predicate IsValid X = 0 = X X 255 @-}
-- | Use the predicate to define a refinement type (subset) of valid
integers
{-@ type Valid = {v:Int | IsValid v}@-}
-- | A function that checks whether a given Int is indeed valid
{-@ isValid :: n:Int - {v:Bool | Prop v = IsValid n} @-}
isValid n = 0 = n n (255 :: Int)
-- | A function that can only be called with Valid Ints.
{-@ workWithValidNumber :: Valid - IO () @-}
workWithValidNumber n = putStrLn $ This is a valid number ++ show (n ::
Int)
-- | This is fine...
ok= workWithValidNumber 12
-- | ... But this is not.
notOk = workWithValidNumber 257
-- | Finally the top level loop that inputs a number, tests it
-- and calls `workWithValidNumber` if the number is valid.
loop = do putStrLn Enter Number between 0 and 255
n - readLn :: IO Int
if isValid n
then workWithValidNumber n
else putStrLn Humph, bad input, try again! loop
--
Alexander
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
