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) instance Cantor MyType
A warning: this package will work with recursive types, but you *must* manually specify the cardinality. This unfortunately is necessary due to GHC generics marking all fields as recursive, regardless of whether or not they actually are. Still, it's straightforward to manually specify the cardinality:
Recursive example
data Tree a = Leaf | Branch (Tree a) a (Tree a) deriving (Generic) instance Cantor a => Cantor (Tree a) where cardinality = Countable
If your type is finite, you can specify this by deriving the Finite
typeclass, which is a subclass of Cantor
:
Finite example
data Color = Red | Green | Blue deriving (Generic) instance Cantor Color instance Finite Color
Synopsis
- cantorEnumeration :: Cantor a => [a]
- data Cardinality
- class Cantor a where
- cardinality :: Cardinality
- toCantor :: Integer -> a
- fromCantor :: a -> Integer
- class Cantor a => Finite a where
Documentation
cantorEnumeration :: Cantor a => [a] Source #
Enumerates all values of a type by mapping toCantor
over the naturals.
data Cardinality 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.
Instances
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 (Rep a) => Cardinality Source #
toCantor :: Integer -> a Source #
toCantor :: (Generic a, GCantor (Rep a)) => Integer -> a Source #
fromCantor :: a -> Integer Source #
fromCantor :: (Generic a, GCantor (Rep a)) => a -> Integer Source #
Instances
class Cantor a => Finite a where Source #
The Finite
typeclass simply entails that the Cardinality
of the set is finite.
Nothing