{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
{-# 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.TypeLits.Internal
import GHC.TypeNats.Internal
import Data.Bool
import Data.Char(Char)
import Data.Eq
import Data.Ord
type Compare :: k -> k -> Ordering
type family Compare a b
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 = (x <=? y) ~ 'True
type x >= y = (x >=? y) ~ 'True
type x < y = (x >? y) ~ 'True
type x > y = (x >? y) ~ 'True
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