diff options
Diffstat (limited to 'libraries')
| -rw-r--r-- | libraries/base/Data/Type/Ord.hs | 125 | ||||
| -rw-r--r-- | libraries/base/GHC/TypeLits.hs | 48 | ||||
| -rw-r--r-- | libraries/base/GHC/TypeLits/Internal.hs | 33 | ||||
| -rw-r--r-- | libraries/base/GHC/TypeNats.hs | 35 | ||||
| -rw-r--r-- | libraries/base/GHC/TypeNats/Internal.hs | 26 | ||||
| -rw-r--r-- | libraries/base/base.cabal | 3 |
6 files changed, 239 insertions, 31 deletions
diff --git a/libraries/base/Data/Type/Ord.hs b/libraries/base/Data/Type/Ord.hs new file mode 100644 index 0000000000..d882a82a61 --- /dev/null +++ b/libraries/base/Data/Type/Ord.hs @@ -0,0 +1,125 @@ +{-# 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 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Maintainer : libraries@haskell.org +-- Stability : experimental +-- Portability : not portable +-- +-- Basic operations on type-level Orderings. +-- +-- @since 4.16.0.0 +----------------------------------------------------------------------------- + +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 + +-- | 'Compare' branches on the kind of its arguments to either compare by +-- 'Symbol' or 'Nat'. +-- @since 4.16.0.0 +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 + +-- | Ordering data type for type literals that provides proof of their ordering. +-- @since 4.16.0.0 +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 <=?, <=, >=?, >=, <?, <, >?, > + +-- | Comparison (<=) of comparable types, as a constraint. +-- @since 4.16.0.0 +type x <= y = (x <=? y) ~ 'True + +-- | Comparison (>=) of comparable types, as a constraint. +-- @since 4.16.0.0 +type x >= y = (x >=? y) ~ 'True + +-- | Comparison (<) of comparable types, as a constraint. +-- @since 4.16.0.0 +type x < y = (x >? y) ~ 'True + +-- | Comparison (>) of comparable types, as a constraint. +-- @since 4.16.0.0 +type x > y = (x >? y) ~ 'True + + +-- | Comparison (<=) of comparable types, as a function. +-- @since 4.16.0.0 +type (<=?) :: k -> k -> Bool +type m <=? n = OrdCond (Compare m n) 'True 'True 'False + +-- | Comparison (>=) of comparable types, as a function. +-- @since 4.16.0.0 +type (>=?) :: k -> k -> Bool +type m >=? n = OrdCond (Compare m n) 'False 'True 'True + +-- | Comparison (<) of comparable types, as a function. +-- @since 4.16.0.0 +type (<?) :: k -> k -> Bool +type m <? n = OrdCond (Compare m n) 'True 'False 'False + +-- | Comparison (>) of comparable types, as a function. +-- @since 4.16.0.0 +type (>?) :: k -> k -> Bool +type m >? n = OrdCond (Compare m n) 'False 'False 'True + + +-- | Maximum between two comparable types. +-- @since 4.16.0.0 +type Max :: k -> k -> k +type Max m n = OrdCond (Compare m n) n n m + +-- | Minimum between two comparable types. +-- @since 4.16.0.0 +type Min :: k -> k -> k +type Min m n = OrdCond (Compare m n) m m n + + +-- | A case statement on `Ordering`. +-- `Ordering c l e g` is `l` when `c ~ LT`, `e` when `c ~ EQ`, and `g` when +-- `c ~ GT`. +-- @since 4.16.0.0 +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 diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs index 206fd385ea..b0daf341c8 100644 --- a/libraries/base/GHC/TypeLits.hs +++ b/libraries/base/GHC/TypeLits.hs @@ -31,7 +31,7 @@ working with type-level data will be defined in a separate library. module GHC.TypeLits ( -- * Kinds - Natural, Nat, Symbol -- Symbol is declared in GHC.Types in package ghc-prim + N.Natural, N.Nat, Symbol -- Symbol is declared in GHC.Types in package ghc-prim -- * Linking type and value level , N.KnownNat, natVal, natVal' @@ -40,6 +40,8 @@ module GHC.TypeLits , N.SomeNat(..), SomeSymbol(..), SomeChar(..) , someNatVal, someSymbolVal, someCharVal , N.sameNat, sameSymbol, sameChar + , OrderingI(..) + , N.cmpNat, cmpSymbol, cmpChar -- * Functions on type literals @@ -65,9 +67,10 @@ import GHC.Prim(magicDict, Proxy#) import Data.Maybe(Maybe(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality((:~:)(Refl)) +import Data.Type.Ord(OrderingI(..)) import Unsafe.Coerce(unsafeCoerce) -import GHC.TypeNats (Natural, Nat, KnownNat) +import GHC.TypeLits.Internal(CmpSymbol, CmpChar) import qualified GHC.TypeNats as N -------------------------------------------------------------------------------- @@ -80,7 +83,7 @@ class KnownSymbol (n :: Symbol) where symbolSing :: SSymbol n -- | @since 4.7.0.0 -natVal :: forall n proxy. KnownNat n => proxy n -> Integer +natVal :: forall n proxy. N.KnownNat n => proxy n -> Integer natVal p = toInteger (N.natVal p) -- | @since 4.7.0.0 @@ -89,7 +92,7 @@ symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x -- | @since 4.8.0.0 -natVal' :: forall n. KnownNat n => Proxy# n -> Integer +natVal' :: forall n. N.KnownNat n => Proxy# n -> Integer natVal' p = toInteger (N.natVal' p) -- | @since 4.8.0.0 @@ -171,11 +174,6 @@ instance Read SomeChar where -------------------------------------------------------------------------------- --- | Comparison of type-level symbols, as a function. --- --- @since 4.7.0.0 -type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering - -- | Concatenation of type-level symbols. -- -- @since 4.10.0.0 @@ -231,11 +229,6 @@ type family TypeError (a :: ErrorMessage) :: b where -- Char-related type families --- | Comparison of type-level characters. --- --- @since 4.16.0.0 -type family CmpChar (a :: Char) (b :: Char) :: Ordering - -- | Extending a type-level symbol with a type-level character -- -- @since 4.16.0.0 @@ -270,6 +263,33 @@ sameChar x y | charVal x == charVal y = Just (unsafeCoerce Refl) | otherwise = Nothing +-- | Like 'sameSymbol', but if the symbols aren't equal, this additionally +-- provides proof of LT or GT. +-- @since 4.16.0.0 +cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b) + => proxy1 a -> proxy2 b -> OrderingI a b +cmpSymbol x y = case compare (symbolVal x) (symbolVal y) of + EQ -> case unsafeCoerce (Refl, Refl) :: (CmpSymbol a b :~: 'EQ, a :~: b) of + (Refl, Refl) -> EQI + LT -> case unsafeCoerce Refl :: (CmpSymbol a b :~: 'LT) of + Refl -> LTI + GT -> case unsafeCoerce Refl :: (CmpSymbol a b :~: 'GT) of + Refl -> GTI + +-- | Like 'sameChar', but if the Chars aren't equal, this additionally +-- provides proof of LT or GT. +-- @since 4.16.0.0 +cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b) + => proxy1 a -> proxy2 b -> OrderingI a b +cmpChar x y = case compare (charVal x) (charVal y) of + EQ -> case unsafeCoerce (Refl, Refl) :: (CmpChar a b :~: 'EQ, a :~: b) of + (Refl, Refl) -> EQI + LT -> case unsafeCoerce Refl :: (CmpChar a b :~: 'LT) of + Refl -> LTI + GT -> case unsafeCoerce Refl :: (CmpChar a b :~: 'GT) of + Refl -> GTI + + -------------------------------------------------------------------------------- -- PRIVATE: diff --git a/libraries/base/GHC/TypeLits/Internal.hs b/libraries/base/GHC/TypeLits/Internal.hs new file mode 100644 index 0000000000..052394065e --- /dev/null +++ b/libraries/base/GHC/TypeLits/Internal.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK not-home #-} + +{-| +This module exports the Type Literal kinds as well as the comparison type +families for those kinds. It is needed to prevent module cycles while still +allowing these identifiers to be improted in 'Data.Type.Ord'. + +@since 4.16.0.0 +-} + +module GHC.TypeLits.Internal + ( Symbol + , CmpSymbol, CmpChar + ) where + +import GHC.Base(Ordering) +import GHC.Types(Symbol, Char) + +-- | Comparison of type-level symbols, as a function. +-- +-- @since 4.7.0.0 +type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering + +-- Char-related type families + +-- | Comparison of type-level characters. +-- +-- @since 4.16.0.0 +type family CmpChar (a :: Char) (b :: Char) :: Ordering diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs index a2dabb1fca..f9733d55a3 100644 --- a/libraries/base/GHC/TypeNats.hs +++ b/libraries/base/GHC/TypeNats.hs @@ -33,6 +33,7 @@ module GHC.TypeNats -- * Functions on type literals , type (<=), type (<=?), type (+), type (*), type (^), type (-) , CmpNat + , cmpNat , Div, Mod, Log2 ) where @@ -46,8 +47,10 @@ import GHC.Prim(magicDict, Proxy#) import Data.Maybe(Maybe(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality((:~:)(Refl)) +import Data.Type.Ord(OrderingI(..), type (<=), type (<=?)) import Unsafe.Coerce(unsafeCoerce) +import GHC.TypeNats.Internal(CmpNat) -- | A type synonym for 'Natural'. -- @@ -163,27 +166,10 @@ instance Read SomeNat where -------------------------------------------------------------------------------- -infix 4 <=?, <= infixl 6 +, - infixl 7 *, `Div`, `Mod` infixr 8 ^ --- | Comparison of type-level naturals, as a constraint. --- --- @since 4.7.0.0 -type x <= y = (x <=? y) ~ 'True - --- | Comparison of type-level naturals, as a function. --- --- @since 4.7.0.0 -type family CmpNat (m :: Nat) (n :: Nat) :: Ordering - -{- | Comparison of type-level naturals, as a function. -NOTE: The functionality for this function should be subsumed -by 'CmpNat', so this might go away in the future. -Please let us know, if you encounter discrepancies between the two. -} -type family (m :: Nat) <=? (n :: Nat) :: Bool - -- | Addition of type-level naturals. -- -- @since 4.7.0.0 @@ -234,6 +220,21 @@ sameNat x y | natVal x == natVal y = Just (unsafeCoerce Refl) | otherwise = Nothing +-- | Like 'sameNat', but if the numbers aren't equal, this additionally +-- provides proof of LT or GT. +-- @since 4.16.0.0 +cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) + => proxy1 a -> proxy2 b -> OrderingI a b +cmpNat x y = case compare (natVal x) (natVal y) of + EQ -> case unsafeCoerce (Refl, Refl) :: (CmpNat a b :~: 'EQ, a :~: b) of + (Refl, Refl) -> EQI + LT -> case unsafeCoerce Refl :: (CmpNat a b :~: 'LT) of + Refl -> LTI + GT -> case unsafeCoerce Refl :: (CmpNat a b :~: 'GT) of + Refl -> GTI + + + -------------------------------------------------------------------------------- -- PRIVATE: diff --git a/libraries/base/GHC/TypeNats/Internal.hs b/libraries/base/GHC/TypeNats/Internal.hs new file mode 100644 index 0000000000..7ae787310f --- /dev/null +++ b/libraries/base/GHC/TypeNats/Internal.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_HADDOCK not-home #-} + +{-| +This module exports the Type Nat kind as well as the comparison type +family for that kinds. It is needed to prevent module cycles while still +allowing these identifiers to be improted in 'Data.Type.Ord'. + +@since 4.16.0.0 +-} + +module GHC.TypeNats.Internal + ( Natural + , CmpNat + ) where + +import GHC.Base(Ordering) +import GHC.Num.Natural(Natural) + +-- | Comparison of type-level naturals, as a function. +-- +-- @since 4.7.0.0 +type family CmpNat (m :: Natural) (n :: Natural) :: Ordering diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal index ac5cb24814..530e0503c0 100644 --- a/libraries/base/base.cabal +++ b/libraries/base/base.cabal @@ -159,6 +159,7 @@ Library Data.Type.Bool Data.Type.Coercion Data.Type.Equality + Data.Type.Ord Data.Typeable Data.Unique Data.Version @@ -277,7 +278,9 @@ Library GHC.Storable GHC.TopHandler GHC.TypeLits + GHC.TypeLits.Internal GHC.TypeNats + GHC.TypeNats.Internal GHC.Unicode GHC.Weak GHC.Word |