Safe Haskell | None |
---|---|

Language | Haskell2010 |

Cantor pairing gives us an isomorphism between a single natural number and pairs of natural numbers. This package provides a modern API to this functionality using GHC generics, allowing the encoding of arbitrary combinations of finite or countably infinite types in natural number form.

As a user, all you need to do is derive generic and get the instances for free.

# Example

import GHC.Generics import Cantor data MyType = MyType { value1 :: [ Maybe Bool ] , value2 :: Integer } deriving (Generic,Cantor)

# Recursive example

This should work nicely even with simple inductive types:

data Tree a = Leaf | Branch (Tree a) a (Tree a) deriving (Generic,Cantor)

# Finite example

If your type is finite, you can specify this by deriving the `Finite`

typeclass, which is a subclass of `Cantor`

:

data Color = Red | Green | Blue deriving (Generic,Cantor,Finite)

# Mutually-recursive types

If you have mutually-recursive types, unfortunately you'll need to manually specify the cardinality for now, but you can still get the to/from encodings for free:

data Foo = FooNil | Foo Bool Bar deriving (Generic,Show) data Bar = BarNil | Bar Bool Foo deriving (Generic,Show) instance Cantor Foo where cardinality = Countable instance Cantor Bar

## Synopsis

- cantorEnumeration :: Cantor a => [a]
- data Cardinality where
- pattern Countable :: Cardinality
- pattern Finite :: Integer -> Cardinality

- class Cantor a where
- cardinality :: Cardinality
- toCantor :: Integer -> a
- fromCantor :: a -> Integer

- class Cantor a => Finite a
- fCardinality :: forall a. Finite a => Integer

# Documentation

cantorEnumeration :: Cantor a => [a] Source #

Enumerates all values of a type by mapping `toCantor`

over the naturals or finite subset of naturals with the correct cardinality.

`>>>`

[fromList [],fromList [0],fromList [1],fromList [0,1],fromList [2]]`take 5 cantorEnumeration :: [ Data.IntSet.IntSet ]`

data Cardinality where Source #

`Cardinality`

can be either `Finite`

or `Countable`

. `Countable`

cardinality entails that a type has the same cardinality as the natural numbers. Note that not all infinite types are countable: for example, `Natural -> Natural`

is an infinite type, but it is not countably infinite; the basic intuition is that there is no possible way to enumerate all values of type `Natural -> Natural`

without "skipping" almost all of them. This is in contrast to the naturals, where despite their being infinite, we can trivially (by definition, in fact!) enumerate all of them without skipping any.

pattern Countable :: Cardinality | |

pattern Finite :: Integer -> Cardinality |

## Instances

Eq Cardinality Source # | |

Defined in Cantor (==) :: Cardinality -> Cardinality -> Bool # (/=) :: Cardinality -> Cardinality -> Bool # | |

Ord Cardinality Source # | |

Defined in Cantor compare :: Cardinality -> Cardinality -> Ordering # (<) :: Cardinality -> Cardinality -> Bool # (<=) :: Cardinality -> Cardinality -> Bool # (>) :: Cardinality -> Cardinality -> Bool # (>=) :: Cardinality -> Cardinality -> Bool # max :: Cardinality -> Cardinality -> Cardinality # min :: Cardinality -> Cardinality -> Cardinality # | |

Show Cardinality Source # | |

Defined in Cantor showsPrec :: Int -> Cardinality -> ShowS # show :: Cardinality -> String # showList :: [Cardinality] -> ShowS # | |

Generic Cardinality Source # | |

Defined in Cantor type Rep Cardinality :: Type -> Type # from :: Cardinality -> Rep Cardinality x # to :: Rep Cardinality x -> Cardinality # | |

type Rep Cardinality Source # | |

Defined in Cantor |

The `Cantor`

class gives a way to convert a type to and from the natural numbers, as well as specifies the cardinality of the type.

Nothing

cardinality :: Cardinality Source #

cardinality :: GCantor a (Rep a) => Cardinality Source #

toCantor :: Integer -> a Source #

toCantor :: (Generic a, GCantor a (Rep a)) => Integer -> a Source #

fromCantor :: a -> Integer Source #

fromCantor :: (Generic a, GCantor a (Rep a)) => a -> Integer Source #

## Instances

class Cantor a => Finite a Source #

The `Finite`

typeclass simply entails that the `Cardinality`

of the set is finite.

## Instances

fCardinality :: forall a. Finite a => Integer Source #

Cardinality of a finite type.