arith-encode-1.0.2: A practical arithmetic encoding (aka Godel numbering) library.

Safe HaskellNone
LanguageHaskell2010

Data.ArithEncode.Basic

Contents

Description

Definition of Encoding, and a set of fundamental Encodings and constructions.

This module contains the basic definitions for Encodings. 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 Encodings for most algebraic datatypes without having to manually write encode/decode implementations.

Synopsis

Basic Definitions

Constructors

data Encoding ty Source #

Type for an encoding. The structure of this type is deliberately hidden from users. Use the mkEncoding functions to construct Encodings, and the seven functions to use them.

mkEncoding Source #

Arguments

:: (ty -> Integer)

The encoding function.

-> (Integer -> ty)

The decoding function. Can assume all inputs are positive.

-> Maybe Integer

The number of mappings, or Nothing if it is infinite.

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

mkInfEncoding Source #

Arguments

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

An exception to be thrown if an illegal argument is given to encode, decode.

Constructors

IllegalArgument !String 
Instances
Show IllegalArgument Source # 
Instance details

Defined in Data.ArithEncode.Basic

Methods

showsPrec :: Int -> IllegalArgument -> ShowS #

show :: IllegalArgument -> String #

showList :: [IllegalArgument] -> ShowS #

Exception IllegalArgument Source # 
Instance details

Defined in Data.ArithEncode.Basic

Methods

toException :: IllegalArgument -> SomeException #

fromException :: SomeException -> Maybe IllegalArgument #

displayException :: IllegalArgument -> String #

encode Source #

Arguments

:: Encoding ty

Encoding to use.

-> ty

Value to encode.

-> Integer

Encoded value.

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 Source #

Arguments

:: Encoding ty

Encoding to use.

-> Integer

Number to decode.

-> ty

Decoded value.

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.

size Source #

Arguments

:: Encoding ty

Encoding to use.

-> Maybe Integer

Number of values mapped, or Nothing for infinity.

Get the size of an Encoding, or Nothing if it is infinite.

inDomain Source #

Arguments

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

identity :: Encoding Integer Source #

The identity encoding. Maps every positive Integer to itself.

Note: only positive integers are in the domain of this encoding. For all an encoding whose domain is all integers, use integral.

singleton :: Eq ty => ty -> Encoding ty Source #

A singleton encoding. Maps a singular value to 0.

integral :: Integral n => Encoding n Source #

An encoding of all integers.

Note: this is not an identity mapping.

interval Source #

Arguments

:: Integral n 
=> n

The (inclusive) lower bound on the range.

-> n

The (inclusive) upper bound on the range.

-> Encoding n 

Build an encoding from a finite range of Integrals.

Both the upper and lower bounds are inclusive. This allows an Encoding to be created for bounded integer datatypes, such as Int8.

fromHashableList Source #

Arguments

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

fromOrdList Source #

Arguments

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

wrap Source #

Arguments

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

exclude Source #

Arguments

:: [ty]

The list of items to exclude.

-> Encoding ty

The base Encoding.

-> Encoding ty 

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

either Source #

Arguments

:: Encoding ty1

The Encoding that will be represented by Left.

-> Encoding ty2

The Encoding that will be represented by Right.

-> Encoding (Either ty1 ty2) 

Combine two encodings into a single encoding that returns an Either of the two types.

union Source #

Arguments

:: [Encoding ty]

The components of the union.

-> Encoding ty 

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.

power Source #

Arguments

:: Integer

Number of elements in the resulting lists

-> Encoding ty

Encoding for the elements

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

boundedSeq Source #

Arguments

:: Integer

The maximum length of the sequence

-> Encoding ty

The Encoding for the sequence elements

-> Encoding [ty] 

Construct an encoding for sequences whose length is bounded by a given value from an encoding for elements of the sequence.

Recursive

recursive Source #

Arguments

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

recursive2 Source #

Arguments

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

recursive3 Source #

Arguments

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

recursive4 Source #

Arguments

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

recursive5 Source #

Arguments

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

recursive6 Source #

Arguments

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

recursive7 Source #

Arguments

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

recursive8 Source #

Arguments

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

recursive9 Source #

Arguments

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

recursive10 Source #

Arguments

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