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