cantor-pairing 0.1.0.0 → 0.1.1.0

raw patch · 4 files changed

+314/−136 lines, 4 filesdep +integer-logarithmsdep +mtldep ~arithmoidep ~basedep ~containersPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: integer-logarithms, mtl

Dependency ranges changed: arithmoi, base, containers, integer-gmp

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−2
• cantor-pairing.cabal +7/−4
• src/Cantor.hs +287/−130
• test/Spec.hs +16/−0

@@ -1,5 +1,7 @@ # Revision history for cantor-pairing -## 0.1.0.0 -- YYYY-mm-dd+## 0.1.1.0 -* First version. Released on an unsuspecting world.+- Instances for `Int`, `Word`, `IntSet`, and `Set+- Basic recursion is now detected generically, so there is now no need to manually specify that the cardinality is `Countable`+

@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                cantor-pairing-version:             0.1.0.0+version:             0.1.1.0 synopsis:            Convert data to and from a natural number representation description:         Convert data to and from a natural number representation conveniently using GHC Generics. homepage:            https://github.com/identicalsnowflake/cantor-pairing@@ -26,6 +26,7 @@                      , base ^>=4.12.0.0                      , containers ^>= 0.6.0.1                      , integer-gmp ^>= 1.0.2.0+                     , integer-logarithms ^>= 1.0.2.2   hs-source-dirs:      src   ghc-options: -Wall -Wextra   default-language:    Haskell2010@@ -35,9 +36,11 @@   type: exitcode-stdio-1.0   main-is: test/Spec.hs   build-depends:-      base-    , cantor-pairing-    , hspec >= 2 && < 3+                  base+                , cantor-pairing+                , containers+                , hspec >= 2 && < 3+                , mtl >= 2.2.2   build-tool-depends: hspec-discover:hspec-discover   default-language:    Haskell2010 

@@ -1,8 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -25,14 +28,13 @@ -- -- 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:+-- This should work nicely even with simple inductive types: --  -- = Recursive example -- @ -- data Tree a = Leaf | Branch (Tree a) a (Tree a) deriving (Generic) ----- instance Cantor a => Cantor (Tree a) where---   cardinality = Countable+-- instance Cantor a => Cantor (Tree a) -- @ -- -- If your type is finite, you can specify this by deriving the @Finite@ typeclass, which is a subclass of @Cantor@:@@ -46,8 +48,8 @@ -- @ -- -module Cantor (-         cantorEnumeration+module Cantor+       ( cantorEnumeration        , Cardinality(..)        , Cantor(..)        , Finite(..)@@ -60,12 +62,19 @@ import GHC.Natural import Data.Semigroup import Data.Functor.Identity-import Data.Functor.Const+import qualified Data.Functor.Const import Data.Proxy import Math.NumberTheory.Powers.Squares (integerSquareRoot') import Data.Void-import qualified Data.Map as M+import Data.Bits (finiteBitSize)+import Data.Bits+import Data.Foldable (foldl')+import Math.NumberTheory.Logarithms +import qualified Data.Map as M+import qualified Data.Sequence+import qualified Data.Set+import qualified Data.IntSet  -- internal value-level representation, currently only used for function enumeration data ESpace a = ESpace {@@ -87,7 +96,9 @@   Finite i -> te <$> [ 0 .. (i - 1) ]   Countable -> te <$> [ 0 .. ] --- | Enumerates all values of a type by mapping @toCantor@ over the naturals.+-- | Enumerates all values of a type by mapping @toCantor@ over the naturals or finite subset of naturals with the correct cardinality.+-- +-- If the cardinality of the type is large and finite, (e.g., @IntSet@), you will need to try fixing the amount of items you want instead like @toCantor @IntSet <$> [ 0 .. 10 ]@. This is unfortunately necessary because even though the list is computed lazily in @cantorEnumeration@, its *size* is not, and the size of @IntSet@ is a *very* large number which is not feasible to compute even on a modern system (it has more than 200k terabytes of digits!). Note that if you defer to using even larger types like @Integer@ which have true non-finite cardinality instead of finite approximations like @Int@, you will naturally tend to avoid this problem. cantorEnumeration :: Cantor a => [ a ] cantorEnumeration = enumerateSpace defaultSpace @@ -132,20 +143,20 @@ class Cantor a where   cardinality :: Cardinality   -  default cardinality :: (GCantor (Rep a)) => Cardinality-  cardinality = gCardinality @(Rep a)+  default cardinality :: GCantor a (Rep a) => Cardinality+  cardinality = gCardinality' @a @(Rep a)      toCantor :: Integer -> a -- ideally this should be `Fin n -> a` (for finite types)                            -- or `N` (for countably infinite types).                            -- I chose not to use `Natural` from `GHC.Natural`                            -- because it's turned out to be a huge pain and integrates                            -- poorly with the haskell ecosystem-  default toCantor :: (Generic a , GCantor (Rep a)) => Integer -> a-  toCantor = to . gToCantor+  default toCantor :: (Generic a , GCantor a (Rep a)) => Integer -> a+  toCantor = to . gToCantor' @a @(Rep a)    fromCantor :: a -> Integer-  default fromCantor :: (Generic a , GCantor (Rep a)) => a -> Integer-  fromCantor = gFromCantor . from+  default fromCantor :: (Generic a , GCantor a (Rep a)) => a -> Integer+  fromCantor = gFromCantor' @a @(Rep a) . from     instance Cantor Natural where@@ -218,7 +229,7 @@  instance Finite Int instance Cantor Int where-  cardinality = Finite $ 2 ^ (64 :: Integer)+  cardinality = Finite $ 2 ^ (finiteBitSize @Int undefined)   toCantor = fromInteger . toCantor @Integer   fromCantor = fromCantor @Integer . toInteger @@ -246,6 +257,12 @@   toCantor = fromIntegral   fromCantor = fromIntegral +instance Finite Word+instance Cantor Word where+  cardinality = Finite $ 2 ^ (finiteBitSize @Word undefined)+  toCantor = fromIntegral +  fromCantor =  fromIntegral+ instance Finite Char instance Cantor Char where   cardinality = Finite . fromIntegral $ (fromEnum (maxBound :: Char) :: Int) + 1@@ -264,7 +281,7 @@ instance Cantor a => Cantor (Last a) instance Cantor a => Cantor (First a) instance Cantor a => Cantor (Identity a)-instance Cantor a => Cantor (Const a b)+instance Cantor a => Cantor (Data.Functor.Const.Const a b) instance Cantor a => Cantor (Option a) instance Cantor a => Cantor (Min a) instance Cantor a => Cantor (Max a)@@ -286,7 +303,7 @@ instance Finite a => Finite (Last a) instance Finite a => Finite (First a) instance Finite a => Finite (Identity a)-instance Finite a => Finite (Const a b)+instance Finite a => Finite (Data.Functor.Const.Const a b) instance Finite a => Finite (Option a) instance Finite a => Finite (Min a) instance Finite a => Finite (Max a)@@ -296,43 +313,146 @@ instance Finite a => Finite (Maybe a) instance (Finite a , Finite b) => Finite (Either a b) +instance Cantor a => Cantor [ a ]+instance Cantor a => Cantor (Data.Sequence.Seq a) where+  cardinality = cardinality @[ a ]+  toCantor = Data.Sequence.fromList . toCantor+  fromCantor = fromCantor . foldr (:) [] --- due to generics issues below, when making recursive instances, cardinality must--- manually be specified-instance Cantor a => Cantor [ a ] where-  cardinality = Countable+-- this algorithm is correct, but too slow for large a+-- instance (Ord a , Finite a , Cantor b) => Cantor (M.Map a b) where+--   cardinality = cardinality @(a -> Maybe b)+--   toCantor i = m+--     where+--       m :: M.Map a b+--       m = M.fromList $ mapMaybe (\(a,w) -> (,) a <$> w) $ zip (toCantor <$> [ 0 .. ]) (eToCantor es i)+      +--       es :: ESpace [ Maybe b ]+--       es = nary (fCardinality @a) defaultSpace --- how to memoise gCardinality??-class GCantor f where-  gCardinality :: Cardinality+--   fromCantor g = eFromCantor es . fmap (\i -> M.lookup (toCantor i) g) $ [ 0 .. (fCardinality @a - 1) ]+--     where+--       es :: ESpace [ Maybe b ]+--       es = nary (fCardinality @a) defaultSpace -  gToCantor :: Integer -> f a-  gFromCantor :: f a -> Integer+-- instance (Ord a , Finite a , Finite b) => Finite (M.Map a b) -instance GCantor V1 where-  gCardinality = Finite 0-  gToCantor _ = error "Cantor bounds error."-  gFromCantor _ = error "Cantor bounds error."+-- espace for `Set (Fin c)`+fSetEnum :: Integer -> ESpace (Data.Set.Set Integer)+fSetEnum c = ESpace (Finite (2 ^ c)) t f+  where+    t :: Integer -> Data.Set.Set Integer+    t 0 = Data.Set.empty+    t m = Data.Set.fromAscList $ foldr g mempty [ 0 .. (integerLog2 m + 1) ]+      where+        g :: Int -> [ Integer ] -> [ Integer ]+        g i s = if testBit m i+          then toInteger i : s+          else s -instance GCantor U1 where-  gCardinality = Finite 1-  gToCantor _ = U1-  gFromCantor _ = 0+    f :: Data.Set.Set Integer -> Integer+    f = foldl' g 0+      where+        g :: Integer -> Integer -> Integer+        g a i = setBit a (fromInteger i) -nary :: Integer -> ESpace a -> ESpace [ a ]-nary 0 _ = undefined-nary 1 (ESpace c t f) = ESpace c (\i -> [ t i ]) $ \case-  [ x ] -> f x-  _ -> undefined-nary i es = case es *** nary (i - 1) es of-  ESpace c t f -> ESpace c t' f'+instance (Ord a , Finite a) => Cantor (Data.Set.Set a) where+  cardinality = Finite (2 ^ fCardinality @a)+  -- would be nice to map monotonic and save a log here, but that only works when+  -- Ord a respects the ordering on Integer, which we have no assurance of+  toCantor = Data.Set.map toCantor . eToCantor (fSetEnum (fCardinality @a))+  fromCantor = eFromCantor (fSetEnum (fCardinality @a)) . Data.Set.map fromCantor++instance (Ord a , Finite a) => Finite (Data.Set.Set a)++-- espace for `IntSet (Fin c)`, where c is in proper range+fSetEnum' :: Integer -> ESpace Data.IntSet.IntSet+fSetEnum' c = ESpace (Finite (2 ^ c)) t f+  where+    t :: Integer -> Data.IntSet.IntSet+    t 0 = Data.IntSet.empty+    t m = Data.IntSet.fromAscList $ foldr g mempty [ 0 .. (integerLog2 m + 1) ]+      where+        g :: Int -> [ Int ] -> [ Int ]+        g i s = if testBit m i+          then i : s+          else s++    f :: Data.IntSet.IntSet -> Integer+    f = Data.IntSet.foldl' g 0+      where+        g :: Integer -> Int -> Integer+        g a i = setBit a i++instance Cantor Data.IntSet.IntSet where+  cardinality = Finite (2 ^ fCardinality @Int)+  toCantor = eToCantor (fSetEnum' (fCardinality @Int))+  fromCantor = eFromCantor (fSetEnum' (fCardinality @Int))++instance Finite Data.IntSet.IntSet++-- this algorithm is wrong; only works on Countable a.+-- instance Cantor a => Cantor (Data.IntMap.Lazy.IntMap a) where+--   cardinality = case cardinality @a of+--     Countable -> Countable+--     Finite c -> Finite $ (c + 1) ^ fCardinality @Int+--   toCantor i = if i == 0 then mempty else case cantorSplit i of+--     (j , k) -> Data.IntMap.Lazy.fromAscList $ zip (Data.IntSet.toAscList s) as+--       where+--         s :: Data.IntSet.IntSet+--         s = toCantor (j + 1)++--         es :: ESpace [ a ]+--         es = nary (toInteger (Data.IntSet.size s)) defaultSpace++--         as :: [ a ]+--         as = eToCantor es k+--   fromCantor m = if Data.IntMap.Lazy.null m then 0 else case unzip (Data.IntMap.Lazy.toAscList m) of+--     (is , as) -> cantorUnsplit (fromCantor s , eFromCantor es as)+--       where+--         s = Data.IntSet.fromAscList is+  +--         es :: ESpace [ a ]+--         es = nary (toInteger (Data.IntSet.size s)) defaultSpace++-- instance Finite a => Finite (Data.IntMap.Lazy.IntMap a)+++-- ES is just an alias to get in a position to use stimes for nary to get the nice algorithm+data ES a = ES !Int (ESpace (Endo [ a ])) (ESpace [ a ])++instance Semigroup (ES a) where+  (<>) (ES a x x') (ES b y y') = ES (a + b) s1 s2     where-      t' j = case t j of-        (a , as) -> a : as+      s1 :: ESpace (Endo [ a ])+      s1 = case x ***  y of+        (ESpace c f _) -> ESpace c f' undefined+          where+            f' :: Integer -> Endo [ a ]+            f' i = case f i of+             (xs , ys) -> xs <> ys -      f' (a : as) = f (a , as)-      f' _ = undefined+      s2 :: ESpace [ a ]+      s2 = case x' *** y' of+        (ESpace c _ t) -> ESpace c undefined t'+          where+            t' :: [ a ] -> Integer+            t' = t . splitAt a +nary :: forall a . Integer -> ESpace a -> ESpace [ a ]+nary 0 _ = undefined+nary i (ESpace c f t) = case stimes i es' of+  (ES _ (ESpace c' f' _) (ESpace _ _ t')) -> ESpace c' (flip appEndo [] . f') t'+  where+    toE :: [ a ] -> Endo [ a ]+    toE = Endo . (<>)+    +    es' :: ES a+    es' = ES 1 (ESpace c (\j -> toE [ f j ]) undefined) $ ESpace c undefined $ \case+      [ x ] -> t x+      _ -> error "Bounds error."++ infixr 7 *** (***) :: forall a b . ESpace a -> ESpace b -> ESpace (a , b) (***) (ESpace (Finite ca) tea fea) (ESpace (Finite cb) teb feb) =@@ -458,14 +578,66 @@      fec (a , b) = cantorUnsplit (fea a , feb b) -instance (GCantor a , GCantor b) => GCantor (a :*: b) where-  gCardinality = case (gCardinality @a , gCardinality @b) of++-- https://en.wikipedia.org/wiki/Pairing_function#Cantor_pairing_function+-- adapted for integer square rooting in the w, which should yield the same result+-- but benchmarks significantly faster. buuut on closer inspection that makes no sense, since+-- this is exactly what arithmoi is doing anyway...+--+-- also, maybe try this https://gist.github.com/orlp/3481770+cantorSplit :: Integer -> (Integer , Integer)+cantorSplit i = +  let w = (integerSquareRoot' (8 * i + 1) - 1) `div` 2 +      -- original implementation (convert to/from float for the sqrt)+      -- w :: Int = floor (0.5 * (sqrt (8 * fromIntegral i + 1 :: Double) - 1))+      t = (w^(2 :: Int) + w) `quot` 2+      y = i - t+      x = w - y+  in+  (x , y)++cantorUnsplit :: (Integer , Integer) -> Integer+cantorUnsplit (x , y) = (((x + y + 1) * (x + y)) `quot` 2) + y++class GCantor s f where+  hasExit :: Bool+  gCardinality' :: Cardinality+  gToCantor' :: Integer -> f a+  gFromCantor' :: f a -> Integer++instance GCantor s V1 where+  hasExit = False+  gCardinality' = Finite 0+  gToCantor' = undefined+  gFromCantor' = undefined++instance GCantor s U1 where+  hasExit = True+  gCardinality' = Finite 1+  gToCantor' _ = U1+  gFromCantor' _ = 0++instance {-# OVERLAPPING #-} Cantor a => GCantor a (K1 i a) where+  hasExit = False+  gCardinality' = Countable+  gToCantor' = K1 . toCantor+  gFromCantor' (K1 x) = fromCantor x++instance {-# OVERLAPPABLE #-} Cantor b => GCantor w (K1 i b) where+  hasExit = True+  gCardinality' = cardinality @b+  gToCantor' = K1 . toCantor+  gFromCantor' (K1 x) = fromCantor x++instance (GCantor s a , GCantor s b) => GCantor s (a :*: b) where+  hasExit = hasExit @s @a && hasExit @s @b+  gCardinality' = case (gCardinality' @s @a , gCardinality' @s @b) of     (Finite i , Finite j) -> Finite (i * j)     (Finite 0 , _) -> Finite 0     (_ , Finite 0) -> Finite 0     _ -> Countable -  gToCantor i = case (gCardinality @a , gCardinality @b) of+  gToCantor' i = case (gCardinality' @s @a , gCardinality' @s @b) of     (Finite ca , Finite cb) ->       let par_s = min ca cb -- small altitude of the parallelogram           tri_l = par_s - 1@@ -475,7 +647,7 @@       if i < tri_a          then -- we're in the triangle, so just use cantor               case cantorSplit i of-                (a , b) -> (gToCantor a :*: gToCantor b)+                (a , b) -> (gToCantor' @s @a a :*: gToCantor' @s @b b)          else let j = i - tri_a -- shadowing would make this so much safer, alas...                   par_l = max ca cb - tri_l                   par_a = par_s * par_l in@@ -490,11 +662,11 @@                                           then (c2 , c1)                                           else (c1 , c2)                           in-                          (gToCantor a :*: gToCantor b)+                          (gToCantor' @s @a a :*: gToCantor' @s @b b)                  else let k = j - par_a                           l = tri_a - (k + 1) in                       case cantorSplit l of-                        (a , b) -> (gToCantor (ca - (a + 1)) :*: gToCantor (cb - (b + 1)))+                        (a , b) -> (gToCantor' @s @a (ca - (a + 1)) :*: gToCantor' @s @b (cb - (b + 1)))     (Finite ca , Countable) ->       let par_s = ca -- small altitude of the parallelogram           tri_l = par_s - 1@@ -502,7 +674,7 @@       in       if i < tri_a          then case cantorSplit i of-                (a , b) -> (gToCantor a :*: gToCantor b)+                (a , b) -> (gToCantor' @s @a a :*: gToCantor' @s @b b)          else let j = i - tri_a -- shadowing would make this so much safer, alas...               in               case divModInteger j par_s of@@ -511,7 +683,7 @@                       c2 = s                       (a , b) = (c2 , c1)                   in-                  (gToCantor a :*: gToCantor b)+                  (gToCantor' @s @a a :*: gToCantor' @s @b b)            (Countable , Finite cb) ->       let par_s = cb -- small altitude of the parallelogram@@ -520,7 +692,7 @@       in       if i < tri_a          then case cantorSplit i of-                (a , b) -> (gToCantor a :*: gToCantor b)+                (a , b) -> (gToCantor' @s @a a :*: gToCantor' @s @b b)          else let j = i - tri_a -- shadowing would make this so much safer, alas...               in               case divModInteger j par_s of@@ -529,13 +701,13 @@                       c2 = s                       (a , b) = (c1 , c2)                   in-                  (gToCantor a :*: gToCantor b)+                  (gToCantor' @s @a a :*: gToCantor' @s @b b)     _ -> case cantorSplit i of-      (a , b) -> (gToCantor a :*: gToCantor b)+      (a , b) -> (gToCantor' @s @a a :*: gToCantor' @s @b b)   -  gFromCantor (a :*: b) = case (gCardinality @a , gCardinality @b) of+  gFromCantor' (a :*: b) = case (gCardinality' @s @a , gCardinality' @s @b) of     (Finite ca , Finite cb) ->-      let (x , y) = (gFromCantor a , gFromCantor b)+      let (x , y) = (gFromCantor' @s @a a , gFromCantor' @s @b b)           par_s = min ca cb           tri_l = par_s - 1       in@@ -553,7 +725,7 @@                       in                       tri_a + x' + y' * par_s     (Finite ca , Countable) ->-      let (x , y) = (gFromCantor a , gFromCantor b)+      let (x , y) = (gFromCantor' @s @a a , gFromCantor' @s @b b)           par_s = ca           tri_l = par_s - 1       in@@ -564,7 +736,7 @@               in               tri_a + x' + y' * par_s     (Countable , Finite cb) ->-      let (x , y) = (gFromCantor a , gFromCantor b)+      let (x , y) = (gFromCantor' @s @a a , gFromCantor' @s @b b)           par_s = cb           tri_l = par_s - 1       in@@ -574,89 +746,74 @@                   tri_a = (tri_l * (tri_l + 1)) `div` 2               in               tri_a + x' + y' * par_s-    _ -> cantorUnsplit (gFromCantor a , gFromCantor b)+    _ -> cantorUnsplit (gFromCantor' @s @a a , gFromCantor' @s @b b) --- https://en.wikipedia.org/wiki/Pairing_function#Cantor_pairing_function--- adapted for integer square rooting in the w, which should yield the same result--- but benchmarks significantly faster. buuut on closer inspection that makes no sense, since--- this is exactly what arithmoi is doing anyway...------ also, maybe try this https://gist.github.com/orlp/3481770-cantorSplit :: Integer -> (Integer , Integer)-cantorSplit i = -  let w = (integerSquareRoot' (8 * i + 1) - 1) `div` 2 -      -- original implementation (convert to/from float for the sqrt)-      -- w :: Int = floor (0.5 * (sqrt (8 * fromIntegral i + 1 :: Double) - 1))-      t = (w^(2 :: Int) + w) `quot` 2-      y = i - t-      x = w - y-  in-  (x , y) -cantorUnsplit :: (Integer , Integer) -> Integer-cantorUnsplit (x , y) = (((x + y + 1) * (x + y)) `quot` 2) + y--instance (GCantor a , GCantor b) => GCantor (a :+: b) where-  gCardinality = case (gCardinality @a , gCardinality @b) of+-- in this instance, make sure we head towards the exit if there is one, otherwise we can get+-- stuck endlessly in the labyrinth+instance (GCantor s a , GCantor s b) => GCantor s (a :+: b) where+  hasExit = hasExit @s @a || hasExit @s @b+  gCardinality' = case (gCardinality' @s @a , gCardinality' @s @b) of     (Finite i , Finite j) -> Finite (i + j)     _ -> Countable -  gToCantor i = case (gCardinality @a , gCardinality @b) of+  gToCantor' i = case (gCardinality' @s @a , gCardinality' @s @b) of     (Finite ca , Finite cb) -> if i < 2 * min ca cb       then case divModInteger i 2 of-        (# k , 0 #) -> L1 $ gToCantor k-        (# k , _ #) -> R1 $ gToCantor k+        (# k , 0 #) -> L1 $ gToCantor' @s @a k+        (# k , _ #) -> R1 $ gToCantor' @s @b k       else if ca > cb-           then L1 $ gToCantor (i - cb)-           else R1 $ gToCantor (i - ca)+           then L1 $ gToCantor' @s @a (i - cb)+           else R1 $ gToCantor' @s @b (i - ca)     (Finite ca , Countable) -> if i < 2 * ca       then case divModInteger i 2 of-        (# k , 0 #) -> L1 $ gToCantor k-        (# k , _ #) -> R1 $ gToCantor k-      else R1 $ gToCantor (i - ca)-    (Countable , Finite cb) -> if i < 2 * cb-      then case divModInteger i 2 of-        (# k , 0 #) -> L1 $ gToCantor k-        (# k , _ #) -> R1 $ gToCantor k-      else L1 $ gToCantor (i - cb)-    _ -> case divModInteger i 2 of-      (# k , 0 #) -> L1 $ gToCantor k-      (# k , _ #) -> R1 $ gToCantor k+        (# k , 0 #) -> L1 $ gToCantor' @s @a k+        (# k , _ #) -> R1 $ gToCantor' @s @b k+      else R1 $ gToCantor' @s @b (i - ca)+    (Countable , Finite _) -> case gToCantor' @s @(b :+: a) i of+      L1 x -> R1 x+      R1 x -> L1 x+    _ -> if not (hasExit @s @a) && hasExit @s @b+            then case gToCantor' @s @(b :+: a) i of+              L1 x -> R1 x+              R1 x -> L1 x+            else case divModInteger i 2 of+             (# k , 0 #) -> L1 $ gToCantor' @s @a k+             (# k , _ #) -> R1 $ gToCantor' @s @b k -  gFromCantor (L1 x) = case gCardinality @b of-    Finite cb -> case gFromCantor x of-      0 -> 0-      i -> i + min cb i-    Countable -> case gFromCantor x of-      0 -> 0-      i -> 2 * i-  gFromCantor (R1 x) = case gCardinality @a of-    Finite ca -> case gFromCantor x of+  gFromCantor' (L1 x) = case gCardinality' @s @b of+    Finite cb -> case gCardinality' @s @a of+      Countable -> gFromCantor' @s @(b :+: a) $ R1 x+      _ -> case gFromCantor' @s @a x of+        0 -> 0+        i -> i + min cb i+    Countable -> case gCardinality' @s @a of+      Countable -> if not (hasExit @s @a) && hasExit @s @b+        then gFromCantor' @s @(b :+: a) $ R1 x+        else case gFromCantor' @s @a x of+          0 -> 0+          i -> 2 * i+      _ -> case gFromCantor' @s @a x of+        0 -> 0+        i -> 2 * i+  gFromCantor' (R1 x) = case gCardinality' @s @a of+    Finite ca -> case gFromCantor' @s @b x of       0 -> 1       i -> i + min ca (i + 1)-    Countable -> case gFromCantor x of-      0 -> 1-      i -> 2 * i + 1- --- this SHOULD work at least in basic cases,--- but GHC generic deriving does not properly distinguish between--- K1 i for non-recursive cases and K1 R for recursive cases -______---- instance {-# OVERLAPPING #-} Cantor a => GCantor (K1 R a) where---   gCardinality = Countable---   gToCantor i = K1 $ toCantor i---   gFromCantor (K1 x) = fromCantor x--instance (Cantor a) => GCantor (K1 i a) where-  gCardinality = cardinality @a--  gToCantor x = K1 (toCantor x)--  gFromCantor (K1 x) = fromCantor x--instance (GCantor f) => GCantor (M1 i t f) where-  gCardinality = gCardinality @f+    Countable -> case gCardinality' @s @b of+      Finite _ -> gFromCantor' @s @(b :+: a) $ L1 x+      Countable -> if not (hasExit @s @a) && hasExit @s @b+        then gFromCantor' @s @(b :+: a) $ L1 x+        else case gFromCantor' @s @b x of+          0 -> 1+          i -> 2 * i + 1 -  gToCantor x = M1 (gToCantor x)+instance GCantor s f => GCantor s (M1 i t f) where+  hasExit = hasExit @s @f -  gFromCantor (M1 x) = gFromCantor x+  gCardinality' = gCardinality' @s @f+  +  gToCantor' = M1 . gToCantor' @s @f+  +  gFromCantor' (M1 x) = gFromCantor' @s @f x 

@@ -13,12 +13,21 @@  import Cantor +data TreeL a = NodeL | BranchL (TreeL a) a (TreeL a) deriving (Generic,Eq) +instance Cantor a => Cantor (TreeL a)++data TreeR a = BranchR (TreeR a) a (TreeR a) | NodeR deriving (Generic,Eq)++instance Cantor a => Cantor (TreeR a)++ instance (Finite a , Cantor b) => Eq (a -> b) where   (==) f g = fmap (fromCantor . f) cantorEnumeration == fmap (fromCantor . g) cantorEnumeration  data C = R | G | B deriving (Generic,Eq,Ord,Show,Cantor,Finite) + main :: IO () main = hspec $ do   describe "cardinality" $ do@@ -105,6 +114,13 @@          it "for [ C -> Integer ]" $       (checkUISO @([ (C -> Integer) ])) `shouldBe` True++    it "for TreeL Bool" $+      (checkUISO @(TreeL Bool)) `shouldBe` True      ++    it "for TreeR Bool" $+      (checkUISO @(TreeR Bool)) `shouldBe` True+        where     fcheckUISO :: forall a . (Eq a , Finite a) => Bool