Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.PolyKinded

Contents

Lists of types and application
- Singleton for list of types
Splitting types

Description

Representation of types as constructor + list of types.

Synopsis

data LoT k where
- LoT0 :: LoT Type
- (:&&:) :: k -> LoT ks -> LoT (k -> ks)
type family (f :: k) :@@: (tys :: LoT k) :: Type where ...
type LoT1 a = a :&&: 'LoT0
type LoT2 a b = a :&&: (b :&&: 'LoT0)
type family HeadLoT (tys :: LoT (k -> k')) :: k where ...
type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where ...
type family SpineLoT (tys :: LoT k) = (tys' :: LoT k) | tys' -> tys where ...
data SLoT (l :: LoT k) where
- SLoT0 :: SLoT 'LoT0
- SLoTA :: Proxy t -> SLoT ts -> SLoT (t :&&: ts)
class SForLoT (l :: LoT k) where
- slot :: SLoT l
data Proxy (t :: k) = Proxy
type SplitF (t :: d) (f :: k) = SplitF' t f 'LoT0
data Nat
- = Z
- | S Nat
data TyEnv where
- TyEnv :: forall k. k -> LoT k -> TyEnv
type family SplitN (n :: Nat) t :: TyEnv where ...

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

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 Source #

List of types with a single element.

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

List of types with two elements.

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

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 ... 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 (tys :: LoT k) = (tys' :: LoT k) | tys' -> tys 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 (a :&&: as) = a :&&: SpineLoT as
SpineLoT 'LoT0 = '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

Instances details

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

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

Instances details

Generic1 (Proxy :: k -> Type)
Instance details 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 LiftedRep -> 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 # 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] #
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 #
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 #
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 #
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 #
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 #
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 #
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] #
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 #
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 #
Read (Proxy t)	Since: base-4.7.0.0
Instance details 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
Instance details 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
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 #
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 (Type -> Type -> Type)
>>> :kind! SplitF (Either Int Bool) (Either Int)
Bool :&&: LoT0 :: LoT (Type -> Type)

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