ruin-0.1.0.1: Pliable records

Data.Ruin.Ancillaries

Description

These definitions are typically not revealed to the user, unless you're doing something cheeky. So they are hidden behind this extra import.

Synopsis

# Type-level basics

type family (xs :: [k]) ++ (ys :: [k]) :: [k] where ... Source #

Equations

 '[] ++ ys = ys (x ': xs) ++ ys = x ': (xs ++ ys)

type family Difference (xs :: [k]) (ys :: [k]) :: [k] where ... Source #

Equations

 Difference '[] ys = '[] Difference (x ': xs) ys = If (Elem x ys) (Difference xs ys) (x ': Difference xs ys)

type family DifferenceByFst (xs :: [(k, v)]) (ys :: [k]) :: [(k, v)] where ... Source #

Equations

 DifferenceByFst '[] ys = '[] DifferenceByFst (x ': xs) ys = If (Elem (Fst x) ys) (DifferenceByFst xs ys) (x ': DifferenceByFst xs ys)

type family Elem (t :: k) (ts :: [k]) :: Bool where ... Source #

Equations

 Elem t '[] = False Elem t (t ': ts) = True Elem t (t2 ': ts) = Elem t ts

type family Fst (p :: (a, b)) :: a where ... Source #

Equations

 Fst '(a, _) = a

type family Head (xs :: [a]) :: a where ... Source #

Equations

 Head (a ': _) = a

type family Intersection (xs :: [k]) (ys :: [k]) :: [k] where ... Source #

Equations

 Intersection '[] ys = '[] Intersection (x ': xs) ys = If (Elem x ys) (x ': Intersection xs ys) (Intersection xs ys)

type family MapFst (ps :: [(a, b)]) :: [a] where ... Source #

Equations

 MapFst '[] = '[] MapFst ('(a, b) ': ps) = a ': MapFst ps

type family Snd (p :: (a, b)) :: b where ... Source #

Equations

 Snd '(_, b) = b

type family Tail (xs :: [a]) :: [a] where ... Source #

Equations

 Tail (_ ': as) = as

# Disjointedness

type DisjointFields a b = MustBeDisjoint a b (Intersection (FieldNames a) (FieldNames b)) Source #

These record types share no field names.

type family MustBeDisjoint (a :: *) (b :: *) (ss :: [Symbol]) :: Constraint where ... Source #

Equations

 MustBeDisjoint a b '[] = () MustBeDisjoint a b ss = TypeError ((((Text "ruin: The record types " :$$: (Text " " :<>: ShowType a)) :$$: Text "and") :$$: (Text " " :<>: ShowType b)) :$$: (Text "must be disjoint, but both have these fields: " :<>: ShowType ss))

type family MustHaveNoExtras (rc :: *) (ss :: [Symbol]) :: Constraint where ... Source #

Equations

 MustHaveNoExtras rc '[] = () MustHaveNoExtras rc ss = TypeError ((Text "ruin: The argument type" :$$: (Text " " :<>: ShowType rc)) :$$: (Text "has unused fields: " :<>: ShowType ss))

# Search

type family Find (rc :: *) (s :: Symbol) :: Maybe Loc where ... Source #

Equations

 Find (Pair l r) s = SearchBoth (Find l s) (Find r s) Find rc s = FindViaFields (Fields rc) s

type family FindViaFields (fields :: [(Symbol, *)]) (s :: Symbol) :: Maybe Loc where ... Source #

Equations

 FindViaFields '[] s = Nothing FindViaFields ('(s, ty) ': ss) s = Just Here FindViaFields ('(s1, ty) ': ss) s2 = FindViaFields ss s2

data Loc Source #

Constructors

 Here L Loc R Loc

Instances

 TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a Source # MethodsgArgsExtricate1 :: rep x -> Eval (s :@ a) TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a Source # MethodsmightExtricate1 :: rc -> Eval (s :@ a) (Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a Source # MethodsmightExtricate1 :: rc -> Eval (s :@ a) GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a Source # MethodsgArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a) GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a Source # MethodsgArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a) MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a) MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a) (~) (* -> *) rep (K1 i a) => GArgsHas dn (Just Loc Here) (M1 S (MetaSel (Just Symbol s) su ss ds) rep) s a Source # MethodsgArgsExtricate1 :: M1 S (MetaSel (Just Symbol s) su ss ds) rep x -> Eval (s :@ a)

type family MergeLoc (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where ... Source #

Equations

 MergeLoc Nothing Nothing = Nothing MergeLoc Nothing (Just r) = Just (R r) MergeLoc (Just l) _ = Just (L l)

class MightHave top mloc rc s a Source #

Minimal complete definition

mightExtricate1

Instances

 TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a Source # MethodsmightExtricate1 :: rc -> Eval (s :@ a) (Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a Source # MethodsmightExtricate1 :: rc -> Eval (s :@ a) MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a) MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a)

data Pair l r Source #

A custom tuple type. The library user should avoid mentioning this type directly. The only constructor exported by Data.Ruin is <@.

Note that the instance Has s (Pair l r) uses Has s l if s is in Fields l, even if s is also in Fields r.

Note the comment on the Build (Pair l r) instance: unlike tuples, Pairs are not record types.

Constructors

 MkPair l r infixr 3

Instances

 MightHave (Pair l r) (Find (Pair l r) s) (Pair l r) s (FieldType s (Pair l r)) => Has s (Pair l r) Source # Associated Typestype FieldType (s :: Symbol) (Pair l r) :: * Source # Methodsextricate1 :: Label s -> Pair l r -> Eval (FieldType s (Pair l r)) Source # MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a) MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a Source # MethodsmightExtricate1 :: Pair l r -> Eval (s :@ a) (Lift l, Lift r) => Lift (Pair l r) Source # Methodslift :: Pair l r -> Q Exp # (NFData l, NFData r) => NFData (Pair l r) Source # Methodsrnf :: Pair l r -> () # TypeError Constraint NoBuildPair => Build (Pair l r) Source # This is a non-instance. Associated Typestype Fields (Pair l r) :: [(Symbol, *)] Source #type Shape (Pair l r) o :: Constraint Source # Methodsbuild :: (Applicative i, GivesThese (Fields (Pair l r)) i rc) => rc -> Compose * * Eval i (Pair l r) Source #buildNonStrict :: GivesThese (Fields (Pair l r)) Identity rc => rc -> Pair l r Source # type FieldType s (Pair l r) Source # type FieldType s (Pair l r) type Fields (Pair l r) Source # type Fields (Pair l r) = (++) (Symbol, *) (Fields l) (DifferenceByFst Symbol * (Fields r) (FieldNames l)) type Shape (Pair l r) o Source # type Shape (Pair l r) o

type family SearchBoth (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where ... Source #

Equations

 SearchBoth (Just loc) _ = Just (L loc) SearchBoth _ (Just loc) = Just (R loc) SearchBoth _ _ = Nothing

unPair :: Pair l r -> (l, r) Source #

# Generics

class GArgsHas dn ml rep s a Source #

Minimal complete definition

gArgsExtricate1

Instances

 TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a Source # MethodsgArgsExtricate1 :: rep x -> Eval (s :@ a) GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a Source # MethodsgArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a) GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a Source # MethodsgArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a) (~) (* -> *) rep (K1 i a) => GArgsHas dn (Just Loc Here) (M1 S (MetaSel (Just Symbol s) su ss ds) rep) s a Source # MethodsgArgsExtricate1 :: M1 S (MetaSel (Just Symbol s) su ss ds) rep x -> Eval (s :@ a)

class GBox isABox t Source #

This class distinguishes between data T a = MkT a and data T a = Mk !a/newtype T a = MkT a, since Generic's from conflates the two.

The first index is assumed to be (IsABox (Rep t)).

Minimal complete definition

fromEval

Instances

 Generic t => GBox False t Source # MethodsfromEval :: t -> Eval (Rep t x) Generic t => GBox True t Source # MethodsfromEval :: t -> Eval (Rep t x)

type family GFieldType (ml :: Maybe Loc) (rep :: * -> *) :: * where ... Source #

Equations

 GFieldType (Just Here) (M1 S (MetaSel (Just s) su ss ds) (K1 i c)) = c GFieldType (Just loc) (M1 i c rep) = GFieldType (Just loc) rep GFieldType (Just (L loc)) (l :*: r) = GFieldType (Just loc) l GFieldType (Just (R loc)) (l :*: r) = GFieldType (Just loc) r

type family GFields (rep :: * -> *) :: [(Symbol, *)] where ... Source #

Equations

 GFields (M1 D c rep) = GFields rep GFields (M1 C c rep) = GFields rep GFields (M1 S (MetaSel (Just s) su ss ds) (K1 i c)) = '['(s, c)] GFields (l :*: r) = GFields l ++ GFields r GFields U1 = '[]

type family GFind (rep :: * -> *) (s :: Symbol) :: Maybe Loc where ... Source #

Equations

 GFind (M1 S (MetaSel (Just s) su ss ds) rep) s = Just Here GFind (M1 i c rep) s = GFind rep s GFind (l :*: r) s = MergeLoc (GFind l s) (GFind r s) GFind rep s = Nothing

class GenericBuildConArgs top dn rep Source #

Minimal complete definition

gRupConArgs, gBuildNonStrictConArgs

Instances

 GenericBuildConArgs top dn U1 Source # MethodsgRupConArgs :: (Applicative i, GivesThese (GFields U1) i rc) => rc -> Compose * * Eval i (U1 x)gBuildNonStrictConArgs :: GivesThese (GFields U1) Identity rc => rc -> U1 x (Lemma_AppendGivesThese (GFields l), GenericBuildConArgs top dn l, GenericBuildConArgs top dn r) => GenericBuildConArgs top dn ((:*:) l r) Source # MethodsgRupConArgs :: (Applicative i, GivesThese (GFields (l :*: r)) i rc) => rc -> Compose * * Eval i ((l :*: r) x)gBuildNonStrictConArgs :: GivesThese (GFields (l :*: r)) Identity rc => rc -> (l :*: r) x (Has s top, (~) (* -> *) rep (K1 i c)) => GenericBuildConArgs top dn (M1 S (MetaSel (Just Symbol s) su ss ds) rep) Source # MethodsgRupConArgs :: (Applicative i, GivesThese (GFields (M1 S (MetaSel (Just Symbol s) su ss ds) rep)) i rc) => rc -> Compose * * Eval i (M1 S (MetaSel (Just Symbol s) su ss ds) rep x)gBuildNonStrictConArgs :: GivesThese (GFields (M1 S (MetaSel (Just Symbol s) su ss ds) rep)) Identity rc => rc -> M1 S (MetaSel (Just Symbol s) su ss ds) rep x TypeError Constraint (NotBuildSyntax dn) => GenericBuildConArgs top dn (M1 S (MetaSel (Nothing Symbol) su ss ds) rep) Source # MethodsgRupConArgs :: (Applicative i, GivesThese (GFields (M1 S (MetaSel (Nothing Symbol) su ss ds) rep)) i rc) => rc -> Compose * * Eval i (M1 S (MetaSel (Nothing Symbol) su ss ds) rep x)gBuildNonStrictConArgs :: GivesThese (GFields (M1 S (MetaSel (Nothing Symbol) su ss ds) rep)) Identity rc => rc -> M1 S (MetaSel (Nothing Symbol) su ss ds) rep x

type family IsABox (rep :: * -> *) :: Bool where ... Source #

See GBox.

Equations

 IsABox (M1 D (MetaData _ _ _ False) (M1 C c (M1 S s (K1 k a)))) = True IsABox _ = False

## GHC.Generics defaults

class GenericBuild top rep Source #

Generic defintion of rup.

Minimal complete definition

gRup, gBuildNonStrict

Instances

type GenericFieldType s t = GFieldType (GFind (Rep t) s) (Rep t) Source #

GHC.Generics implementation of FieldType.

type GenericFields t = GFields (Rep t) Source #

GHC.Generics implementation of Fields.

class GenericHas rep s a Source #

Generic definition of has.

Minimal complete definition

gExtricate1

Instances

 TypeError Constraint (Not1ConstructorMessage dn) => GenericHas (M1 D (MetaData dn mn pn nt) V1) s a Source # MethodsgExtricate1 :: M1 D (MetaData dn mn pn nt) V1 x -> Eval (s :@ a) TypeError Constraint (Not1ConstructorMessage dn) => GenericHas (M1 D (MetaData dn mn pn nt) ((:+:) l r)) s a Source # MethodsgExtricate1 :: M1 D (MetaData dn mn pn nt) (l :+: r) x -> Eval (s :@ a) GArgsHas dn (GFind conargs s) conargs s a => GenericHas (M1 D (MetaData dn mn pn nt) (M1 C c conargs)) s a Source # MethodsgExtricate1 :: M1 D (MetaData dn mn pn nt) (M1 C c conargs) x -> Eval (s :@ a)

type family GenericShape (t :: k) (o :: *) :: Constraint where ... Source #

GenericShape t o requires that o is headed by the same type constructor that heads t:

  GenericShape (T ...) o = Hoid T o


This is the correct definition of Shape for all data types declared using record syntax, except for data family instances. For those, the T part should be replaced by the head of the data family instance: the type up to and including the indices but excluding the non-index parameters.

Equations

 GenericShape (f _) o = GenericShape f o GenericShape t o = Hoid t o

genericExtricate1 :: forall s t. (Generic t, GBox (IsABox (Rep t)) t, GenericHas (Rep t) s (FieldType s t)) => Label s -> t -> Eval (FieldType s t) Source #

GHC.Generics implementation of extricate1.

genericBuild :: forall t rc i. (Fields t ~ GenericFields t, Applicative i, Generic t, GenericBuild t (Rep t), GivesThese (Fields t) i rc) => rc -> Compose Eval i t Source #

GHC.Generics implementation of rup.

Relies on extricate1 in order to satisfy the Strictness law of Build.

genericBuildNonStrict :: forall t rc. (Fields t ~ GenericFields t, Generic t, GenericBuild t (Rep t), GivesThese (Fields t) Identity rc) => rc -> t Source #

GHC.Generics implementation of buildNonStrict.

It is maximally non-strict.

# Proxied

phoid :: forall t a. Hoid t a => Proxy# t -> a -> a Source #

hoid but with a proxy argument.

prfrom :: forall h rc t. (Hoid h rc, rc IsSymmetricRecordOf t, Build t) => Proxy# h -> rc -> t Source #

prto :: forall h t rc. (Hoid h t, rc IsSymmetricRecordOf t, Build t) => Proxy# h -> rc -> t Source #

# Miscellancy

newtype s :@ a infix 1 Source #

A record type with a single field.

Constructors

 Dub a

Instances

 (~) Symbol s1 s2 => Has s1 ((:@) s2 a) Source # Associated Typestype FieldType (s1 :: Symbol) ((:@) s2 a) :: * Source # Methodsextricate1 :: Label s1 -> (s2 :@ a) -> Eval (FieldType s1 (s2 :@ a)) Source # Functor ((:@) s) Source # Methodsfmap :: (a -> b) -> (s :@ a) -> s :@ b #(<\$) :: a -> (s :@ b) -> s :@ a # Generic1 ((:@) s) Source # Associated Typestype Rep1 ((:@) s :: * -> *) :: * -> * # Methodsfrom1 :: (s :@ a) -> Rep1 ((:@) s) a #to1 :: Rep1 ((:@) s) a -> s :@ a # Eq a => Eq ((:@) s a) Source # Methods(==) :: (s :@ a) -> (s :@ a) -> Bool #(/=) :: (s :@ a) -> (s :@ a) -> Bool # (Data a, KnownSymbol s) => Data ((:@) s a) Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (s :@ a) -> c (s :@ a) #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (s :@ a) #toConstr :: (s :@ a) -> Constr #dataTypeOf :: (s :@ a) -> DataType #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (s :@ a)) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (s :@ a)) #gmapT :: (forall b. Data b => b -> b) -> (s :@ a) -> s :@ a #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (s :@ a) -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (s :@ a) -> r #gmapQ :: (forall d. Data d => d -> u) -> (s :@ a) -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> (s :@ a) -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> (s :@ a) -> m (s :@ a) #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (s :@ a) -> m (s :@ a) #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (s :@ a) -> m (s :@ a) # Ord a => Ord ((:@) s a) Source # Methodscompare :: (s :@ a) -> (s :@ a) -> Ordering #(<) :: (s :@ a) -> (s :@ a) -> Bool #(<=) :: (s :@ a) -> (s :@ a) -> Bool #(>) :: (s :@ a) -> (s :@ a) -> Bool #(>=) :: (s :@ a) -> (s :@ a) -> Bool #max :: (s :@ a) -> (s :@ a) -> s :@ a #min :: (s :@ a) -> (s :@ a) -> s :@ a # (KnownSymbol s, Show a) => Show ((:@) s a) Source # MethodsshowsPrec :: Int -> (s :@ a) -> ShowS #show :: (s :@ a) -> String #showList :: [s :@ a] -> ShowS # Generic ((:@) s a) Source # Associated Typestype Rep ((:@) s a) :: * -> * # Methodsfrom :: (s :@ a) -> Rep (s :@ a) x #to :: Rep (s :@ a) x -> s :@ a # (Lift a, KnownSymbol s) => Lift ((:@) s a) Source # Methodslift :: (s :@ a) -> Q Exp # Binary a => Binary ((:@) s a) Source # Methodsput :: (s :@ a) -> Put #get :: Get (s :@ a) #putList :: [s :@ a] -> Put # Serialize a => Serialize ((:@) s a) Source # Methodsput :: Putter (s :@ a) #get :: Get (s :@ a) # NFData a => NFData ((:@) s a) Source # Methodsrnf :: (s :@ a) -> () # Build ((:@) s a) Source # Associated Typestype Fields ((:@) s a) :: [(Symbol, *)] Source #type Shape ((:@) s a) o :: Constraint Source # Methodsbuild :: (Applicative i, GivesThese (Fields (s :@ a)) i rc) => rc -> Compose * * Eval i (s :@ a) Source #buildNonStrict :: GivesThese (Fields (s :@ a)) Identity rc => rc -> s :@ a Source # type FieldType s1 ((:@) s2 a) Source # type FieldType s1 ((:@) s2 a) = a type Rep1 ((:@) s) Source # type Rep1 ((:@) s) = D1 (MetaData ":@" "Data.Ruin.All" "ruin-0.1.0.1-1nMKf3bIpLD7vK6e2S9ClO" True) (C1 (MetaCons "Dub" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) Par1)) type Rep ((:@) s a) Source # type Rep ((:@) s a) = D1 (MetaData ":@" "Data.Ruin.All" "ruin-0.1.0.1-1nMKf3bIpLD7vK6e2S9ClO" True) (C1 (MetaCons "Dub" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) type Fields ((:@) s a) Source # type Fields ((:@) s a) = (:) (Symbol, *) ((,) Symbol * s a) ([] (Symbol, *)) type Shape ((:@) s _) o Source # type Shape ((:@) s _) o = Hoid * (* -> *) ((:@) s) o

type IsSubtypeOf rc t = GivesThese (Fields t) Identity (GiveAllItHas rc) Source #

The width subtyping relation, with evidence.

type IsSymmetricRecordOf t rc = (t IsSubtypeOf rc, NoExtraFields t rc (FieldNames t) (FieldNames rc)) Source #

class Gives s a i rc where Source #

The key difference betwen Gives and Has is that the codomain is a class index instead of FieldType s rc. This enables instances like Monoid a => Gives s a MEmpty.

Minimal complete definition

get

Methods

get :: rc -> Compose Eval i a Source #

Instances

 (Applicative i, (~) * a (FieldType s rc), Has s rc) => Gives s a i (GiveAllItHas rc) Source # Methodsget :: GiveAllItHas rc -> Compose * * Eval i a Source #

newtype GiveAllItHas rc Source #

A newtype whose only utility is its parametric Gives instance, which defers to Has.

Constructors

 MkGiveAllItHas rc

Instances

 (Applicative i, (~) * a (FieldType s rc), Has s rc) => Gives s a i (GiveAllItHas rc) Source # Methodsget :: GiveAllItHas rc -> Compose * * Eval i a Source #

type family GivesThese (fields :: [(Symbol, *)]) (i :: * -> *) (rc :: *) :: Constraint where ... Source #

Equations

 GivesThese '[] i rc = () GivesThese (f ': fs) i rc = (GivesThis f i rc, GivesThese fs i rc)

type family GivesThis (field :: (Symbol, *)) (i :: * -> *) (rc :: *) :: Constraint where ... Source #

Equations

 GivesThis f i rc = Gives (Fst f) (Snd f) i rc

type family Hoid (t :: k) (a :: k2) :: Constraint where ... Source #

Do not reuse; consider this an implementation detail of hoid.

Equations

 Hoid (t :: _ -> cod) a = Hoid (t (Lookup t cod a)) a Hoid t a = t ~~ a

data Label s Source #

Use -XOverloadedLabels to create labels. For example, #x :: Label "x".

Or use mkLabel.

Constructors

 MkLabel

Instances

 (~) Symbol s1 s2 => IsLabel s1 (Label s2) Source # MethodsfromLabel :: Proxy# Symbol s1 -> Label s2 #

class Lemma_AppendGivesThese fs1 Source #

If Has (fs1 ++ fs2) rc, then Has fs1 rc and Has fs2 rc.

Minimal complete definition

lemmaFst, lemmaSnd

Instances

 Lemma_AppendGivesThese ([] (Symbol, *)) Source # MethodslemmaFst :: GivesThese (((Symbol, *) ++ [(Symbol, *)]) fs2) i rc => Proxy# (* -> *) i -> Proxy# [(Symbol, *)] fs2 -> (GivesThese [(Symbol, *)] i rc -> rc -> a) -> rc -> alemmaSnd :: GivesThese (((Symbol, *) ++ [(Symbol, *)]) fs2) i rc => Proxy# (* -> *) i -> Proxy# [(Symbol, *)] fs2 -> (GivesThese fs2 i rc -> rc -> a) -> rc -> a Lemma_AppendGivesThese fs1 => Lemma_AppendGivesThese ((:) (Symbol, *) f fs1) Source # MethodslemmaFst :: GivesThese (((Symbol, *) ++ ((Symbol, *) ': f) fs1) fs2) i rc => Proxy# (* -> *) i -> Proxy# [(Symbol, *)] fs2 -> (GivesThese (((Symbol, *) ': f) fs1) i rc -> rc -> a) -> rc -> alemmaSnd :: GivesThese (((Symbol, *) ++ ((Symbol, *) ': f) fs1) fs2) i rc => Proxy# (* -> *) i -> Proxy# [(Symbol, *)] fs2 -> (GivesThese fs2 i rc -> rc -> a) -> rc -> a

type SymmetricRecordsA t i rc = (GivesThese (Fields t) i (GiveAllItHasA rc), NoExtraFields t rc (FieldNames t) (FieldNames rc)) Source #

data Tup1 a Source #

This is a "tuple of one component", so that it can have a data constructor like all the other tuples.

It is crucially not a newtype!

Constructors

 MkTup1 a

Instances

 Has s a => Has s (Tup1 a) Source # Associated Typestype FieldType (s :: Symbol) (Tup1 a) :: * Source # Methodsextricate1 :: Label s -> Tup1 a -> Eval (FieldType s (Tup1 a)) Source # Show a => Show (Tup1 a) Source # MethodsshowsPrec :: Int -> Tup1 a -> ShowS #show :: Tup1 a -> String #showList :: [Tup1 a] -> ShowS # Build a => Build (Tup1 a) Source # Associated Typestype Fields (Tup1 a) :: [(Symbol, *)] Source #type Shape (Tup1 a) o :: Constraint Source # Methodsbuild :: (Applicative i, GivesThese (Fields (Tup1 a)) i rc) => rc -> Compose * * Eval i (Tup1 a) Source #buildNonStrict :: GivesThese (Fields (Tup1 a)) Identity rc => rc -> Tup1 a Source # type FieldType s (Tup1 a) Source # type FieldType s (Tup1 a) = FieldType s a type Fields (Tup1 a) Source # type Fields (Tup1 a) = Fields a type Shape (Tup1 a) o Source # type Shape (Tup1 a) o

mkLabel :: forall s. Label s Source #

Creates a label that is determined either by type inference or via -XTypeApplications.

rupEval :: forall t rc. (Build t, rc IsSubtypeOf t) => rc -> Eval t Source #

rup = runEval . rupEval
rupEval = build . MkGiveAllItHas

rupNonStrict :: forall t rc. (Build t, rc IsSubtypeOf t) => rc -> t Source #

rupNonStrict = buildNonStrict . MkGiveAllItHas