All finite data structures of the same size (cardinality) can be converted between each other and to/from a finite (peano) number

AlgebraicData.hs

{-

Algebraic data is called such because the ways to define a type
correspond to the basic algebra operations for numbers:

An empty type    Void        corresponds to 0
The unit type    ()          corresponds to 1
A sum type       Either x y  corresponds to x + y
A product type   (x, y)      corresponds to x * y

The interpretation of this is that the corresponding number for a type
is the number of possible values it can have.

For example:

data Bool = False  |  True
size Bool =   1    +   1

There are exactly two boolean values, False and True

Same thing for these data types:

type Bool' = Either () ()
size Bool' = (+)    1  1

type Bool'' = Maybe () = Nothing | Just ()
size Bool''            = 1       +      1

The first value: 0 ~ False ~ Left ()  ~ Nothing
The second value: 1 ~ True  ~ Right () ~ Just ()

-----

This module allows you to convert between any two finite (non-recursive)
types of the same size, for example Bool/Bool'/Bool'' above.

It works by converting the data to a natural number between 0
and the size of the type. This constraint is verified on the type-level.

It is kind of like a combination of the Enum and Bounded type classes but type safe.
However, there is of course no guarantee that the isomorphism makes any sense, we just show
that there is a one-to-one correspondance between types of the same size.

-}

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE AllowAmbiguousTypes #-} -- ^ Wouldn't be needed if injective type families were more expressive
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-} -- ^ This would be nice to avoid, but most things would break 
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Wno-orphans #-}
module AlgebraicData where

import Data.Void
import Data.Type.Equality
import qualified GHC.TypeNats as TN
import qualified GHC.Generics as G
import Data.Bifunctor (first, bimap)

-- First we define normal naturals

data Nat = Z | S Nat

type N0 = 'Z
type N1 = 'S N0
type N2 = 'S N1
type N3 = 'S N2
type N4 = 'S N3
type N5 = 'S N4

-- And a convenience function for converting builtin TypeNats to our nats

-- type family N (n :: TN.Nat) = (n' :: Nat) | n' -> n where
type family N (n :: TN.Nat) :: Nat where
    N 0 = 'Z
    N n = 'S (N (n TN.- 1))

-- Plus is injective, but we can't tell GHC that
-- type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a  where
type family Plus a b = (sum :: Nat)  where
    Plus 'Z b = b
    Plus ('S a) b = 'S (Plus a b)

type family Times a b where
    Times 'Z b = 'Z
    Times ('S a) b = Plus b (Times a b) 

-- Then we define Singletons for natural numbers to emulate dependent types
data SNat (n :: Nat) where
    SZ :: SNat 'Z
    SS :: SNat n -> SNat ('S n)

deriving instance Show (SNat n)
-- deriving instance G.Generic (SNat n) -- ^ GHC can't derive generics for GADTs

-- | Class for automatically generating the SNat for a Nat
class KnownSNat (n :: Nat) where
    getSNat :: SNat n
instance KnownSNat 'Z where
    getSNat = SZ
instance KnownSNat n => KnownSNat ('S n) where
    getSNat = SS getSNat

n0 :: SNat N0
n0 = SZ
n1 :: SNat N1
n1 = SS n0
n2 :: SNat N2
n2 = SS n1
n3 :: SNat N3
n3 = SS n2

n15 :: SNat (N 15)
n15 = getSNat

-- Who said Haskell isn't a proof assistant?
plusZ :: SNat n -> Plus n 'Z :~: n
plusZ SZ = Refl
plusZ (SS n) = apply Refl (plusZ n)

plusSuc :: SNat n -> SNat m -> 'S (Plus n m) :~: Plus n ('S m)
plusSuc SZ _ = Refl
plusSuc (SS n) m = apply Refl (plusSuc n m)

-- This is more or less exactly the proof from the agda standard library
plusComm :: SNat n -> SNat m -> Plus n m :~: Plus m n
plusComm SZ m = sym (plusZ m)
plusComm (SS n) m = trans (apply Refl (plusComm n m)) (plusSuc m n)

splus :: SNat n -> SNat m -> SNat (Plus n m)
splus SZ m = m
splus (SS n) m = SS (splus n m)

stimes :: SNat n -> SNat m -> SNat (Times n m)
stimes SZ _ = SZ
stimes (SS n) m = splus m (stimes n m)

spred :: SNat ('S n) -> SNat n
spred (SS n) = n

-- | Finite naturals: `m :: Fin n` means that `0 <= m < n`
data Fin (n :: Nat) where
    FZ :: SNat n -> Fin ('S n)
    FS :: Fin n -> Fin ('S n)

deriving instance Show (Fin n)

enumerateFin :: SNat n -> [Fin n]
enumerateFin SZ = []
enumerateFin (SS n) = FZ n : map FS (enumerateFin n)

finToInt :: Fin n -> Int
finToInt (FZ _) = 0
finToInt (FS n) = 1 + finToInt n

fSize :: Fin n -> SNat n
fSize (FZ n) = SS n
fSize (FS n) = SS (fSize n)

lift :: forall n . Fin n -> Fin ('S n)
lift (FZ n) = FZ (SS n)
lift (FS n) = FS (lift n)

liftN :: SNat n -> Fin m -> Fin (Plus n m)
liftN SZ m = m
liftN (SS n) m = lift $ liftN n m

liftNR :: forall n m. SNat n -> Fin m -> Fin (Plus m n)
liftNR n m = castWith (apply Refl $ plusComm n (fSize m)) $ liftN n m

plusN :: SNat n -> Fin m -> Fin (Plus n m)
plusN SZ m = m
plusN (SS n) m = FS $ plusN n m

plusNR :: forall n m. SNat n -> Fin m -> Fin (Plus m n)
plusNR n m = castWith (apply Refl $ plusComm n (fSize m)) $ plusN n m

getFin :: forall n m. (KnownSNat n, KnownSNat m) => Fin (Plus n ('S m))
getFin = plusN (getSNat @n) $ FZ (getSNat @m)

{-
-- These are not useful

fPlus :: forall n m. Fin n -> Fin m -> Fin (Plus n m)
fPlus (FZ n) m = lift $ liftN n m
fPlus (FS n) m = FS $ fPlus n m

lemma1 :: SNat n -> Fin m -> Fin (Plus m (Times n m))
lemma1 n (FZ m) = FZ $ spred (stimes (SS n) (SS m))
lemma1 n (FS m) = FZ $ spred (stimes (SS n) (SS (fSize m)))

ftimes :: forall n m. Fin n -> Fin m -> Fin (Times n m)
-- ftimes (FZ (n :: SNat ('S n1))) m = _ -- FZ @(Times ('S n1) m) _
-- :: Fin (Plus m (Times n1 m)) 
ftimes (FZ n) m = lemma1 n m --FZ @(Plus m (Times n1 m)) _
ftimes (FS n) m = fPlus m $ ftimes n m
-}

ftimes :: forall n m. Fin n -> Fin m -> Fin (Times n m)
ftimes (FZ n) m = liftNR (stimes n (fSize m)) m
ftimes (FS n) m = plusN (fSize m) $ ftimes n m

class Finite a where
    -- | The number of possible values
    type SizeOf a :: Nat
    -- | Get a singleton for the number above
    getSize :: SNat (SizeOf a)
    -- | 
    toFin :: a -> Fin (SizeOf a)
    fromFin :: Fin (SizeOf a) -> a

instance KnownSNat n => Finite (Fin n) where
    type SizeOf (Fin n) = n
    getSize = getSNat
    toFin :: Fin n -> Fin n
    toFin = id
    fromFin :: Fin n -> Fin n
    fromFin = id

instance KnownSNat n => Finite (SNat n) where
    type SizeOf (SNat n) = N1
    getSize = n1
    toFin :: SNat n -> Fin N1
    toFin _ = FZ SZ
    fromFin :: Fin N1 -> SNat n
    fromFin _ = getSNat

deriving via Generically Void instance Finite Void
deriving via Generically () instance Finite ()
deriving via Generically Bool instance Finite Bool
deriving via Generically (Maybe a) instance Finite a => Finite (Maybe a)
deriving via Generically (Either a b) instance (Finite a, Finite b) =>  Finite (Either a b)

-- This is how the above instances would be written manually

-- instance Finite Void where
--     type instance SizeOf Void = N0
--     getSize = SZ
--     toFin :: Void -> Fin 'Z
--     toFin x = case x of {}
--     fromFin :: Fin 'Z -> Void
--     fromFin x = case x of {}

-- instance Finite () where
--     type instance SizeOf () = N1
--     getSize = SS SZ
--     toFin :: () -> Fin N1
--     toFin () = FZ SZ
--     fromFin :: Fin N1 -> ()
--     fromFin (FZ _) = ()
--     fromFin (FS x) = case x of {}

-- instance Finite Bool where
--     type instance SizeOf Bool = N2
--     getSize = SS (SS SZ)
--     toFin :: Bool -> Fin N2
--     toFin False = FZ (SS SZ)
--     toFin True = FS (FZ SZ)
--     fromFin :: Fin N2 -> Bool
--     fromFin (FZ _) = False
--     fromFin (FS (FZ _)) = True
--     fromFin (FS (FS x)) = case x of {}

-- instance Finite a =>  Finite (Maybe a) where
--     type SizeOf (Maybe a) = 'S (SizeOf a)
--     getSize = SS (getSize @a)
--     toFin :: Finite a => Maybe a -> Fin ('S (SizeOf a))
--     toFin Nothing = FZ (getSize @a)
--     toFin (Just a) = FS $ toFin a
--     fromFin :: Fin ('S (SizeOf a)) -> Maybe a
--     fromFin (FZ _) = Nothing
--     fromFin (FS n) = Just $ fromFin n

splitFinEither :: SNat n -> SNat m -> Fin (Plus n m) -> Either (Fin n) (Fin m)
splitFinEither SZ _ fp = Right fp
splitFinEither (SS n) _ (FZ _fp) = Left $ FZ n
splitFinEither (SS (n :: SNat n')) (m :: SNat m) (FS fp :: Fin (Plus ('S n') m)) 
   = either (Left . FS) Right $ splitFinEither n m (fp :: Fin (Plus n' m))


-- instance (Finite a, Finite b) =>  Finite (Either a b) where
--     type instance SizeOf (Either a b) = Plus (SizeOf a) (SizeOf b)
--     getSize = splus (getSize @a) (getSize @b)
--     -- toFin :: (Finite a, Finite b) => Either a b -> Fin (SizeOf (Either a b))
--     toFin :: (Finite a, Finite b) => Either a b -> Fin (Plus (SizeOf a) (SizeOf b))
--     toFin (Left a) = castWith (apply Refl (plusComm (getSize @b) (getSize @a))) $ liftN (getSize @b) $ toFin a
--     toFin (Right b) = plusN (getSize @a) $ toFin b
--     -- fromFin :: (Finite a, Finite b) => Fin (SizeOf (Either a b)) -> Either a b
--     fromFin :: (Finite a, Finite b) => Fin (Plus (SizeOf a) (SizeOf b)) -> Either a b
--     fromFin  = bimap fromFin fromFin . splitFinEither (getSize @a) (getSize @b) 

splitFinPair :: forall n m. SNat n -> SNat m -> Fin (Times n m) -> (Fin n, Fin m)
splitFinPair SZ _ ft = case ft of {}
-- splitFinPair (SS (n :: SNat n')) m (FZ ft :: Fin (Times ('S n') m)) = _ n m ft
-- splitFinPair (SS n) m (FS ft) = undefined n m ft
splitFinPair (SS n) m ft = case splitFinEither m (stimes n m) ft of
  Left x -> ((,) (FZ n) x)
  Right b ->  first FS $ splitFinPair n m b

instance (Finite a, Finite b) =>  Finite (a, b) where
    type instance SizeOf (a,b) = Times (SizeOf a) (SizeOf b)
    getSize :: SNat (Times (SizeOf a) (SizeOf b))
    getSize = stimes (getSize @a) (getSize @b)
    toFin (a,b) = ftimes (toFin a) (toFin b)
    fromFin :: (Finite a, Finite b) => Fin (SizeOf (a, b)) -> (a, b)
    fromFin = bimap fromFin fromFin . splitFinPair (getSize @a) (getSize @b)


-- | The main result. We can convert between any finite types with the same cardinality
convert :: (Finite a, Finite b, SizeOf a ~ SizeOf b) => a -> b
convert = fromFin . toFin

-- | We can also enumerate any finite type
enumerateFinite :: forall a. Finite a => [a]
enumerateFinite = fromFin <$> enumerateFin (getSize @a)

convert_id :: Finite a => a -> a
convert_id = convert

prop_convert_id :: (Eq a, Finite a) => a -> Bool
prop_convert_id x = x == convert_id x

prop_all_convert_id :: forall a. (Eq a, Finite a) => Bool
prop_all_convert_id = all prop_convert_id $ enumerateFinite @a

-- Orphan instance
instance (Finite a, Eq b) => Eq ((->) a b) where
    a == b = all (\x -> a x == b x) $ enumerateFinite 

--- Generics


instance Finite (f p) =>  Finite (G.M1 i t f p) where
    type SizeOf (G.M1 i t f p) = SizeOf (f p)
    getSize = getSize @(f p)
    toFin :: Finite (f p) => G.M1 i t f p -> Fin (SizeOf (G.M1 i t f p))
    toFin =  toFin . G.unM1
    fromFin = G.M1 . fromFin

instance Finite (G.V1 p) where
    type instance SizeOf (G.V1 p) = N0
    getSize = SZ
    toFin :: G.V1 p -> Fin 'Z
    toFin x = case x of {}
    fromFin :: Fin 'Z -> G.V1 p
    fromFin x = case x of {}

instance (Finite (f p), Finite (g p)) =>  Finite ((f G.:+: g) p) where
    type instance SizeOf ((f G.:+: g) p) = Plus (SizeOf (f p)) (SizeOf (g p))
    getSize = splus (getSize @(f p)) (getSize @(g p))
    -- toFin :: (Finite (f p), Finite (g p)) => (f :+: g) p -> Fin (SizeOf ((f :+: g) p))
    toFin :: (Finite (f p), Finite (g p)) => (f G.:+: g) p -> Fin (Plus (SizeOf (f p)) (SizeOf (g p)))
    toFin (G.L1 a) = castWith (apply Refl (plusComm (getSize @(g p)) (getSize @(f p)))) $ liftN (getSize @(g p)) $ toFin a
    toFin (G.R1 b) = plusN (getSize @(f p)) $ toFin b
    -- fromFin :: (Finite (f p), Finite (g p)) => Fin (SizeOf ((f :+: g) p)) -> (f :+: g) p
    fromFin :: (Finite (f p), Finite (g p)) => Fin (Plus (SizeOf (f p)) (SizeOf (g p))) -> (f G.:+: g) p
    -- fromFin  = bimap fromFin fromFin . eitherToGPlus . splitFinEither (getSize @(f p)) (getSize @(g p)) 
    fromFin  = either (G.L1 . fromFin) (G.R1 . fromFin) . splitFinEither (getSize @(f p)) (getSize @(g p)) 

pairToGPair :: (f p, g p) -> (G.:*:) f g p
pairToGPair (a, b) = a G.:*: b

instance (Finite (f p), Finite (g p)) =>  Finite ((G.:*:) f g p) where
    type instance SizeOf ((G.:*:) f g p) = Times (SizeOf (f p)) (SizeOf (g p))
    getSize :: SNat (Times (SizeOf (f p)) (SizeOf (g p)))
    getSize = stimes (getSize @(f p)) (getSize @(g p))
    toFin (a G.:*: b) = ftimes (toFin a) (toFin b)
    fromFin :: (Finite (f p), Finite (g p)) => Fin (SizeOf ((G.:*:) f g  p)) -> (f G.:*: g) p
    fromFin = pairToGPair . bimap fromFin fromFin . splitFinPair (getSize @(f p)) (getSize @(g p))
    -- fromFin = _ . bimap fromFin fromFin . splitFinPair (getSize @(f p)) (getSize @(g p))

instance Finite (G.U1 p) where
    type instance SizeOf (G.U1 p) = N1
    getSize = SS SZ
    toFin :: G.U1 p -> Fin N1
    toFin G.U1 = FZ SZ
    fromFin :: Fin N1 -> G.U1 p
    fromFin (FZ _) = G.U1
    fromFin (FS x) = case x of {}

-- This is where we could recurse automatically with Generic if we wanted
-- It might also be possible to explicitly prevent recursion here

-- instance (G.Generic c, Finite (G.Rep c ())) =>  Finite (G.K1 i c p) where
--     type SizeOf (G.K1 i c p) = SizeOf (G.Rep c ())
--     getSize = getSize @(G.Rep c ())
--     -- toFin :: Finite c => G.K1 i c p -> Fin (SizeOf (G.K1 i c p))
--     toFin =  gToFin . G.unK1
--     -- fromFin :: Fin (SizeOf c) -> G.K1 i c p
--     fromFin = G.K1 . gFromFin

instance Finite c =>  Finite (G.K1 i c p) where
    type SizeOf (G.K1 i c p) = SizeOf c
    getSize = getSize @c
    toFin :: Finite c => G.K1 i c p -> Fin (SizeOf (G.K1 i c p))
    toFin =  toFin . G.unK1
    fromFin :: Fin (SizeOf c) -> G.K1 i c p
    fromFin = G.K1 . fromFin

newtype Generically c = Generically {getGenerically :: c}

instance (G.Generic c, Finite (G.Rep c ())) =>  Finite (Generically c) where
    type SizeOf (Generically c) = SizeOf (G.Rep c ())
    getSize = getSize @(G.Rep c ())
    toFin =  toFin . G.from @c @() . getGenerically
    -- toFin =  gToFin . getGenerically
    fromFin = Generically . G.to @c @() . fromFin
    -- fromFin = Generically . gFromFin

-- {-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE ConstraintKinds #-}
-- type GFinite x = Finite (G.Rep x ())

-- {-# LANGUAGE FlexibleContexts #-}
-- gToFin :: forall a. (G.Generic a, Finite (G.Rep a ())) => a -> Fin (SizeOf (G.Rep a ()))
-- gToFin = toFin . G.from @a @()
-- gFromFin :: forall a. (G.Generic a, Finite (G.Rep a ())) => Fin (SizeOf (G.Rep a ())) -> a
-- gFromFin = G.to @a @() . fromFin

-- An infinite data structure as an experiment
data Delay = Delay Delay
  deriving (G.Generic)
  -- This fails with stack overflow. It would be better if it failed faster, but better than an infinite loop
  -- deriving Finite via Generically Delay


-- | An example type with three elements
--
-- >>> getSize @Trinary
-- SS (SS (SS SZ))
--
-- >>> toFin T2
-- FS (FZ (SS SZ))
-- 
-- >> finToNat $ toFin T2
-- 2
data Trinary = T1 | T2 | T3
  deriving (G.Generic, Show)
  deriving Finite via Generically Trinary

-- deriving via Generically [a] instance Finite [a]

-- {-# LANGUAGE QuantifiedConstraints #-}
-- {-# LANGUAGE RankNTypes #-}
-- data Finite0 proxy p = Finite0 (Finite p => proxy p)
-- data Finite1 proxy p = Finite1 ((forall a. Finite (p a)) => proxy p)
-- data Finite2 proxy p = Finite2 ((forall a b. Finite (p a b)) => proxy p)