Data.PolyKinded

Representation of types as constructor + list of types.

Lists of types and application

data LoT k where

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

Constructors

LoT0 :: LoT Type

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

Apply a list of types to a type constructor.

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

Equations

f :@@: _ = f

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

type LoT1 a = a ':&&: 'LoT0

List of types with a single element.

type LoT2 a b = a ':&&: (b ':&&: 'LoT0)

List of types with two elements.

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

Head of a non-empty list of types.

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

Equations

HeadLoT (a ':&&: _) = a

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

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 (tys :: LoT k) = (tys' :: LoT k) | tys' -> tys where ...

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 (a ':&&: as) = a ':&&: SpineLoT as

SpineLoT 'LoT0 = 'LoT0

Singleton for list of types

data SLoT (l :: LoT k) where

Constructors

SLoT0 :: SLoT 'LoT0

SLoTA :: Proxy t -> SLoT ts -> SLoT (t ':&&: ts)

class SForLoT (l :: LoT k) where

Methods

slot :: SLoT l

Instances

l ~ 'LoT0 => SForLoT (l :: LoT Type)

Defined in Data.PolyKinded

Methods

slot :: SLoT l

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

Defined in Data.PolyKinded

Methods

slot :: SLoT l

data Proxy (t :: k)

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 :: forall (a :: k0). Proxy a -> Rep1 Proxy a

to1 :: forall (a :: k0). Rep1 Proxy a -> 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

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]

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

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

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

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

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

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

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]

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

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

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

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

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

Splitting types

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

Split a type t until the constructor f is found.

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

data Nat

Simple natural numbers.

Constructors

Z

S Nat

data TyEnv where

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 ...

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