Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data family Sing :: k -> Type
- class SingI (a :: k) where
- class DecidableEquality k where
- decideEquality :: Sing (a :: k) -> Sing (b :: k) -> Maybe (a :~: b)
- data Nat
- knownNat :: Sing (n :: Nat) -> Int
- type family Length (xs :: [k]) :: Nat where ...
- type family Or (a :: Bool) (b :: Bool) where ...
- type family Equal (x :: k) (y :: k) where ...
- type family Elem (x :: k) (xs :: [k]) where ...
- type family Assert (b :: Bool) (err :: ErrorMessage) :: Constraint where ...
- data IsElem (x :: k) (xs :: [k]) where
- checkIsElem :: DecidableEquality k => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs)
- class Phantom (f :: k -> Type) where
- phantom :: forall a b. f a -> f b
- data Poly (f :: k -> Type) = Poly (forall (a :: k). f a)
- maybePoly :: Phantom f => Maybe (f a) -> Maybe (Poly f)
Singletons
data family Sing :: k -> Type Source #
Instances
Show (Sing c) Source # | |
data Sing (a :: Type) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel | |
data Sing (n :: Symbol) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel | |
data Sing (n :: Nat) Source # | |
data Sing (xs :: [k]) Source # | |
data Sing (c :: Constr Symbol) Source # | |
Defined in Debug.RecoverRTTI.Constr |
class SingI (a :: k) where Source #
Instances
SingI (a :: Type) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel | |
KnownSymbol n => SingI (n :: Symbol) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel | |
SingI 'Z Source # | |
SingI n => SingI ('S n :: Nat) Source # | |
KnownConstr c => SingI (c :: Constr Symbol) Source # | |
Defined in Debug.RecoverRTTI.Constr | |
SingI ('[] :: [k]) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel | |
(SingI x, SingI xs) => SingI (x ': xs :: [a]) Source # | |
Defined in Debug.RecoverRTTI.Util.TypeLevel |
class DecidableEquality k where Source #
Instances
Natural numbers
General purpose type level functions
type family Assert (b :: Bool) (err :: ErrorMessage) :: Constraint where ... Source #
Assert type-level predicate
We cannot define this in terms of a more general If
construct, because
ghc
's type-level language has an undefined reduction order and so we get
no short-circuiting.
Type-level membership check
checkIsElem :: DecidableEquality k => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs) Source #