Safe Haskell	Safe
Language	Haskell2010

Haskus.Utils.Types

Description

Common type functions

Synopsis

Documentation

data Nat :: * #

(Kind) This is the kind of type-level natural numbers.

Instances

type (==) Nat a b
type (==) Nat a b = EqNat a b

data Symbol :: * #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

SingKind Symbol	Since: 4.9.0.0
Associated Types type DemoteRep Symbol :: * Methods fromSing :: Sing Symbol a -> DemoteRep Symbol
KnownSymbol a => SingI Symbol a	Since: 4.9.0.0
Methods sing :: Sing a a
data Sing Symbol
data Sing Symbol where SSym :: Sing Symbol s
type DemoteRep Symbol
type DemoteRep Symbol = String
type (==) Symbol a b
type (==) Symbol a b = EqSymbol a b

natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a Source #

Get a Nat value

natValue' :: forall (n :: Nat). KnownNat n => Word Source #

Get a Nat value

symbolValue :: forall (s :: Symbol). KnownSymbol s => String Source #

Get a Symbol value

class KnownNat (n :: Nat) #

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: 4.7.0.0

Minimal complete definition

natSing

class KnownSymbol (n :: Symbol) #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #

Comparison of type-level symbols, as a function.

Since: 4.7.0.0

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #

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 (<=) (x :: Nat) (y :: Nat) = (~) Bool ((<=?) x y) True infix 4 #

Comparison of type-level naturals, as a constraint.

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

Addition of type-level naturals.

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #

Subtraction of type-level naturals.

Since: 4.7.0.0

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

Multiplication of type-level naturals.

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) where ... Source #

Like: If cond t (TypeError msg)

The difference is that the TypeError doesn't appear in the RHS of the type which lead to better error messages (see GHC #14771).

For instance: type family F n where F n = If (n <=? 8) Int8 (TypeError (Text ERROR))

type family G n where G n = Assert (n <=? 8) Int8 (Text ERROR)

If GHC cannot solve `F n ~ Word`, it shows: ERROR If GHC cannot solve `G n ~ Word`, it shows: can't match .. with Word

Equations

Assert True val msg = val
Assert False val msg = TypeError msg

type family If (c :: Bool) (t :: k) (e :: k) where ... Source #

If-then-else

Equations

If True t e = t
If False t e = e

type family Modulo (a :: Nat) (b :: Nat) where ... Source #

Modulo

Equations

Modulo a b = Modulo' (a <=? b) a b

type family Same a b :: Nat where ... Source #

Type equality to Nat

Equations

Same a a = 1
Same a b = 0

data Proxy k (t :: k) :: forall k. k -> * #

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Generic1 k (Proxy k)
Associated Types type Rep1 (Proxy k) (f :: Proxy k -> ) :: k -> # Methods from1 :: f a -> Rep1 (Proxy k) f a # to1 :: Rep1 (Proxy k) f a -> f a #
Monad (Proxy *)	Since: 4.7.0.0
Methods (>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b # (>>) :: Proxy * a -> Proxy * b -> Proxy * b # return :: a -> Proxy * a # fail :: String -> Proxy * a #
Functor (Proxy *)	Since: 4.7.0.0
Methods fmap :: (a -> b) -> Proxy * a -> Proxy * b # (<$) :: a -> Proxy * b -> Proxy * a #
Applicative (Proxy *)	Since: 4.7.0.0
Methods pure :: a -> Proxy * a # (<>) :: Proxy (a -> b) -> Proxy * a -> Proxy * b # liftA2 :: (a -> b -> c) -> Proxy * a -> Proxy * b -> Proxy * c # (>) :: Proxy a -> Proxy * b -> Proxy * b # (<) :: Proxy a -> Proxy * b -> Proxy * a #
Foldable (Proxy *)	Since: 4.7.0.0
Methods fold :: Monoid m => Proxy * m -> m # foldMap :: Monoid m => (a -> m) -> Proxy * a -> m # foldr :: (a -> b -> b) -> b -> Proxy * a -> b # foldr' :: (a -> b -> b) -> b -> Proxy * a -> b # foldl :: (b -> a -> b) -> b -> Proxy * a -> b # foldl' :: (b -> a -> b) -> b -> Proxy * a -> b # foldr1 :: (a -> a -> a) -> Proxy * a -> a # foldl1 :: (a -> a -> a) -> Proxy * a -> a # toList :: Proxy * a -> [a] # null :: Proxy * a -> Bool # length :: Proxy * a -> Int # elem :: Eq a => a -> Proxy * a -> Bool # maximum :: Ord a => Proxy * a -> a # minimum :: Ord a => Proxy * a -> a # sum :: Num a => Proxy * a -> a # product :: Num a => Proxy * a -> a #
Traversable (Proxy *)	Since: 4.7.0.0
Methods traverse :: Applicative f => (a -> f b) -> Proxy * a -> f (Proxy * b) # sequenceA :: Applicative f => Proxy * (f a) -> f (Proxy * a) # mapM :: Monad m => (a -> m b) -> Proxy * a -> m (Proxy * b) # sequence :: Monad m => Proxy * (m a) -> m (Proxy * a) #
Eq1 (Proxy *)	Since: 4.9.0.0
Methods liftEq :: (a -> b -> Bool) -> Proxy * a -> Proxy * b -> Bool #
Ord1 (Proxy *)	Since: 4.9.0.0
Methods liftCompare :: (a -> b -> Ordering) -> Proxy * a -> Proxy * b -> Ordering #
Read1 (Proxy *)	Since: 4.9.0.0
Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy * a) # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy * a] # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Proxy * a) # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Proxy * a] #
Show1 (Proxy *)	Since: 4.9.0.0
Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy * a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy * a] -> ShowS #
Alternative (Proxy *)	Since: 4.9.0.0
Methods empty :: Proxy * a # (<\|>) :: Proxy * a -> Proxy * a -> Proxy * a # some :: Proxy * a -> Proxy * [a] # many :: Proxy * a -> Proxy * [a] #
MonadPlus (Proxy *)	Since: 4.9.0.0
Methods mzero :: Proxy * a # mplus :: Proxy * a -> Proxy * a -> Proxy * a #
Hashable1 (Proxy *)
Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Proxy * a -> Int #
Bounded (Proxy k t)
Methods minBound :: Proxy k t # maxBound :: Proxy k t #
Enum (Proxy k s)	Since: 4.7.0.0
Methods succ :: Proxy k s -> Proxy k s # pred :: Proxy k s -> Proxy k s # toEnum :: Int -> Proxy k s # fromEnum :: Proxy k s -> Int # enumFrom :: Proxy k s -> [Proxy k s] # enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s] # enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s] # enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s] #
Eq (Proxy k s)	Since: 4.7.0.0
Methods (==) :: Proxy k s -> Proxy k s -> Bool # (/=) :: Proxy k s -> Proxy k s -> Bool #
Ord (Proxy k s)	Since: 4.7.0.0
Methods compare :: Proxy k s -> Proxy k s -> Ordering # (<) :: Proxy k s -> Proxy k s -> Bool # (<=) :: Proxy k s -> Proxy k s -> Bool # (>) :: Proxy k s -> Proxy k s -> Bool # (>=) :: Proxy k s -> Proxy k s -> Bool # max :: Proxy k s -> Proxy k s -> Proxy k s # min :: Proxy k s -> Proxy k s -> Proxy k s #
Read (Proxy k s)	Since: 4.7.0.0
Methods readsPrec :: Int -> ReadS (Proxy k s) # readList :: ReadS [Proxy k s] # readPrec :: ReadPrec (Proxy k s) # readListPrec :: ReadPrec [Proxy k s] #
Show (Proxy k s)	Since: 4.7.0.0
Methods showsPrec :: Int -> Proxy k s -> ShowS # show :: Proxy k s -> String # showList :: [Proxy k s] -> ShowS #
Ix (Proxy k s)	Since: 4.7.0.0
Methods range :: (Proxy k s, Proxy k s) -> [Proxy k s] # index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int # unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool # rangeSize :: (Proxy k s, Proxy k s) -> Int # unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int
Generic (Proxy k t)
Associated Types type Rep (Proxy k t) :: * -> * # Methods from :: Proxy k t -> Rep (Proxy k t) x # to :: Rep (Proxy k t) x -> Proxy k t #
Semigroup (Proxy k s)	Since: 4.9.0.0
Methods (<>) :: Proxy k s -> Proxy k s -> Proxy k s # sconcat :: NonEmpty (Proxy k s) -> Proxy k s # stimes :: Integral b => b -> Proxy k s -> Proxy k s #
Monoid (Proxy k s)	Since: 4.7.0.0
Methods mempty :: Proxy k s # mappend :: Proxy k s -> Proxy k s -> Proxy k s # mconcat :: [Proxy k s] -> Proxy k s #
Hashable (Proxy k a)
Methods hashWithSalt :: Int -> Proxy k a -> Int # hash :: Proxy k a -> Int #
type Rep1 k (Proxy k)
type Rep1 k (Proxy k) = D1 k (MetaData "Proxy" "Data.Proxy" "base" False) (C1 k (MetaCons "Proxy" PrefixI False) (U1 k))
type Rep (Proxy k t)
type Rep (Proxy k t) = D1 * (MetaData "Proxy" "Data.Proxy" "base" False) (C1 * (MetaCons "Proxy" PrefixI False) (U1 *))

type family TypeError b (a :: ErrorMessage) :: b where ... #

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: 4.9.0.0

data ErrorMessage :: * where #

A description of a custom type error.

Constructors

Text :: ErrorMessage	Show the text as is.
ShowType :: ErrorMessage	Pretty print the type. `ShowType :: k -> ErrorMessage`
(:<>:) :: ErrorMessage infixl 6	Put two pieces of error message next to each other.
(:$$:) :: ErrorMessage infixl 5	Stack two pieces of error message on top of each other.