kind-apply-0.3.2.0: Utilities to work with lists of types

Safe HaskellSafe
LanguageHaskell2010

Data.PolyKinded

Contents

Synopsis

Lists of types and application

data LoT k where Source #

LoT k represents a list of types which can be applied to a data type of kind k.

Constructors

LoT0 :: LoT *

Empty list of types.

(:&&:) :: k -> LoT ks -> LoT (k -> ks) infixr 5

Cons a type with a list of types.

type family (f :: k) :@@: (tys :: LoT k) :: * where ... Source #

Apply a list of types to a type constructor.

>>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)
Either Int Bool :: *

Equations

f :@@: _ = f 
f :@@: as = f (HeadLoT as) :@@: TailLoT as 

type LoT1 a = a :&&: LoT0 Source #

type LoT2 a b = a :&&: (b :&&: LoT0) Source #

type family HeadLoT (tys :: LoT (k -> k')) :: k where ... Source #

Head of a non-empty list of types.

>>> :kind! HeadLoT (Int :&&: LoT0)
Int :: *

Equations

HeadLoT (a :&&: _) = a 

type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where ... Source #

Tail of a non-empty list of types.

>>> :kind! TailLoT (Int :&&: Bool :&&: LoT0)
Bool :&&: LoT0 :: LoT (Type -> Type)

Equations

TailLoT (_ :&&: as) = as 

type family SpineLoT (ts :: LoT k) :: LoT k where ... Source #

Construct the spine of a list of types whose length is known.

It can be useful to introduce unification variables for lists of types which will be fully instantiated during constraint resolution. A constraint p ~ SpineLoT p will thus instantiate the spine of p.

On concrete lists, this is the identity function.

Equations

SpineLoT (ts :: LoT (k -> k')) = HeadLoT ts :&&: SpineLoT (TailLoT ts) 
SpineLoT (ts :: LoT *) = LoT0 

Singleton for list of types

data SLoT (l :: LoT k) where Source #

Constructors

SLoT0 :: SLoT LoT0 
SLoTA :: Proxy t -> SLoT ts -> SLoT (t :&&: ts) 

class SForLoT (l :: LoT k) where Source #

Methods

slot :: SLoT l Source #

Instances
l ~ LoT0 => SForLoT (l :: LoT Type) Source # 
Instance details

Defined in Data.PolyKinded

Methods

slot :: SLoT l Source #

(l ~ (t :&&: ts), SForLoT ts) => SForLoT (l :: LoT (k -> k')) Source # 
Instance details

Defined in Data.PolyKinded

Methods

slot :: SLoT l Source #

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) 
Instance details

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

Instance details

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

Instance details

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

Instance details

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

Instance details

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

Instance details

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

Instance details

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

Instance details

Defined in Data.Proxy

Methods

mzero :: Proxy a #

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

Bounded (Proxy t)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

minBound :: Proxy t #

maxBound :: Proxy t #

Enum (Proxy s)

Since: base-4.7.0.0

Instance details

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

Instance details

Defined in Data.Proxy

Methods

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

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

Ord (Proxy s)

Since: base-4.7.0.0

Instance details

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

Instance details

Defined in Data.Proxy

Show (Proxy s)

Since: base-4.7.0.0

Instance details

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

Instance details

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) 
Instance details

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

Instance details

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

Instance details

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

Instance details

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

Instance details

Defined in GHC.Generics

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

Splitting types

type SplitF (t :: d) (f :: k) = SplitF' t f LoT0 Source #

Split a type t until the constructor f is found.

>>> :kind! SplitF (Either Int Bool) Either
Int :&&: Bool :&&: LoT0 :: LoT (* -> * -> *)
>>> :kind! SplitF (Either Int Bool) (Either Int)
Bool :&&: LoT0 :: LoT (* -> *)

data Nat Source #

Simple natural numbers.

Constructors

Z 
S Nat 

data TyEnv where Source #

A type constructor and a list of types that can be applied to it.

Constructors

TyEnv :: forall k. k -> LoT k -> TyEnv 

type family SplitN (n :: Nat) t :: TyEnv where ... Source #

Split a type t until its list of types has length n.

>>> :kind! SplitN (Either Int Bool) (S (S Z))
TyEnv Either (Int :&&: Bool :&&: LoT0) :: TyEnv
>>> :kind! SplitF (Either Int Bool) (S Z)
TyEnv (Either Int) (Bool :&&: LoT0) :: TyEnv

Equations

SplitN n t = SplitN' n t LoT0