Propellor.Types.Singletons

Simple implementation of singletons, portable back to ghc 7.6.3

Documentation

data family Sing x

The data family of singleton types.

Instances

((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (Property (MetaTypes [k] x)) (Property (MetaTypes [k] y))

((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (Property (MetaTypes [k] x)) (RevertableProperty (MetaTypes [k] y) (MetaTypes k y'))

((~) CheckCombine (CheckCombinable k x y) CanCombine, SingI [k] (Combine k x y)) => Combines (RevertableProperty (MetaTypes [k] x) (MetaTypes k x')) (Property (MetaTypes [k] y))

((~) CheckCombine (CheckCombinable k x y) CanCombine, (~) CheckCombine (CheckCombinable k1 x' y') CanCombine, SingI [k] (Combine k x y), SingI [k1] (Combine k1 x' y')) => Combines (RevertableProperty (MetaTypes [k] x) (MetaTypes [k] x')) (RevertableProperty (MetaTypes [k] y) (MetaTypes [k] y'))

data Sing Bool where

• TrueS :: Sing Bool True
• FalseS :: Sing Bool False

data Sing MetaType where

• OSDebianS :: Sing MetaType (Targeting OSDebian)
• OSBuntishS :: Sing MetaType (Targeting OSBuntish)
• OSFreeBSDS :: Sing MetaType (Targeting OSFreeBSD)
• WithInfoS :: Sing MetaType WithInfo

type (+) * (MetaTypes [k] a) (MetaTypes [k] b)

data Sing [k] where

• Nil :: Sing [k] ([] k)
• Cons :: Sing k x -> Sing [k] xs -> Sing [k] ((:) k x xs)

type CombinedType (Property (MetaTypes [k] x)) (Property (MetaTypes [k] y)) = Property (MetaTypes [k] (Combine k x y))

type CombinedType (Property (MetaTypes [k] x)) (RevertableProperty (MetaTypes [k] y) (MetaTypes k1 y')) = Property (MetaTypes [k] (Combine k x y))

type IncludesInfo (MetaTypes [MetaType] l)

type CombinedType (RevertableProperty (MetaTypes [k] x) (MetaTypes k1 x')) (Property (MetaTypes [k] y)) = Property (MetaTypes [k] (Combine k x y))

type CombinedType (RevertableProperty (MetaTypes [k] x) (MetaTypes [k1] x')) (RevertableProperty (MetaTypes [k] y) (MetaTypes [k1] y')) = RevertableProperty (MetaTypes [k] (Combine k x y)) (MetaTypes [k1] (Combine k1 x' y'))

class SingI t where

A class used to pass singleton values implicitly.

Methods

sing :: Sing t

Instances

SingI Bool False

SingI Bool True

SingI MetaType WithInfo

SingI MetaType (Targeting OSDebian)

SingI MetaType (Targeting OSBuntish)

SingI MetaType (Targeting OSFreeBSD)

SingI [k] ([] k)

(SingI k x, SingI [k] xs) => SingI [k] ((:) k x xs)

class (kparam ~ KProxy) => SingKind kparam where

Associated Types

type DemoteRep kparam :: *

Methods

fromSing :: Sing (a :: k) -> DemoteRep kparam

From singleton to value.

Instances

SingKind Bool (KProxy Bool)

SingKind MetaType (KProxy MetaType)

SingKind a (KProxy a) => SingKind [a] (KProxy [a])

data KProxy t :: * -> *

A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only

Constructors

KProxy