Monadic interface

The Induction class contains high-level combinators for performing monadic operations on inductive structures --- that is, datatypes tagged with a natural number.

Methods

deductionM Source

Arguments

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

deduction2M Source

Arguments

:: 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 deduction2M method is the same idea as the deductionM method, but it simultaneously folds over two inductive structures rather than one.

inductionM Source

Arguments

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

transformM Source

Arguments

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

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.

Instances

Induction Zero
Induction n => Induction (SuccessorTo n)

inductionMOnLeftFold Source

Arguments

:: (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

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.

inductionMOnRightFold Source

Arguments

:: (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

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.

Pure (non-monadic) interface

deduction Source

Arguments

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

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.

deduction2 Source

Arguments

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

The deduction2 function is the same idea as the deductionM function, but it simultaneously folds over two inductive structures rather than one.

induction :: Induction n => (a -> (a, f Zero)) -> (forall n. a -> f n -> (a, f (SuccessorTo n))) -> a -> (a, f n)Source

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.

transform :: Induction n => (f Zero -> g Zero) -> (forall n. (f n -> g n) -> f (SuccessorTo n) -> g (SuccessorTo n)) -> f n -> g nSource

The transform function provides a high-level combinator for transforming one inductive structure into another. See transformM for a monadic version of this function.

inductionOnLeftFold Source

Arguments

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

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.

inductionOnRightFold Source

Arguments

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

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.