Haskus.Utils.Types

Common type functions

Documentation

data Nat

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

data Symbol

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

Instances

SingKind Symbol

Since: base-4.9.0.0

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol :: Type

Methods

fromSing :: Sing a -> DemoteRep Symbol

KnownSymbol a => SingI (a :: Symbol)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

sing :: Sing a

data Sing (s :: Symbol)

Defined in GHC.Generics

data Sing (s :: Symbol) where

• SSym :: forall (s :: Symbol). KnownSymbol s => Sing s

type DemoteRep Symbol

Defined in GHC.Generics

type DemoteRep Symbol = String

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

Get a Nat value

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

Get a Nat value

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

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: base-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: base-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: base-4.7.0.0

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

Comparison of type-level symbols, as a function.

Since: base-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) = (x <=? y) ~ True infix 4

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

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

Addition of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Like: If cond t (TypeError msg)

The difference is that the TypeError doesn't appear in the RHS of the type which leads 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 ...

If-then-else

Equations

If True t e = t

If False t e = e

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

Modulo

Equations

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

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

Type equality to Nat

Equations

Same a a = 1

Same a b = 0

data Proxy (t :: k) :: forall k. k -> Type

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> Type)

Defined in GHC.Generics

Associated Types

type Rep1 Proxy :: k -> Type

Methods

from1 :: Proxy a -> Rep1 Proxy a

to1 :: Rep1 Proxy a -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

fail :: String -> Proxy a

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

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 :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Foldable

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 :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Traversable

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)

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s

pred :: Proxy s -> Proxy s

toEnum :: Int -> Proxy s

fromEnum :: Proxy s -> Int

enumFrom :: Proxy s -> [Proxy s]

enumFromThen :: Proxy s -> Proxy s -> [Proxy s]

enumFromTo :: Proxy s -> Proxy s -> [Proxy s]

enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s]

Eq (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Ord (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering

(<) :: Proxy s -> Proxy s -> Bool

(<=) :: Proxy s -> Proxy s -> Bool

(>) :: Proxy s -> Proxy s -> Bool

(>=) :: Proxy s -> Proxy s -> Bool

max :: Proxy s -> Proxy s -> Proxy s

min :: Proxy s -> Proxy s -> Proxy s

Read (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

readsPrec :: Int -> ReadS (Proxy t)

readList :: ReadS [Proxy t]

readPrec :: ReadPrec (Proxy t)

readListPrec :: ReadPrec [Proxy t]

Show (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Ix (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

Generic (Proxy t)

Defined in GHC.Generics

Associated Types

type Rep (Proxy t) :: Type -> Type

Methods

from :: Proxy t -> Rep (Proxy t) x

to :: Rep (Proxy t) x -> Proxy t

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep1 (Proxy :: k -> Type) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> Type))

type Rep (Proxy t)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: Type -> Type))

type family TypeError (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: base-4.9.0.0

data ErrorMessage where

A description of a custom type error.

Constructors

Text :: forall. Symbol -> ErrorMessage

Show the text as is.

ShowType :: forall t. t -> ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 5

Stack two pieces of error message on top of each other.