{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Ord (
Compare, OrderingI(..)
, type (<=), type (<=?)
, type (>=), type (>=?)
, type (>), type (>?)
, type (<), type (<?)
, Max, Min
, OrdCond
) where
import GHC.Show(Show(..))
import GHC.TypeError
import GHC.TypeLits.Internal
import GHC.TypeNats.Internal
import GHC.Types (type (~))
import Data.Bool
import Data.Char(Char)
import Data.Eq
import Data.Ord
type Compare :: k -> k -> Ordering
type family Compare (a :: k) (b :: k) :: Ordering
type instance Compare (a :: Natural) b = CmpNat a b
type instance Compare (a :: Symbol) b = CmpSymbol a b
type instance Compare (a :: Char) b = CmpChar a b
data OrderingI a b where
LTI :: Compare a b ~ 'LT => OrderingI a b
EQI :: Compare a a ~ 'EQ => OrderingI a a
GTI :: Compare a b ~ 'GT => OrderingI a b
deriving instance Show (OrderingI a b)
deriving instance Eq (OrderingI a b)
infix 4 <=?, <=, >=?, >=, <?, <, >?, >
type x <= y = Assert (x <=? y) (LeErrMsg x y)
type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
type x >= y = Assert (x >=? y) (GeErrMsg x y)
type GeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " >= " ':<>: 'ShowType y)
type x < y = Assert (x <? y) (LtErrMsg x y)
type LtErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " < " ':<>: 'ShowType y)
type x > y = Assert (x >? y) (GtErrMsg x y)
type GtErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " > " ':<>: 'ShowType y)
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
type (>=?) :: k -> k -> Bool
type m >=? n = OrdCond (Compare m n) 'False 'True 'True
type (<?) :: k -> k -> Bool
type m <? n = OrdCond (Compare m n) 'True 'False 'False
type (>?) :: k -> k -> Bool
type m >? n = OrdCond (Compare m n) 'False 'False 'True
type Max :: k -> k -> k
type Max m n = OrdCond (Compare m n) n n m
type Min :: k -> k -> k
type Min m n = OrdCond (Compare m n) m m n
type OrdCond :: Ordering -> k -> k -> k -> k
type family OrdCond o lt eq gt where
OrdCond 'LT lt eq gt = lt
OrdCond 'EQ lt eq gt = eq
OrdCond 'GT lt eq gt = gt