(original) (raw)

{-# 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