Safe Haskell | None |
---|---|
Language | Haskell2010 |
Definition of Encoding
, and a set of fundamental Encoding
s
and constructions.
This module contains the basic definitions for Encoding
s. It
defines the Encoding
type, the functions for creating an
Encoding
, and a set of stock constructions.
The Encoding
type is encapsulated; the functions mkEncoding
(and the variants thereof) are used to synthetically construct an
encoding from the fundamental operations.
The IllegalArgument
exception datatype, as well as the
fundamental operations are also defined here.
In addition to this, a set of basic definitions and constructions
are provided. These definitions should be suitable for defining
Encoding
s for most algebraic datatypes without having to manually
write encode/decode implementations.
Synopsis
- data Encoding ty
- mkEncoding :: (ty -> Integer) -> (Integer -> ty) -> Maybe Integer -> (ty -> Bool) -> Encoding ty
- mkInfEncoding :: (ty -> Integer) -> (Integer -> ty) -> (ty -> Bool) -> Encoding ty
- data IllegalArgument = IllegalArgument !String
- encode :: Encoding ty -> ty -> Integer
- decode :: Encoding ty -> Integer -> ty
- size :: Encoding ty -> Maybe Integer
- inDomain :: Encoding ty -> ty -> Bool
- identity :: Encoding Integer
- singleton :: Eq ty => ty -> Encoding ty
- integral :: Integral n => Encoding n
- interval :: Integral n => n -> n -> Encoding n
- fromHashableList :: forall ty. (Hashable ty, Ord ty) => [ty] -> Encoding ty
- fromOrdList :: forall ty. Ord ty => [ty] -> Encoding ty
- wrap :: (a -> Maybe b) -> (b -> Maybe a) -> Encoding b -> Encoding a
- optional :: Encoding ty -> Encoding (Maybe ty)
- mandatory :: Encoding (Maybe ty) -> Encoding ty
- nonzero :: Encoding ty -> Encoding ty
- exclude :: [ty] -> Encoding ty -> Encoding ty
- either :: Encoding ty1 -> Encoding ty2 -> Encoding (Either ty1 ty2)
- union :: forall ty. [Encoding ty] -> Encoding ty
- pair :: Encoding ty1 -> Encoding ty2 -> Encoding (ty1, ty2)
- triple :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding (ty1, ty2, ty3)
- quad :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding (ty1, ty2, ty3, ty4)
- quint :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding (ty1, ty2, ty3, ty4, ty5)
- sextet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6)
- septet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7)
- octet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8)
- nonet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding ty9 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8, ty9)
- dectet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding ty9 -> Encoding ty10 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8, ty9, ty10)
- power :: Integer -> Encoding ty -> Encoding [ty]
- set :: Ord ty => Encoding ty -> Encoding (Set ty)
- hashSet :: (Hashable ty, Ord ty) => Encoding ty -> Encoding (HashSet ty)
- seq :: Encoding ty -> Encoding [ty]
- boundedSeq :: Integer -> Encoding ty -> Encoding [ty]
- recursive :: (Encoding ty -> Encoding ty) -> Encoding ty
- recursive2 :: ((Encoding ty1, Encoding ty2) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2) -> Encoding ty2) -> (Encoding ty1, Encoding ty2)
- recursive3 :: ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty3) -> (Encoding ty1, Encoding ty2, Encoding ty3)
- recursive4 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty4) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4)
- recursive5 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty5) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5)
- recursive6 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty5) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty6) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6)
- recursive7 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty5) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty6) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty7) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7)
- recursive8 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty5) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty6) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty7) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty8) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8)
- recursive9 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty5) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty6) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty7) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty8) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty9) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9)
- recursive10 :: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty1) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty2) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty3) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty4) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty5) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty6) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty7) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty8) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty9) -> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty10) -> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10)
Basic Definitions
Constructors
Type for an encoding. The structure of this type is deliberately
hidden from users. Use the mkEncoding
functions to construct
Encoding
s, and the seven functions to use them.
:: (ty -> Integer) | The encoding function. |
-> (Integer -> ty) | The decoding function. Can assume all inputs are positive. |
-> Maybe Integer | The number of mappings, or |
-> (ty -> Bool) | A function indicating whether or not a given value is in the domain of values. |
-> Encoding ty |
Create an encoding from all the necessary components.
:: (ty -> Integer) | The encoding function. |
-> (Integer -> ty) | The decoding function. Can assume all inputs are positive. |
-> (ty -> Bool) | A function indicating whether or not a given value is in the domain of values. |
-> Encoding ty |
Create an infinite-sized encoding. This variant does not need a size.
Using Encodings
data IllegalArgument Source #
Instances
Show IllegalArgument Source # | |
Defined in Data.ArithEncode.Basic showsPrec :: Int -> IllegalArgument -> ShowS # show :: IllegalArgument -> String # showList :: [IllegalArgument] -> ShowS # | |
Exception IllegalArgument Source # | |
Defined in Data.ArithEncode.Basic |
Encode a ty
as a positive Integer
(ie. a natural number).
If the given ty
is not in the domain of the Encoding
(meaning,
inDomain
returns False
), the underlying implementation may
throw IllegalArgument
. However, this is not strictly required;
therefore, do not rely on IllegalArgument
being thrown.
Decode a ty
from a positive Integer
(ie. a natural number).
If the given Integer
is out of bounds (ie. it is bigger than
size
), the underlying implementation may throw
IllegalArgument
. However, this not strictly required;
therefore, do not rely on IllegalArgument
being thrown.
:: Encoding ty | Encoding to use. |
-> ty | Value to query. |
-> Bool | Whether or not the value is in the domain of the encoding. |
Indicate whether or not a value is in the domain of the encoding.
Building Encodings
Basic Encodings
integral :: Integral n => Encoding n Source #
An encoding of all integers.
Note: this is not an identity mapping.
:: (Hashable ty, Ord ty) | |
=> [ty] | A list of items to encode. |
-> Encoding ty | An encoding mapping the items in the list to natural numbers. |
Build an encoding from a list of items with a Hashable
instance.
:: Ord ty | |
=> [ty] | A list of items to encode. |
-> Encoding ty | An encoding mapping the items in the list to natural numbers. |
Build an encoding from a list of items with an Ord
instance.
Constructions
Wrapping
:: (a -> Maybe b) | The forward encoding function. |
-> (b -> Maybe a) | The reverse encoding function. |
-> Encoding b | The inner encoding. |
-> Encoding a |
Wrap an encoding using a pair of functions. These functions must also define an isomorphism.
Optional
optional :: Encoding ty -> Encoding (Maybe ty) Source #
Generate an encoding for Maybe ty
from an inner encoding for
ty
.
mandatory :: Encoding (Maybe ty) -> Encoding ty Source #
The dual of optional
. This construction assumes that Nothing
maps to 0
, and removes it from the input domain.
Using this construction on encodings for Maybe ty
which are not
produced by optional
may have unexpected results.
Exclusion
nonzero :: Encoding ty -> Encoding ty Source #
Removes the mapping to 0
(ie. the first mapping). This has the
same effect as exclude [x]
, where x
is the value that maps to
0
. It is also similar to mandatory
, except that it does not
change the base type.
Removes the mapping to the items in the list. The resulting
encode
, decode
, and highestIndex
are O(length excludes
), so
this should only be used with a very short excludes list.
Unions
:: Encoding ty1 | The |
-> Encoding ty2 | The |
-> Encoding (Either ty1 ty2) |
Combine two encodings into a single encoding that returns an
Either
of the two types.
Combine a set of encodings with the result type into a single encoding which represents the disjoint union of the components.
Products and Powers
pair :: Encoding ty1 -> Encoding ty2 -> Encoding (ty1, ty2) Source #
Take encodings for two datatypes A and B, and build an encoding for a pair (A, B).
triple :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding (ty1, ty2, ty3) Source #
Construct an encoding for a 3-tuple from the encodings for the
three components. This is actually just a wrapper around pair
.
quad :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding (ty1, ty2, ty3, ty4) Source #
Construct an encoding for a 4-tuple from the encodings for the
four components. This is actually just a wrapper around pair
.
quint :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding (ty1, ty2, ty3, ty4, ty5) Source #
Construct an encoding for a 5-tuple from the encodings for the
five components. This is actually just a wrapper around pair
.
sextet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6) Source #
Construct an encoding for a 6-tuple from the encodings for the
six components. This is actually just a wrapper around pair
.
septet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7) Source #
Construct an encoding for a 7-tuple from the encodings for the
seven components. This is actually just a wrapper around pair
.
octet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8) Source #
Construct an encoding for an 8-tuple from the encodings for the
eight components. This is actually just a wrapper around pair
.
nonet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding ty9 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8, ty9) Source #
Construct an encoding for a 9-tuple from the encodings for the
nine components. This is actually just a wrapper around pair
.
dectet :: Encoding ty1 -> Encoding ty2 -> Encoding ty3 -> Encoding ty4 -> Encoding ty5 -> Encoding ty6 -> Encoding ty7 -> Encoding ty8 -> Encoding ty9 -> Encoding ty10 -> Encoding (ty1, ty2, ty3, ty4, ty5, ty6, ty7, ty8, ty9, ty10) Source #
Construct an encoding for a 10-tuple from the encodings for the
ten components. This is actually just a wrapper around pair
.
:: Integer | Number of elements in the resulting lists |
-> Encoding ty |
|
-> Encoding [ty] |
Take an Encoding
for elements and a length and produce an
Encoding
for lists of exactly that length.
This differs from boundedSeq
in that the resulting list is
exactly the given length, as opposed to upper-bounded by it.
Sets
set :: Ord ty => Encoding ty -> Encoding (Set ty) Source #
Build an encoding for finite sets of values of a given datatype from an encoding for that datatype.
Note: this encoding and its variants can produce very large numbers for a very small set.
hashSet :: (Hashable ty, Ord ty) => Encoding ty -> Encoding (HashSet ty) Source #
Build an encoding for finite sets of values of a given datatype
from an encoding for that datatype. Similar to set
, but uses
HashSet
instead
Sequences
seq :: Encoding ty -> Encoding [ty] Source #
Construct an encoding for finite sequences of a type from an encoding for values of that type.
Note: This encoding can produce very large numbers for short sequences.
:: Integer | The maximum length of the sequence |
-> Encoding ty | The |
-> Encoding [ty] |
Construct an encoding for sequences whose length is bounded by a given value from an encoding for elements of the sequence.
Recursive
:: (Encoding ty -> Encoding ty) | A function that, given a self-reference, constructs an encoding. |
-> Encoding ty |
Take a function which takes a self-reference and produces a recursive encoding, and produce the fixed-point encoding.
:: ((Encoding ty1, Encoding ty2) -> Encoding ty1) | A function that, given self-references to both encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2) -> Encoding ty2) | A function that, given self-references to both encodings, constructs the second encoding. |
-> (Encoding ty1, Encoding ty2) |
A recursive construction for two mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3) |
A recursive construction for three mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4) |
A recursive construction for four mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5) |
A recursive construction for five mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) -> Encoding ty6) | A function that, given self-references to all encodings, constructs the sixth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6) |
A recursive construction for six mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty6) | A function that, given self-references to all encodings, constructs the sixth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) -> Encoding ty7) | A function that, given self-references to all encodings, constructs the seventh encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7) |
A recursive construction for seven mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty6) | A function that, given self-references to all encodings, constructs the sixth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty7) | A function that, given self-references to all encodings, constructs the seventh encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) -> Encoding ty8) | A function that, given self-references to all encodings, constructs the eighth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8) |
A recursive construction for eight mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty6) | A function that, given self-references to all encodings, constructs the sixth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty7) | A function that, given self-references to all encodings, constructs the seventh encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty8) | A function that, given self-references to all encodings, constructs the eighth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) -> Encoding ty9) | A function that, given self-references to all encodings, constructs the ninth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9) |
A recursive construction for nine mutually-recursive constructions.
:: ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty1) | A function that, given self-references to all encodings, constructs the first encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty2) | A function that, given self-references to all encodings, constructs the second encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty3) | A function that, given self-references to all encodings, constructs the third encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty4) | A function that, given self-references to all encodings, constructs the fourth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty5) | A function that, given self-references to all encodings, constructs the fifth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty6) | A function that, given self-references to all encodings, constructs the sixth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty7) | A function that, given self-references to all encodings, constructs the seventh encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty8) | A function that, given self-references to all encodings, constructs the eighth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty9) | A function that, given self-references to all encodings, constructs the ninth encoding. |
-> ((Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) -> Encoding ty10) | A function that, given self-references to all encodings, constructs the tenth encoding. |
-> (Encoding ty1, Encoding ty2, Encoding ty3, Encoding ty4, Encoding ty5, Encoding ty6, Encoding ty7, Encoding ty8, Encoding ty9, Encoding ty10) |
A recursive construction for ten mutually-recursive constructions.