TypeLevel.NaturalNumber.Induction

Monadic interface

class Induction n where

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

Methods

deductionM

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

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

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

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

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

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

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

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)

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 n

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

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

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.