{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PatternSynonyms, PolyKinds #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Type.Ordinal
(
Ordinal (..), pattern OZ, pattern OS, HasOrdinal,
mkOrdinalQQ, odPN, odLit,
sNatToOrd', sNatToOrd,
ordToNatural, unsafeNaturalToOrd', unsafeNaturalToOrd,
reallyUnsafeNaturalToOrd,
naturalToOrd, naturalToOrd',
ordToSing, inclusion, inclusion',
(@+), enumOrdinal,
absurdOrd, vacuousOrd,
ordToInt, unsafeFromInt, unsafeFromInt'
) where
import Data.Type.Natural.Singleton.Compat
import Data.List (genericDrop, genericTake)
import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Data.Singletons.Decide
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Enum
import Data.Type.Equality
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 qualified GHC.TypeLits as TL
import Language.Haskell.TH hiding (Type)
import Language.Haskell.TH.Quote
import Numeric.Natural
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, SingKind nat) => HasOrdinal nat
instance (PeanoOrder nat, SingKind 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 (toNatural (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 sn = withSingI sn $ map (reallyUnsafeNaturalToOrd Proxy) [0..toNatural sn - 1]
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)
{-# INLINE succOrd #-}
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)
{-# INLINE minBound #-}
maxBound =
withWitness (lneqSucc (sing :: Sing m)) $
sNatToOrd (sing :: Sing m)
{-# INLINE maxBound #-}
{-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-}
unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))
=> Int -> Ordinal n
unsafeFromInt = unsafeNaturalToOrd . fromIntegral
unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))
=> Natural -> Ordinal n
unsafeNaturalToOrd k =
fromMaybe (error "unsafeNaturalToOrd Out of bound") $
naturalToOrd k
{-# DEPRECATED unsafeFromInt' "Use unsafeNaturalToOrd' instead" #-}
unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)
=> proxy nat -> Int -> Ordinal n
unsafeFromInt' p = unsafeNaturalToOrd' p . fromIntegral
unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)
=> proxy nat -> Natural -> Ordinal n
unsafeNaturalToOrd' _ n =
case fromNatural n of
SomeSing sn ->
case sn %< (sing :: Sing n) of
STrue -> sNatToOrd' (sing :: Sing n) sn
SFalse -> error "Bound over!"
{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-}
reallyUnsafeNaturalToOrd :: forall pxy nat (n :: nat). (HasOrdinal nat, SingI n)
=> pxy nat -> Natural -> Ordinal n
reallyUnsafeNaturalToOrd _ k =
case fromNatural k of
SomeSing (sk :: Sing (k :: nat)) ->
withRefl (unsafeCoerce (Refl :: () :~: ()) :: (k < n) :~: 'True) $
OLt sk
sNatToOrd' :: (PeanoOrder nat, (m < n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n
sNatToOrd' _ = OLt
{-# INLINE sNatToOrd' #-}
sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m < n) ~ 'True) => Sing m -> Ordinal n
sNatToOrd = sNatToOrd' sing
naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n)
=> Natural -> Maybe (Ordinal (n :: nat))
naturalToOrd = naturalToOrd' (sing :: Sing n)
naturalToOrd' :: HasOrdinal nat
=> Sing (n :: nat) -> Natural -> Maybe (Ordinal n)
naturalToOrd' sn k =
case fromNatural k of
SomeSing sk ->
case sk %< sn of
STrue -> Just (OLt sk)
_ -> Nothing
ordToSing :: (PeanoOrder nat) => Ordinal (n :: nat) -> SomeSing nat
ordToSing (OLt n) = SomeSing n
{-# INLINE ordToSing #-}
{-# DEPRECATED ordToInt "Use ordToNatural instead." #-}
ordToInt :: (HasOrdinal nat)
=> Ordinal (n :: nat)
-> Int
ordToInt = fromIntegral . ordToNatural
{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Int #-}
{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Int #-}
ordToNatural :: HasOrdinal nat
=> Ordinal (n :: nat)
-> Natural
ordToNatural (OLt n) = toNatural n
{-# SPECIALISE ordToNatural :: Ordinal (n :: PN.Nat) -> Natural #-}
{-# SPECIALISE ordToNatural :: Ordinal (n :: TL.Nat) -> Natural #-}
inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m
inclusion' _ = unsafeCoerce
{-# INLINE inclusion' #-}
inclusion :: ((n <= m) ~ 'True) => Ordinal n -> Ordinal m
inclusion = unsafeCoerce
{-# INLINE inclusion #-}
(@+) :: 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 |]