- class Induction n where
- deductionM :: Monad m => α -> (f Zero -> α -> m β) -> (forall n. f (SuccessorTo n) -> α -> m (f n, α)) -> f n -> m β
- deduction2M :: Monad m => α -> (f Zero -> g Zero -> α -> m β) -> (forall n. f (SuccessorTo n) -> g (SuccessorTo n) -> α -> m (f n, g n, α)) -> f n -> g n -> m β
- inductionM :: Monad m => (α -> m (α, f Zero)) -> (forall n. α -> f n -> m (α, f (SuccessorTo n))) -> α -> m (α, f n)
- transformM :: Monad m => (f Zero -> m (g Zero)) -> (forall n. (f n -> m (g n)) -> f (SuccessorTo n) -> m (g (SuccessorTo n))) -> f n -> m (g n)

- inductionMOnLeftFold :: (Induction n, Monad m) => m (f Zero) -> (forall n. α -> f n -> m (f (SuccessorTo n))) -> [α] -> m (f n)
- inductionMOnRightFold :: (Induction n, Monad m) => m (f Zero) -> (forall n. α -> f n -> m (f (SuccessorTo n))) -> [α] -> m (f n)
- deduction :: Induction n => α -> (f Zero -> α -> β) -> (forall n. f (SuccessorTo n) -> α -> (f n, α)) -> f n -> β
- deduction2 :: Induction n => α -> (f Zero -> g Zero -> α -> β) -> (forall n. f (SuccessorTo n) -> g (SuccessorTo n) -> α -> (f n, g n, α)) -> f n -> g n -> β
- induction :: Induction n => (a -> (a, f Zero)) -> (forall n. a -> f n -> (a, f (SuccessorTo n))) -> a -> (a, f n)
- transform :: Induction n => (f Zero -> g Zero) -> (forall n. (f n -> g n) -> f (SuccessorTo n) -> g (SuccessorTo n)) -> f n -> g n
- inductionOnLeftFold :: Induction n => f Zero -> (forall n. α -> f n -> f (SuccessorTo n)) -> [α] -> f n
- inductionOnRightFold :: Induction n => f Zero -> (forall n. α -> f n -> f (SuccessorTo n)) -> [α] -> f n

# Monadic interface

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

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

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

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

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

Induction Zero | |

Induction n => Induction (SuccessorTo n) |

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

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

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

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

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

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