type-level-natural-number-induction (empty) → 1.0

raw patch · 4 files changed

+269/−0 lines, 4 filesdep +basedep +transformersdep +type-level-natural-numbersetup-changed

Dependencies added: base, transformers, type-level-natural-number

Files

• LICENSE +22/−0
• Setup.hs +2/−0
• TypeLevel/NaturalNumber/Induction.hs +216/−0
• type-level-natural-number-induction.cabal +29/−0

@@ -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.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -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

@@ -0,0 +1,29 @@+Name:                type-level-natural-number-induction+Version:             1.0+License:             BSD3+License-file:        LICENSE+Author:              Gregory Crosswhite+Maintainer:          Gregory Crosswhite <gcross@phys.washington.edu>+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