diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,22 @@ +Copyright (c) 2010, Gregory M. Crosswhite +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, +are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + * 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. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 COPYRIGHT OWNER 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.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/TypeLevel/NaturalNumber/Induction.hs b/TypeLevel/NaturalNumber/Induction.hs new file mode 100644 --- /dev/null +++ b/TypeLevel/NaturalNumber/Induction.hs @@ -0,0 +1,216 @@ +{- Copyright (c) 2010, Gregory M. Crosswhite. All rights reserved. -} + +{-# LANGUAGE Rank2Types #-} + +module TypeLevel.NaturalNumber.Induction ( + -- * Monadic interface + Induction(..), + inductionMOnLeftFold, + inductionMOnRightFold, + -- * Pure (non-monadic) interface + deduction, + deduction2, + induction, + transform, + inductionOnLeftFold, + inductionOnRightFold, +) where + +import Control.Applicative +import Data.Functor.Identity +import TypeLevel.NaturalNumber + +-- | The Induction class contains high-level combinators for +-- performing monadic operations on inductive structures --- that is, +-- datatypes tagged with a natural number. +class Induction n where + -- | The 'deductionM' method provides a high-level combinator for + -- folding monadically over an inductive structure; essentially + -- this method is the opposite of the 'inductionM' method which + -- builds up an inductive structure rather than tearing one down. + -- See 'deduction' for a non-monadic version of this function, and + -- 'deduction2M' for a version of this function acting on two + -- structures simultaneously rather than one. + deductionM :: + Monad m + => α -- ^ the seed data + -> (f Zero -> α -> m β) -- ^ the action to perform for the base case + -> (forall n. f (SuccessorTo n) -> α -> m (f n,α)) -- ^ the action to perform for the inductive case + -> f n -- ^ the structure to fold over + -> m β -- ^ the (monadic) result + + -- | The 'deduction2M' method is the same idea as the 'deductionM' + -- method, but it simultaneously folds over two inductive structures + -- rather than one. + deduction2M :: + Monad m + => α -- ^ the seed data + -> (f Zero -> g Zero -> α -> m β) -- ^ the action to perform for the base case + -> (forall n. f (SuccessorTo n) -> g (SuccessorTo n) -> α -> m (f n,g n,α)) -- ^ the action to perform for the inductive case + -> f n -- ^ the first of the two structures to fold over + -> g n -- ^ the second of the two structures to fold over + -> m β -- ^ the (monadic) result + + -- | The 'inductionM' method provides a high-level combinator for + -- building up an inductive structure monadically starting from + -- given seed data; essentially this method is the opposite of + -- `deductionM' method which tears down an inductive structure + -- rather than building one up. See 'induction' for a non-monadic + -- version of this function. + inductionM :: + Monad m + => (α -> m (α,f Zero)) -- ^ the action to perform for the base case + -> (forall n. α -> f n -> m (α,f (SuccessorTo n))) -- ^ the action to perform for the inductive case + -> α -- ^ the seed data for the operation + -> m (α,f n) -- ^ the (monadic) result + + -- | The 'transformM' method provides a high-level combinator for + -- monadically transforming one inductive structure into another. + -- See 'transform' for a non-monadic version of this function. + transformM :: + Monad m + => (f Zero -> m (g Zero)) -- ^ the action to perform for the base case + -> (forall n. (f n -> m (g n)) -> f (SuccessorTo n) -> m (g (SuccessorTo n))) -- ^ the action to perform for the inductive case + -> f n -- ^ the structure to be transformed + -> m (g n) -- ^ the (monadic) resulting transformed structure + +instance Induction Zero where + -- | Implementation of the Induction class for the base case. + deductionM a z _ b = z b a + deduction2M a z _ b1 b2 = z b1 b2 a + inductionM z _ a = z a + transformM z _ = z + +instance Induction n => Induction (SuccessorTo n) where + -- | Implementation of the Induction class for the inductive case. + deductionM a z d b = d b a >>= \(b',a') -> deductionM a' z d b' + deduction2M a z d b1 b2 = d b1 b2 a >>= \(b'1,b'2,a') -> deduction2M a' z d b'1 b'2 + inductionM z i a = inductionM z i a >>= \(a',b') -> i a' b' + transformM z i = i (transformM z i) + +-- | The 'deduction' function provides a high-level combinator for +-- folding over an inductive structure; essentially this method is the +-- opposite of the 'induction' method which builds up an inductive +-- structure rather than tearing one down. See 'deductionM' for a +-- monadic version of this function, and 'deduction' for a version of +-- this function acting on two structures simultaneously rather than +-- one. +deduction :: + Induction n + => α -- ^ the seed data + -> (f Zero -> α -> β) -- ^ the base case + -> (forall n. f (SuccessorTo n) -> α -> (f n,α)) -- ^ the inductive case + -> f n -- ^ the structure to fold over + -> β -- ^ the result +deduction a z d b = runIdentity (deductionM a (\b a -> Identity (z b a)) (\b a -> Identity (d b a)) b) + +-- | The 'deduction2' function is the same idea as the 'deductionM' +-- function, but it simultaneously folds over two inductive structures +-- rather than one. +deduction2 :: + Induction n + => α -- ^ the seed data + -> (f Zero -> g Zero -> α -> β) -- ^ the base case + -> (forall n. f (SuccessorTo n) -> g (SuccessorTo n) -> α -> (f n,g n,α)) -- ^ the inductive case + -> f n -- ^ the first of the two structures to fold over + -> g n -- ^ the second of the two structures to fold over + -> β -- ^ the result +deduction2 a z d b1 b2 = runIdentity (deduction2M a (\b1 b2 a -> Identity (z b1 b2 a)) (\b1 b2 a -> Identity (d b1 b2 a)) b1 b2) + +-- | The 'induction' function provides a high-level combinator for +-- building up an inductive structure starting from given seed data; +-- essentially this method is the opposite of `deduction' method which +-- tears down an inductive structure rather than building one up. See +-- 'inductionM' for a monadic version of this function. +induction :: Induction n => (a -> (a,f Zero)) -> (forall n. a -> f n -> (a,f (SuccessorTo n))) -> a -> (a,f n) +induction z i a = runIdentity (inductionM (Identity . z) (\a b -> Identity (i a b)) a) + +-- | The 'transform' function provides a high-level combinator for +-- transforming one inductive structure into another. See +-- 'transformM' for a monadic version of this function. +transform :: Induction n => (f Zero -> g Zero) -> (forall n. (f n -> g n) -> f (SuccessorTo n) -> g (SuccessorTo n)) -> f n -> g n +transform z i x = runIdentity (transformM (Identity . z) (\f -> Identity . i (runIdentity . f)) x) + +-- | The 'inductionOnLeftFold' function is provided for the common +-- case where one is building up an inductive structure by performing +-- a left fold over a list. A pre-condition of calling this function +-- is that the list be the same size as the data structure, i.e. that +-- the length of the list be equal to the natural number tagging the +-- structure. When this pre-condition is violated, it returns _|_ by +-- calling 'error' with a message that the list is either too long or +-- too short. See 'inductionMOnLeftFold' for a monadic version of +-- this function, and 'inductionOnRightFold' for a version of this +-- function that performs a right fold over the list. +inductionOnLeftFold :: + Induction n + => f Zero -- ^ the base case + -> (forall n. α -> f n -> f (SuccessorTo n)) -- ^ the inductive case + -> [α] -- ^ the list to fold over + -> f n -- ^ the result +inductionOnLeftFold z i list = + case leftovers of + [] -> final + _ -> error "List is too long." + where + (leftovers,final) = + induction + (\l -> (l,z)) + (\l a -> + case l of + (x:xs) -> (xs,i x a) + _ -> error "List is too short." + ) + list + +-- | This function is the same idea as 'inductionOnLeftFold' function, +-- but it performs a right-fold rather than a left-fold over the list. +-- See 'inductionMOnRightFold' for a monadic version of this function. +inductionOnRightFold :: + Induction n + => f Zero -- ^ the base case + -> (forall n. α -> f n -> f (SuccessorTo n)) -- ^ the inductive case + -> [α] -- ^ the list to fold over + -> f n -- ^ the result +inductionOnRightFold z i = inductionOnLeftFold z i . reverse + +-- | The 'inductionMOnLeftFold' function is provided for the common +-- case where one is building up an inductive structure by performing +-- a monadic left fold over a list. A pre-condition of calling this +-- function is that the list be the same size as the data structure, +-- i.e. that the length of the list be equal to the natural number +-- tagging the structure. When this pre-condition is violated, it +-- returns _|_ by calling 'error' with a message that the list is +-- either too long or too short. See 'inductionOnLeftFold' for a +-- non-monadic version of this function, and 'inductionMOnRightFold' +-- for a version of this function that performs a right fold over the +-- list. +inductionMOnLeftFold :: + (Induction n, Monad m) + => m (f Zero) -- ^ the action to perform for the base case + -> (forall n. α -> f n -> m (f (SuccessorTo n))) -- ^ the action to perform for the inductive case + -> [α] -- ^ the list to fold over + -> m (f n) -- ^ the (monadic) result +inductionMOnLeftFold z i list = do + (leftovers,final) <- + inductionM + (\l -> z >>= \a' -> return (l,a')) + (\l a -> + case l of + (x:xs) -> i x a >>= \a' -> return (xs,a') + _ -> error "List is too short." + ) + list + case leftovers of + [] -> return final + _ -> error "List is too long." + +-- | This function is the same idea as 'inductionMOnLeftFold' function, +-- but it performs a right-fold rather than a left-fold over the list. +-- See 'inductionOnRightFold' for a non-monadic version of this function. +inductionMOnRightFold :: + (Induction n, Monad m) + => m (f Zero) -- ^ the action to perform for the base case + -> (forall n. α -> f n -> m (f (SuccessorTo n))) -- ^ the action to perform for the inductive case + -> [α] -- ^ the list to fold over + -> m (f n) -- ^ the (monadic) result +inductionMOnRightFold z i = inductionMOnLeftFold z i . reverse diff --git a/type-level-natural-number-induction.cabal b/type-level-natural-number-induction.cabal new file mode 100644 --- /dev/null +++ b/type-level-natural-number-induction.cabal @@ -0,0 +1,29 @@ +Name: type-level-natural-number-induction +Version: 1.0 +License: BSD3 +License-file: LICENSE +Author: Gregory Crosswhite +Maintainer: Gregory Crosswhite +Stability: Provisional +Synopsis: High-level combinators for performing inductive operations. +Description: This package provides high-level combinators for working + with inductive structures --- that is, structures tagged + with a phantom type-level natural number. Combinators + are provided for building up a structure from seed data + using induction, tearing down a structure to obtain a + result, and inductively transforming one structure into + another with the same size. + . + This package uses the type-level-natural-number package for + its type-level representations of the natural numbers. The + only non-Haskell 2010 extension it needs is Rank2Types. +Cabal-version: >=1.2.3 +Build-type: Simple +Category: Type System,Data + +Library + Build-depends: base >= 3 && < 5, + transformers >= 0.2 && < 0.3, + type-level-natural-number >= 1.0 && < 1.2 + Exposed-modules: TypeLevel.NaturalNumber.Induction + Extensions: Rank2Types