diff --git a/Data/Stream/Hinze/Idiom.hs b/Data/Stream/Hinze/Idiom.hs new file mode 100644 --- /dev/null +++ b/Data/Stream/Hinze/Idiom.hs @@ -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 diff --git a/Data/Stream/Hinze/Memo.hs b/Data/Stream/Hinze/Memo.hs new file mode 100644 --- /dev/null +++ b/Data/Stream/Hinze/Memo.hs @@ -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 diff --git a/Data/Stream/Hinze/NumExt.hs b/Data/Stream/Hinze/NumExt.hs new file mode 100644 --- /dev/null +++ b/Data/Stream/Hinze/NumExt.hs @@ -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./) diff --git a/Data/Stream/Hinze/Stream.hs b/Data/Stream/Hinze/Stream.hs new file mode 100644 --- /dev/null +++ b/Data/Stream/Hinze/Stream.hs @@ -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' +-} diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +> import Distribution.Simple +> main = defaultMain diff --git a/hinze-streams.cabal b/hinze-streams.cabal new file mode 100644 --- /dev/null +++ b/hinze-streams.cabal @@ -0,0 +1,49 @@ +name: hinze-streams +version: 1.0 +license: BSD3 +license-file: LICENSE +author: Ralf Hinze +maintainer: Don Stewart +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