type-level-natural-number-induction-1.0.0.1: High-level combinators for performing inductive operations.

TypeLevel.NaturalNumber.Induction

Synopsis

class Induction n whereSource

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.

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.