Finite

A framework for capturing finite ranges with types, where the sizes of the ranges are not fixed statically at compile time, but instead are passed at run-time via implicit parameters. The purpose of the framework is to simplify the handling of objects of bounded size, e.g. finite-state machines, where the number of elements can be defined in the context of the object, e.g. the number of states.

The framework supports:

• Easy access to the object's elements via types.
• Efficient bidirectional mappings between indices and the elements.
• Implicit total orderings on the elements.
• Powerset Support.
• Extension of a single context to a range of contexts via collections.
• Easy passing of the context via implict parameters.
• Generics Support: Finite range types can be easily constructed out of other finite range types using Haskell's `data` constructor.
• Template Haskell: Easy creation of basic finite instances using short Haskell templates, as well as the extension of existing types to more feature rich parameter spaces (requires the explicit import of Finite.TH).

The Finite Class

class Finite b a where

The Finite class.

Minimal complete definition

Nothing

Methods

elements :: FiniteBounds b => T a -> Int

Returns the number of elements associated with the given type.

default elements :: (Generic a, GFinite b (Rep a), FiniteBounds b) => T a -> Int

index :: FiniteBounds b => a -> Int

Turns the value in the associated range into an Int uniquely identifiying the value.

default index :: (Generic a, GFinite b (Rep a), FiniteBounds b) => a -> Int

value :: FiniteBounds b => Int -> a

Turns an Int back to the value that is associated with it.

default value :: (Generic a, GFinite b (Rep a), FiniteBounds b) => Int -> a

offset :: FiniteBounds b => T a -> Int

Allows to put an offset to the integer mapping. Per default the offset is zero.

values :: FiniteBounds b => [a]

Returns a finite list of all elements of that type.

complement :: FiniteBounds b => [a] -> [a]

Complements a given list of elements of that type

(|<|) :: FiniteBounds b => a -> a -> Bool infixr 9

Less than operator according to the implicit total index order.

(|<=|) :: FiniteBounds b => a -> a -> Bool infixr 9

Less or equal than operator according to the implicit total index order.

(|>=|) :: FiniteBounds b => a -> a -> Bool infixr 9

Greater or equal than operator according to the implicit total index order.

(|>|) :: FiniteBounds b => a -> a -> Bool infixr 9

Greater than operator according to the implicit total index order.

(|==|) :: FiniteBounds b => a -> a -> Bool infixr 9

Equal operator according to the implicit total index order.

(|/=|) :: FiniteBounds b => a -> a -> Bool infixr 9

Unequal operator according to the implicit total index order.

initial :: FiniteBounds b => T a -> a

First element according to the total index order.

final :: FiniteBounds b => T a -> a

Last element according to the total index order.

next :: FiniteBounds b => a -> a

Next element according to the total index order (undefined for the last element).

previous :: FiniteBounds b => a -> a

Previous element according to the total index order (undefined for the first element).

bounds :: FiniteBounds b => T a -> (a, a)

The upper and lower bounds of the instance.

Instances

Finite b a => Finite b (PowerSet a)

If the number of elements associated with a type is finite, then it also has finite number of powersets.

Defined in Finite.PowerSet

Methods

elements :: T (PowerSet a) -> Int

index :: PowerSet a -> Int

value :: Int -> PowerSet a

offset :: T (PowerSet a) -> Int

values :: [PowerSet a]

complement :: [PowerSet a] -> [PowerSet a]

(|<|) :: PowerSet a -> PowerSet a -> Bool

(|<=|) :: PowerSet a -> PowerSet a -> Bool

(|>=|) :: PowerSet a -> PowerSet a -> Bool

(|>|) :: PowerSet a -> PowerSet a -> Bool

(|==|) :: PowerSet a -> PowerSet a -> Bool

(|/=|) :: PowerSet a -> PowerSet a -> Bool

initial :: T (PowerSet a) -> PowerSet a

final :: T (PowerSet a) -> PowerSet a

next :: PowerSet a -> PowerSet a

previous :: PowerSet a -> PowerSet a

bounds :: T (PowerSet a) -> (PowerSet a, PowerSet a)

(Ix i, Finite b a) => Finite (Array i b) (Collection i a)

Collections are used to extend Finite-Type / Context-Bounds pairs to an array of bounds. At the same time the finite type is extended to a collection of items that range over the same set of indices as the bounds. Since the FiniteBounds parameter always gives a finite sized array of bounding parameters, it is guaranteed that the connected collection has a finite bound as well.

Defined in Finite.Collection

Methods

elements :: T (Collection i a) -> Int

index :: Collection i a -> Int

value :: Int -> Collection i a

offset :: T (Collection i a) -> Int

values :: [Collection i a]

complement :: [Collection i a] -> [Collection i a]

(|<|) :: Collection i a -> Collection i a -> Bool

(|<=|) :: Collection i a -> Collection i a -> Bool

(|>=|) :: Collection i a -> Collection i a -> Bool

(|>|) :: Collection i a -> Collection i a -> Bool

(|==|) :: Collection i a -> Collection i a -> Bool

(|/=|) :: Collection i a -> Collection i a -> Bool

initial :: T (Collection i a) -> Collection i a

final :: T (Collection i a) -> Collection i a

next :: Collection i a -> Collection i a

previous :: Collection i a -> Collection i a

bounds :: T (Collection i a) -> (Collection i a, Collection i a)

class GFinite b f where

Generics implementation for the Finite class. The realization is closely related to the one presented at https://wiki.haskell.org/GHC.Generics.

Methods

gelements :: FiniteBounds b => T (f a) -> Int

gindex :: FiniteBounds b => f a -> Int

gvalue :: FiniteBounds b => Int -> f a

Instances

GFinite c (U1 :: Type -> Type)

U1 instance.

Defined in Finite.Class

Methods

gelements :: FiniteBounds c => T (U1 a) -> Int

gindex :: FiniteBounds c => U1 a -> Int

gvalue :: FiniteBounds c => Int -> U1 a

Finite b a => GFinite b (K1 i a :: Type -> Type)

K1 instance.

Defined in Finite.Class

Methods

gelements :: FiniteBounds b => T (K1 i a a0) -> Int

gindex :: FiniteBounds b => K1 i a a0 -> Int

gvalue :: FiniteBounds b => Int -> K1 i a a0

(GFinite b f, GFinite b g) => GFinite b (f :+: g)

:+: instance.

Defined in Finite.Class

Methods

gelements :: FiniteBounds b => T ((f :+: g) a) -> Int

gindex :: FiniteBounds b => (f :+: g) a -> Int

gvalue :: FiniteBounds b => Int -> (f :+: g) a

(GFinite b f, GFinite b g) => GFinite b (f :*: g)

:*: instance.

Defined in Finite.Class

Methods

gelements :: FiniteBounds b => T ((f :*: g) a) -> Int

gindex :: FiniteBounds b => (f :*: g) a -> Int

gvalue :: FiniteBounds b => Int -> (f :*: g) a

GFinite c f => GFinite c (M1 i v f)

M1 instance.

Defined in Finite.Class

Methods

gelements :: FiniteBounds c => T (M1 i v f a) -> Int

gindex :: FiniteBounds c => M1 i v f a -> Int

gvalue :: FiniteBounds c => Int -> M1 i v f a

type FiniteBounds b = ?bounds :: b

A better looking constraint specifier.

Powersets

type PowerSet a = [a]

Powersets are just lists of the correpsonding elements. The type has only been added for clearification. Consider the corresponding instance of Finite for possible applications.

Collections

data Collection i a

The Collection type provides a set of items, each assigning an index of type i to a value of type a.

Constructors

Item i a

Instances

(Eq i, Eq a) => Eq (Collection i a)

Equality can be checked for collections, if the index type and the elements can be checked for equality.

Defined in Finite.Collection

Methods

(==) :: Collection i a -> Collection i a -> Bool

(/=) :: Collection i a -> Collection i a -> Bool

(Ord i, Ord a) => Ord (Collection i a)

Order can be checked for collections, if the index type and the elements can be oredered.

Defined in Finite.Collection

Methods

compare :: Collection i a -> Collection i a -> Ordering

(<) :: Collection i a -> Collection i a -> Bool

(<=) :: Collection i a -> Collection i a -> Bool

(>) :: Collection i a -> Collection i a -> Bool

(>=) :: Collection i a -> Collection i a -> Bool

max :: Collection i a -> Collection i a -> Collection i a

min :: Collection i a -> Collection i a -> Collection i a

(Show i, Show a) => Show (Collection i a)

Show a collection through its default constructor.

Defined in Finite.Collection

Methods

showsPrec :: Int -> Collection i a -> ShowS

show :: Collection i a -> String

showList :: [Collection i a] -> ShowS

(Ix i, Finite b a) => Finite (Array i b) (Collection i a)

Collections are used to extend Finite-Type / Context-Bounds pairs to an array of bounds. At the same time the finite type is extended to a collection of items that range over the same set of indices as the bounds. Since the FiniteBounds parameter always gives a finite sized array of bounding parameters, it is guaranteed that the connected collection has a finite bound as well.

Defined in Finite.Collection

Methods

elements :: T (Collection i a) -> Int

index :: Collection i a -> Int

value :: Int -> Collection i a

offset :: T (Collection i a) -> Int

values :: [Collection i a]

complement :: [Collection i a] -> [Collection i a]

(|<|) :: Collection i a -> Collection i a -> Bool

(|<=|) :: Collection i a -> Collection i a -> Bool

(|>=|) :: Collection i a -> Collection i a -> Bool

(|>|) :: Collection i a -> Collection i a -> Bool

(|==|) :: Collection i a -> Collection i a -> Bool

(|/=|) :: Collection i a -> Collection i a -> Bool

initial :: T (Collection i a) -> Collection i a

final :: T (Collection i a) -> Collection i a

next :: Collection i a -> Collection i a

previous :: Collection i a -> Collection i a

bounds :: T (Collection i a) -> (Collection i a, Collection i a)

Polymorphic Type Access

data T a

A type dummy.

(#) :: T a

The type dummy instance.

(\#) :: b -> T a

A type dummy returning function. Intended to use the type engine for accessing the type of the argument. Note that "(\#) :: a -> T a" is just a special instance.

(<<#) :: (a -> b) -> T a -> b infixr 9

Replace a function's argument by its type dummy. Intended to be used for extracting type information of polymorph types only.

(#<<) :: (T a -> b) -> a -> b infixr 9

Replace a function's dummy type argument with its value taking equivalent.

v2t :: a -> T a

Get the type of a given value.

t2v :: T a -> a

Get some undefined value of the given type. Intended to be used for extracting type information of polymorph types only.