hinze-streams (empty) → 1.0
raw patch · 7 files changed
+561/−0 lines, 7 filesdep +Streamdep +basedep +haskell98setup-changed
Dependencies added: Stream, base, haskell98
Files
- Data/Stream/Hinze/Idiom.hs +21/−0
- Data/Stream/Hinze/Memo.hs +16/−0
- Data/Stream/Hinze/NumExt.hs +44/−0
- Data/Stream/Hinze/Stream.hs +398/−0
- LICENSE +30/−0
- Setup.lhs +3/−0
- hinze-streams.cabal +49/−0
+ Data/Stream/Hinze/Idiom.hs view
@@ -0,0 +1,21 @@+module Data.Stream.Hinze.Idiom where++import Prelude (($))++-- | A reimplementation of the classic 'idioms' class, which is now+-- known as Applicative.+--+class Idiom f where+ pure :: a -> f a+ (<>) :: f (a -> b) -> (f a -> f b)++ repeat :: a -> f a+ map :: (a -> b) -> (f a -> f b)+ zip :: (a -> b -> c) -> (f a -> f b -> f c)++ pure = repeat+ (<>) = zip ($)++ repeat a = pure a+ map f s = pure f <> s+ zip g s t = pure g <> s <> t
+ Data/Stream/Hinze/Memo.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE MultiParamTypeClasses #-}++module Data.Stream.Hinze.Memo where++import Prelude (id)++-- | We could add functional dependencies |k -> t| and |t -> k|, but since+-- Haskell has a nominal type system there may be several isomorphic key+-- types that relate to the same table type (or vice versa).+--+class Memo k t where+ tabulate :: (k -> a) -> t a+ lookup :: t a -> (k -> a)+ dom :: t k++ dom = tabulate id
+ Data/Stream/Hinze/NumExt.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE FlexibleInstances #-}++-- | Adds a few useful operators/functions to |Num|.++module Data.Stream.Hinze.NumExt (+ module Data.Stream.Hinze.NumExt,+ module Ratio+ ) where++import Prelude (Eq(..), Ord(..), Num(..), Integral(..), Integer, error, otherwise)+import qualified Prelude+import Ratio++infixl 7 /+infixr 8 ^++class (Num a, Ord a) => NumExt a where+ (/), (^) :: a -> a -> a -- NB. we include '/' to be able to define 'choose' uniformly+ fact :: a -> a+ fall, choose :: a -> a -> a++ -- | Factorials.+ fact 0 = 1+ fact n = n * fact (n - 1)++ -- | Falling factorial powers (see CMath, p.47).+ fall _ 0 = 1+ fall x n = x * fall (x - 1) (n - 1)++ -- | Binomial coefficients.++ choose x k+ | k < 0 = 0+ | otherwise = fall x k / fact k -- TODO: improve++instance NumExt Integer where+ (^) = (Prelude.^)+ (/) = div++instance (NumExt a, Integral a) => NumExt (Ratio a) where+ m ^ n = if denominator n == 1+ then (numerator m ^ numerator n) % (denominator m ^ numerator n)+ else error "^: Ratio"+ (/) = (Prelude./)
+ Data/Stream/Hinze/Stream.hs view
@@ -0,0 +1,398 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}++-- |+-- Functional Pearl: Streams and Unique Fixed Points+-- Ralf Hinze+-- The 13th ACM SIGPLAN International Conference on Functional Programming+-- (ICFP 2008)+-- Victoria, British Columbia, Canada, September 22-24, 2008 +--+-- Streams, infinite sequences of elements, live in a coworld: they are+-- given by a coinductive data type, operations on streams are implemented+-- by corecursive programs, and proofs are conducted using coinduction. But+-- there is more to it: suitably restricted, stream equations possess+-- unique solutions, a fact that is not very widely appreciated. We show+-- that this property gives rise to a simple and attractive proof technique+-- essentially bringing equational reasoning to the coworld. In fact, we+-- redevelop the theory of recurrences, finite calculus and generating+-- functions using streams and stream operators building on the cornerstone+-- of unique solutions. The development is constructive: streams and stream+-- operators are implemented in Haskell, usually by one-liners. The+-- resulting calculus or library, if you wish, is elegant and fun to use.+-- Finally, we rephrase the proof of uniqueness using generalised algebraic+-- data types.+--+-- Particularly elegant examples are obtained using n+k patterns!+--+-- New instances are added for:+--+-- Memo, Idiom, Num (!), Enum, Integral, Fractional, NumExt+--+-- +-- The great contribution of this pearl are coherent numeric instances+-- for infinite streams, given by:+-- +-- > (+) = zip (+)+-- > (-) = zip (-)+-- > (*) = zip (*)+-- > negate = map negate+-- > abs = map abs+-- > signum = map signum+-- > toEnum i = repeat (toEnum i)+-- > div = zip div+-- > mod = zip mod+-- > quotRem s t = unzip (zip quotRem s t)+-- > fromInteger = repeat . fromInteger+-- > s / t = zip (Prelude./) s t+-- > recip s = map recip s+-- > fromRational r = repeat (fromRational r)+-- > (^) = zip (^)+-- > (/) = zip (/)+-- > fact = map fact+-- > fall = zip fall+-- > choose = zip choose++module Data.Stream.Hinze.Stream (++ -- * The Stream data type and basic operations and classes++ module Data.Stream,++ -- * Functions on streams+ (<:),+ unzip,+ (\/),+ iterate,+ (<<),++ -- * Recurrences+ nat, nat', fac, fib, fib', fib'', fibv, bin,+ msb, ones, ones', onesv, carry, frac, god, jos,++ pot, pot',++ turn,+ tree,++ -- * Finite calculus+ diff,+ sum,+ sumv,++ -- * Generating functions+ const,+ z,+ (**),+ reciprocal,+ (//),+ power++ ) where++import Prelude hiding+ (head, tail, const, repeat, map, zip, unzip, iterate, lookup, sum, (**), (/), (^))+import qualified Prelude++import Data.Stream.Hinze.Memo+import Data.Stream.Hinze.Idiom+import Data.Stream.Hinze.NumExt++-- Use Wouter's Stream data type:+import Data.Stream (Stream(..), head, tail)++default (Integer, Rational)++-- TODO: does not work in GHC (power nat 2).++---+-- data Stream a = Cons a (Stream a) deriving (Eq, Ord)+--+-- data Stream a = Cons { head :: a, tail :: Stream a }+--++-- | Cons for streams+infixr 5 <:+(<:) :: a -> Stream a -> Stream a+a <: s = Cons a s++---+++{-+< Natural -> A ~= Stream A ++< data Natural = Zero | Succ Natural++< instance Memo Natural Stream where+< tabulate f = f Zero <: tabulate (f . Succ)+<+< lookup s Zero = head s+< lookup s (Succ n) = lookup (tail s) n+-}++-- | Streams of type 'Stream a' are memoised functions of type 'Natural -> A|'+instance (Integral a) => Memo a Stream where+ tabulate f = f 0 <: tabulate (f . (+ 1))++ lookup s 0 = head s+ lookup s (n + 1) = lookup (tail s) n+ lookup _ _ = error "lookup: negative argument"++---++-- | Stream are idioms aka applicative functors.+--+instance Idiom Stream where+ pure a = s where s = a <: s+ s <> t = (head s) (head t) <: (tail s) <> (tail t)++ repeat a = s where s = a <: s+ map f s = f (head s) <: map f (tail s)+ zip g s t = g (head s) (head t) <: zip g (tail s) (tail t)+++---++-- | Instance declarations.++-- | +first :: Int -> Stream aT -> [aT]+first 0 _s = []+first (n + 1) s = head s : first n (tail s)+first _ _ = error "first: negative argument"++-- | Showing a stream+showStream :: (Show a) => Int -> Stream a -> ShowS+showStream l s = showString "<" . showl (first l s)+ where showl [] = showString "..>"+ showl (a : as) = shows a . showString ", " . showl as++{-+-- Wouter's class derives (Eq, Ord), Ralf hacks around. We go with+-- Wouter (i.e. they diverge).++instance (Show a) => Show (Stream a) where+ showsPrec _d = showStream len -- HACK+instance (Eq a) => Eq (Stream a) where+ s == t = first len s == first len t -- HACK+instance (Ord a) => Ord (Stream a) where+ s <= t = first len s <= first len t -- HACK+-}++-- | `Generic' instances for |Functor| and numeric classes.++-- > instance Functor Stream where+-- > fmap = map++-- | Num instance for streams+instance (Num a) => Num (Stream a) where+ (+) = zip (+)+ (-) = zip (-)+ (*) = zip (*)+ negate = map negate+ abs = map abs+ signum = map signum+ fromInteger = repeat . fromInteger++-- | Enumerate streams+instance (Enum a) => Enum (Stream a) where+ toEnum i = repeat (toEnum i)+ fromEnum = error "fromEnum: not defined for streams"++-- Fake Real instance+instance (Real a) => Real (Stream a) where+ toRational = error "toRational: not defined for streams"++-- | Integral streams+instance (Integral a) => Integral (Stream a) where+ div = zip div+ mod = zip mod+ quotRem s t = unzip (zip quotRem s t)+ toInteger = error "toInteger: not defined for streams"++-- | Fractional streams+instance (Fractional a) => Fractional (Stream a) where+ s / t = zip (Prelude./) s t+ recip s = map recip s+ fromRational r = repeat (fromRational r)++-- | unzip two streams+unzip :: Stream (a, b) -> (Stream a, Stream b)+unzip s = (a <: as, b <: bs)+ where (a, b ) = head s+ (as, bs) = unzip (tail s)++-- | Extra numeric instances+instance (NumExt a) => NumExt (Stream a) where+ (^) = zip (^)+ (/) = zip (/)+ fact = map fact+ fall = zip fall+ choose = zip choose++------------------------------------------------------------------------------+-- $ Recurrences+-- NB. The streams can be given the more general type |(Num a) => Stream a|.+-- However, sometimes this triggers unresolved overloading errors.++nat, nat', fac, fib, fib', fib'', fibv,+ bin, msb, ones, ones', onesv, carry, frac, god, jos :: Stream Integer++pot, pot' :: Stream Bool++nat = 0 <: nat + 1+nat' = tail nat++fac = 1 <: (nat + 1) * fac++fib = 0 <: fib'+fib' = 1 <: fib' + fib+fib'' = tail fib'++fibv = 0 <: fibv + (1 <: fibv)++infixr 5 \/+(\/) :: Stream a -> Stream a -> Stream a+s \/ t = head s <: t \/ tail s++bin = 0 <: 2 * bin + 1 \/ 2 * bin + 2++iterate :: (a -> a) -> (a -> Stream a)+iterate f a = a <: iterate f (f a)++pot = True <: pot \/ repeat False+pot' = tail pot+msb = 1 <: 2 * msb \/ 2 * msb+ones = 0 <: ones'+ones' = 1 <: ones' \/ ones' + 1+carry = 0 \/ carry + 1++turn :: (Integral a) => a -> [a]+turn 0 = []+turn (n + 1) = turn n ++ [n] ++ turn n+turn _ = error "turn: negative argument" ++tree :: (Integral a) => a -> Stream a+tree n = n <: turn n << tree (n + 1)++infixr 5 <<+(<<) :: [a] -> Stream a -> Stream a+[] << s = s+(a : as) << s = a <: (as << s)++frac = nat \/ frac+god = 2 * frac + 1+jos = 1 <: 2 * jos - 1 \/ 2 * jos + 1++------------------------------+-- $ Finite calculus+-------------------------------++diff :: (Num a) => Stream a -> Stream a+diff s = tail s - s++sum :: (Num a) => Stream a -> Stream a+sum s = t where t = 0 <: t + s++onesv = 0 <: onesv + 1 - carry++sumv :: (Num a) => Stream a -> Stream a+sumv s = 0 <: repeat (head s) + sumv (tail s)++------------------------------------------------------------------------------+-- $ Generating functions+------------------------------------------------------------------------------++const :: (Num a) => a -> Stream a+const n = n <: repeat 0++z :: (Num a) => Stream a+z = 0 <: 1 <: repeat 0++infixl 7 **+(**) :: (Num a) => Stream a -> Stream a -> Stream a+s ** t = head s * head t <: repeat (head s) * tail t + tail s ** t++reciprocal :: (Fractional a) => Stream a -> Stream a+reciprocal s = t where a = recip (head s)+ t = a <: repeat (- a) * (tail s ** t)++infixl 7 //+(//) :: (Fractional a) => Stream a -> Stream a -> Stream a+s // t = s ** reciprocal t++power :: (Fractional a, Integral b) => Stream a -> b -> Stream a+power s n+ | n >= 0 = pow s n+ | otherwise = reciprocal (pow s (- n))+ where pow _t 0 = const 1+ pow t (k + 1) = t ** pow t k+ pow _ _ = error "power: impossible"++{-+------------------------------------------------------------------------------+-- Proof of existence and uniqueness of solutions+------------------------------------------------------------------------------++class Coalgebra s where+ head :: s a -> a+ tail :: s a -> s a++unfold :: (Coalgebra s) => s a -> Stream a+unfold s = head s <: unfold (tail s)++data Expr :: * -> * where+ Var :: Stream a -> Expr a+ Repeat :: a -> Expr a+ Plus :: (Num a) => Expr a -> Expr a -> Expr a+ Nat :: Expr Integer++instance Coalgebra Expr where+ head (Var s) = head s+ head (Repeat a) = a+ head (Plus e1 e2) = head e1 + head e2+ head Nat = 0++ tail (Var s) = Var (tail s)+ tail (Repeat a) = Repeat a+ tail (Plus e1 e2) = Plus (tail e1) (tail e2)+ tail Nat = Plus Nat (Repeat 1)++eval :: Expr a -> Stream a+eval = unfold++ repeat k = eval (Repeat k)+ s1 + s2 = eval (Plus (Var s1) (Var s2))+ nat = eval Nat+-}++------------------------------------------------------------------------------++{-+Examples.++> main :: IO ()+> main = do+> print $ fib+> print $ nat * nat+> print $ tail fib ^ 2 - fib * tail (tail fib)+> print $ tail fib ^ 2 - fib * tail (tail fib) == (-1) ^ nat+> print $ pot+> print $ msb+> print $ (nat' - msb)+> print $ ones+> print $ jos+> print $ (jos - 1) / 2+> print $ diff (nat ^ 3)+> print $ diff (2 ^ nat)+> print $ carry+> print $ jos+> print $ diff (fall nat 3)+> print $ 3 * fall nat 2+> print $ sum (0 \/ 1 :: Stream Integer) +> print $ sum (2 * nat + 1)+> print $ sum carry+> print $ nat ** 10 ^ nat+> print $ 9 * (nat ** 10 ^ nat)+> print $ 9 * (nat ** 10 ^ nat) + nat'+-}
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2008, Ralf Hinze++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ hinze-streams.cabal view
@@ -0,0 +1,49 @@+name: hinze-streams+version: 1.0+license: BSD3+license-file: LICENSE+author: Ralf Hinze+maintainer: Don Stewart <dons@galois.com>+homepage: http://code.haskell.org/~dons/code/hinze-streams+category: Data+synopsis: Streams and Unique Fixed Points+description: + Numeric instances for infinite streams. An implementation of:+ .+ /Functional Pearl: Streams and Unique Fixed Points/, Ralf Hinze, University of Oxford+ .+ Streams, infinite sequences of elements, live in a coworld: they are+ given by a coinductive data type, operations on streams are implemented+ by corecursive programs, and proofs are conducted using coinduction. But+ there is more to it: suitably restricted, stream equations possess+ unique solutions, a fact that is not very widely appreciated. We show+ that this property gives rise to a simple and attractive proof technique+ essentially bringing equational reasoning to the coworld. In fact, we+ redevelop the theory of recurrences, finite calculus and generating+ functions using streams and stream operators building on the cornerstone+ of unique solutions. The development is constructive: streams and stream+ operators are implemented in Haskell, usually by one-liners. The+ resulting calculus or library, if you wish, is elegant and fun to use.+ Finally, we rephrase the proof of uniqueness using generalised algebraic+ data types.+ .+ Along with the usual instances for infinite streams, this provides:+ Num, Enum, Real, Fractional, as well as recurrences on streams,+ finite calculus, generators+ .+build-type: Simple+stability: experimental+cabal-version: >= 1.2++library+ build-depends: base, haskell98, Stream++ exposed-modules:+ Data.Stream.Hinze.Idiom+ Data.Stream.Hinze.Memo+ Data.Stream.Hinze.NumExt+ Data.Stream.Hinze.Stream++ extensions: + MultiParamTypeClasses,+ FlexibleInstances