Control.Static.Static

Documentation

type SKey (k :: Symbol) = Sing k

Standalone static key with no associated value.

Users typically don't need this, and should use SKeyed or SKeyedExt as appropriate.

data SKeyed k v

Internal value, typed-indexed by an associated static-key.

Generally, v is not expected to be serialisable or otherwise representable outside of the program. For cases where it is, you should define an instance of RepVal. That then enables you to use toSKeyedExt and other utility functions with this constraint.

Constructors

SKeyed !(SKey k) !v

Instances

Functor (SKeyed k)

Defined in Control.Static.Static

Methods

fmap :: (a -> b) -> SKeyed k a -> SKeyed k b

(<$) :: a -> SKeyed k b -> SKeyed k a

withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol). SKeyed a g -> r) -> r

Similar to withSomeSing for a SKeyedExt, extract the type from the String key and run a typed function on the typed value.

toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g

Convert an internal value to an external value, depending on the existence of an instance of RepVal to help perform the conversion.

toSKeyedEither :: Sing (k :: Symbol) -> Maybe (Either String v) -> Either SKeyedError v

skeyedCons :: (c @@ k) @@ v => SKeyed k v -> TCTab c kk vv -> TCTab c (k ': kk) (v ': vv)

Helper function for building TCTabs.

type RepExtSym3 c g ext = AndC2 c (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ext))

RepExt c g ext k v is a constraint comprising:

• RepVal g (ext v) k

• c k v

modulo singletons defunctionalisation on c and ext.

type family TyContIX r ext (v :: Type) where ...

A continuation from an internal and external value, to a result type r.

Equations

TyContIX r ext v = v -> (ext @@ v) -> r

type TyContIXSym3 (r6989586621679205952 :: Type) (ext6989586621679205953 :: (~>) Type Type) (v6989586621679205954 :: Type) = TyContIX r6989586621679205952 ext6989586621679205953 v6989586621679205954

data TyContIXSym2 (r6989586621679205952 :: Type) (ext6989586621679205953 :: (~>) Type Type) :: (~>) Type Type where

Constructors

TyContIXSym2KindInference :: forall r6989586621679205952 ext6989586621679205953 v6989586621679205954 arg. SameKind (Apply (TyContIXSym2 r6989586621679205952 ext6989586621679205953) arg) (TyContIXSym3 r6989586621679205952 ext6989586621679205953 arg) => TyContIXSym2 r6989586621679205952 ext6989586621679205953 v6989586621679205954

Instances

SuppressUnusedWarnings (TyContIXSym2 ext6989586621679205953 r6989586621679205952 :: TyFun Type Type -> Type)

Defined in Control.Static.Static

Methods

suppressUnusedWarnings :: ()

type Apply (TyContIXSym2 ext6989586621679205953 r6989586621679205952 :: TyFun Type Type -> Type) (v6989586621679205954 :: Type)

Defined in Control.Static.Static

type Apply (TyContIXSym2 ext6989586621679205953 r6989586621679205952 :: TyFun Type Type -> Type) (v6989586621679205954 :: Type) = TyContIX ext6989586621679205953 r6989586621679205952 v6989586621679205954

data TyContIXSym1 (r6989586621679205952 :: Type) :: (~>) ((~>) Type Type) ((~>) Type Type) where

Constructors

TyContIXSym1KindInference :: forall r6989586621679205952 ext6989586621679205953 arg. SameKind (Apply (TyContIXSym1 r6989586621679205952) arg) (TyContIXSym2 r6989586621679205952 arg) => TyContIXSym1 r6989586621679205952 ext6989586621679205953

Instances

SuppressUnusedWarnings (TyContIXSym1 r6989586621679205952 :: TyFun (Type ~> Type) (Type ~> Type) -> Type)

Defined in Control.Static.Static

Methods

suppressUnusedWarnings :: ()

type Apply (TyContIXSym1 r6989586621679205952 :: TyFun (Type ~> Type) (Type ~> Type) -> Type) (ext6989586621679205953 :: Type ~> Type)

Defined in Control.Static.Static

type Apply (TyContIXSym1 r6989586621679205952 :: TyFun (Type ~> Type) (Type ~> Type) -> Type) (ext6989586621679205953 :: Type ~> Type) = TyContIXSym2 r6989586621679205952 ext6989586621679205953

data TyContIXSym0 :: (~>) Type ((~>) ((~>) Type Type) ((~>) Type Type)) where

Constructors

TyContIXSym0KindInference :: forall r6989586621679205952 arg. SameKind (Apply TyContIXSym0 arg) (TyContIXSym1 arg) => TyContIXSym0 r6989586621679205952

Instances

SuppressUnusedWarnings TyContIXSym0

Defined in Control.Static.Static

Methods

suppressUnusedWarnings :: ()

type Apply TyContIXSym0 (r6989586621679205952 :: Type)

Defined in Control.Static.Static

type Apply TyContIXSym0 (r6989586621679205952 :: Type) = TyContIXSym1 r6989586621679205952

gwithStatic :: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap f vv) -> (forall k' v. Just '(k', v) ~ LookupKV k kk vv => Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv) => (c0 @@ k') @@ v => (c1 @@ k') @@ (f @@ v) => Sing k' -> (f @@ v) -> v -> (ext @@ v) -> r) -> Either SKeyedError r

Given an SKeyed of an external value g, do the following:

1. Lookup the corresponding internal value (I) of type v.
2. Decode the external value (X) of type g, if its type can be decoded into the type ext v.
3. Lookup the corresponding continuation (C).
4. Apply (C) to (I) and (X), returning a value of type r.

withStaticCts :: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r

withSomeStaticCts :: forall c0 c1 g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyedExt g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r

withStaticCxt :: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyed k g -> (forall k' v. Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r

withSomeStaticCxt :: forall c f g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyedExt g -> (forall k k' v. Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r