{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
import Data.Void
import GHC.Generics (Generic)
import Test.Hspec
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
it "returns 3 for the cardinality of C" $ do
(fCardinality @C) `shouldBe` 3
it "returns 9 for the cardinality of C x C" $
(fCardinality @(C , C)) `shouldBe` 9
it "returns 6 for the cardinality of Bool x C" $
(fCardinality @(Bool , C)) `shouldBe` 6
it "returns 9 for the cardinality of C x Bool" $
(fCardinality @(C , Bool)) `shouldBe` 6
it "returns 0 for the cardinality of Void x Bool" $
(fCardinality @(Void , Bool)) `shouldBe` 0
it "returns 0 for the cardinality of Bool x Void" $
(fCardinality @(Bool , Void)) `shouldBe` 0
it "returns Countable for the cardinality of Bool x Integer" $
(cardinality @(Bool , Integer)) `shouldBe` Countable
it "returns Countable for the cardinality of Integer x Bool" $
(cardinality @(Integer , Bool)) `shouldBe` Countable
it "returns Finite 0 for the cardinality of Void x Integer" $
(cardinality @(Void , Integer)) `shouldBe` Finite 0
it "returns Finite 0 for the cardinality of Integer x Void" $
(cardinality @(Integer , Void)) `shouldBe` Finite 0
it "returns 8 for the cardinality of (C -> Bool)" $
(fCardinality @(C -> Bool)) `shouldBe` 8
it "returns 9 for the cardinality of (Bool -> C)" $
(fCardinality @(Bool -> C)) `shouldBe` 9
it "returns Countable for the cardinality of (Bool -> Integer)" $
(cardinality @(Bool -> Integer)) `shouldBe` Countable
it "returns Countable for the cardinality of [ C ]" $
(cardinality @([ C ])) `shouldBe` Countable
describe "uniqueness and isomorphism for finite types" $ do
it "for C" $
(fcheckUISO @C) `shouldBe` True
it "for C x Bool" $
(fcheckUISO @(C , Bool)) `shouldBe` True
it "for Bool x C" $
(fcheckUISO @(Bool , C)) `shouldBe` True
it "for (Bool x Bool) x C" $
(fcheckUISO @((Bool , Bool) , C)) `shouldBe` True
it "for Void x C" $
(fcheckUISO @(Void , C)) `shouldBe` True
it "for C x Void" $
(fcheckUISO @(C , Void)) `shouldBe` True
it "for C -> Bool" $
(fcheckUISO @(C -> Bool)) `shouldBe` True
it "for Bool -> C" $
(fcheckUISO @(Bool -> C)) `shouldBe` True
describe "uniqueness and isomorphism for countable types" $ do
it "for C x Integer" $
(checkUISO @(C , Integer)) `shouldBe` True
it "for Integer x C" $
(checkUISO @(C , Integer)) `shouldBe` True
it "for Integer x Integer" $
(checkUISO @(Integer , Integer)) `shouldBe` True
it "for C -> Integer" $
(checkUISO @(C -> Integer)) `shouldBe` True
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
describe "function enumeration even for large domains" $ do
it "should be fast" $
(head (cantorEnumeration @(Word -> Int)) 42173) `shouldBe` 0
where
fcheckUISO :: forall a . (Eq a , Finite a) => Bool
fcheckUISO = e == fmap (toCantor . fromCantor) e
where
e :: [ a ]
e = cantorEnumeration
checkUISO :: forall a . (Eq a , Cantor a) => Bool
checkUISO = e == fmap (toCantor . fromCantor) e
where
e :: [ a ]
e = take 5000 cantorEnumeration