TypeLevel.NaturalNumber.Induction
- 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.
Methods
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.
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.
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.
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) |
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.
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
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.
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.
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.
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.