module Data.Type.Ordinal
(
Ordinal (..), pattern OZ, pattern OS, HasOrdinal,
mkOrdinalQQ, odPN, odLit,
sNatToOrd', sNatToOrd, ordToInt, ordToSing,
unsafeFromInt, inclusion, inclusion',
(@+), enumOrdinal,
absurdOrd, vacuousOrd
) where
import Data.Kind
import Data.List (genericDrop, genericTake)
import Data.Ord (comparing)
import Data.Singletons.Decide
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Enum
import Data.Type.Equality
import Data.Type.Monomorphic
import qualified Data.Type.Natural as PN
import Data.Type.Natural.Builtin ()
import Data.Type.Natural.Class
import Data.Typeable (Typeable)
import Data.Void (absurd)
import GHC.TypeLits (type (+))
import qualified GHC.TypeLits as TL
import Language.Haskell.TH hiding (Type)
import Language.Haskell.TH.Quote
import Proof.Equational
import Proof.Propositional
import Unsafe.Coerce
data Ordinal (n :: nat) where
OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m
fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m)
=> Sing (n :: nat) -> Ordinal m
fromOLt n =
withRefl (sym $ succLneqSucc n (sing :: Sing m)) $
OLt n
pattern OZ :: forall nat (n :: nat). IsPeano nat
=> (Zero nat :< n) ~ 'True => Ordinal n
pattern OZ <- OLt Zero where
OZ = OLt sZero
pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t)
=> (IsPeano nat)
=> Ordinal t -> Ordinal (Succ t)
pattern OS n <- OLt (Succ (fromOLt -> n)) where
OS o = succOrd o
deriving instance Typeable Ordinal
class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),
Integral (MonomorphicRep (Sing :: nat -> *)),
Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat
instance (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),
Integral (MonomorphicRep (Sing :: nat -> *)),
Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat
instance (HasOrdinal nat, SingI (n :: nat))
=> Num (Ordinal n) where
_ + _ = error "Finite ordinal is not closed under addition."
_ _ = error "Ordinal subtraction is not defined"
negate OZ = OZ
negate _ = error "There are no negative oridnals!"
OZ * _ = OZ
_ * OZ = OZ
_ * _ = error "Finite ordinal is not closed under multiplication"
abs = id
signum = error "What does Ordinal sign mean?"
fromInteger = unsafeFromInt' (Proxy :: Proxy nat) . fromInteger
instance (SingI n, HasOrdinal nat)
=> Show (Ordinal (n :: nat)) where
showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n)))
instance (HasOrdinal nat)
=> Eq (Ordinal (n :: nat)) where
o == o' = ordToInt o == ordToInt o'
instance (HasOrdinal nat) => Ord (Ordinal (n :: nat)) where
compare = comparing ordToInt
instance (HasOrdinal nat, SingI n)
=> Enum (Ordinal (n :: nat)) where
fromEnum = fromIntegral . ordToInt
toEnum = unsafeFromInt' (Proxy :: Proxy nat) . fromIntegral
enumFrom = enumFromOrd
enumFromTo = enumFromToOrd
enumFromToOrd :: forall (n :: nat).
(HasOrdinal nat, SingI n)
=> Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd ok ol =
let k = ordToInt ok
l = ordToInt ol
in genericTake (l k + 1) $ enumFromOrd ok
enumFromOrd :: forall (n :: nat).
(HasOrdinal nat, SingI n)
=> Ordinal n -> [Ordinal n]
enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n)
enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n]
enumOrdinal (Succ n) = withSingI n $
withWitness (lneqZero n) $
OLt sZero : map succOrd (enumOrdinal n)
enumOrdinal _ = []
succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n)
succOrd (OLt n) =
withRefl (succLneqSucc n (sing :: Sing n)) $
OLt (sSucc n)
instance SingI n => Bounded (Ordinal ('PN.S n)) where
minBound = OLt PN.SZ
maxBound =
withWitness (leqRefl (sing :: Sing n)) $
sNatToOrd (sing :: Sing n)
instance (SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) where
minBound =
withWitness (lneqZero (sing :: Sing m)) $
OLt (sing :: Sing 0)
maxBound =
withWitness (lneqSucc (sing :: Sing m)) $
sNatToOrd (sing :: Sing m)
unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))
=> MonomorphicRep (Sing :: nat -> *) -> Ordinal n
unsafeFromInt n =
case promote (n :: MonomorphicRep (Sing :: nat -> *)) of
Monomorphic sn ->
case sn %:< (sing :: Sing n) of
STrue -> sNatToOrd' (sing :: Sing n) sn
SFalse -> error "Bound over!"
unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)
=> proxy nat -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n
unsafeFromInt' _ n =
case promote (n :: MonomorphicRep (Sing :: nat -> *)) of
Monomorphic sn ->
case sn %:< (sing :: Sing n) of
STrue -> sNatToOrd' (sing :: Sing n) sn
SFalse -> error "Bound over!"
sNatToOrd' :: (PeanoOrder nat, (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n
sNatToOrd' _ m = OLt m
sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n
sNatToOrd = sNatToOrd' sing
ordToSing :: (PeanoOrder nat) => Ordinal (n :: nat) -> SomeSing nat
ordToSing (OLt n) = SomeSing n
ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *))
=> Ordinal (n :: nat)
-> int
ordToInt (OLt n) = demote $ Monomorphic n
inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m
inclusion' _ = unsafeCoerce
inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m
inclusion on = unsafeCoerce on
(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m)
=> Ordinal n -> Ordinal m -> Ordinal (n :+ m)
OLt k @+ OLt l =
let (n, m) = (n :: Sing n, m :: Sing m)
in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %:+ l
absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a
absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness
vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a
vacuousOrd = fmap absurdOrd
mkOrdinalQQ :: TypeQ -> QuasiQuoter
mkOrdinalQQ t =
QuasiQuoter { quoteExp = \s -> [| OLt $(quoteExp (mkSNatQQ t) s) |]
, quoteType = error "No type quoter for Ordinals"
, quotePat = \s -> [p| OLt ((%~ $(quoteExp (mkSNatQQ t) s)) -> Proved Refl) |]
, quoteDec = error "No declaration quoter for Ordinals"
}
odPN, odLit :: QuasiQuoter
odPN = mkOrdinalQQ [t| PN.Nat |]
odLit = mkOrdinalQQ [t| TL.Nat |]