Data.Ruin.Ancillaries

How the sausage is made.

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

Type-level basics

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

Equations

'[] ++ ys = ys

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

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

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

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

Equations

Elem t '[] = False

Elem t (t ': ts) = True

Elem t (t2 ': ts) = Elem t ts

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

Equations

Fst '(a, _) = a

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

Equations

Head (a ': _) = a

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

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

Equations

MapFst '[] = '[]

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

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

Equations

Snd '(_, b) = b

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

Equations

Tail (_ ': as) = as

Disjointedness

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

These record types share no field names.

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

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

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

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

Equations

FindViaFields '[] s = Nothing

FindViaFields ('(s, ty) ': ss) s = Just Here

FindViaFields ('(s1, ty) ': ss) s2 = FindViaFields ss s2

data Loc

Constructors

Here

L Loc

R Loc

Instances

TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a

Methods

gArgsExtricate1 :: rep x -> Eval (s :@ a)

TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a

Methods

mightExtricate1 :: rc -> Eval (s :@ a)

(Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a

Methods

mightExtricate1 :: rc -> Eval (s :@ a)

GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a

Methods

gArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a)

GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a

Methods

gArgsExtricate1 :: (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

Methods

mightExtricate1 :: 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

Methods

mightExtricate1 :: 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

Methods

gArgsExtricate1 :: 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 ...

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

Minimal complete definition

mightExtricate1

Instances

TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a

Methods

mightExtricate1 :: rc -> Eval (s :@ a)

(Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a

Methods

mightExtricate1 :: rc -> Eval (s :@ a)

MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a

Methods

mightExtricate1 :: 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

Methods

mightExtricate1 :: Pair l r -> Eval (s :@ a)

data Pair l r

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)

Associated Types

type FieldType (s :: Symbol) (Pair l r) :: *

Methods

extricate1 :: Label s -> Pair l r -> Eval (FieldType s (Pair l r))

MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a

Methods

mightExtricate1 :: 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

Methods

mightExtricate1 :: Pair l r -> Eval (s :@ a)

(Lift l, Lift r) => Lift (Pair l r)

Methods

lift :: Pair l r -> Q Exp

(NFData l, NFData r) => NFData (Pair l r)

Methods

rnf :: Pair l r -> ()

TypeError Constraint NoBuildPair => Build (Pair l r)

This is a non-instance.

Associated Types

type Fields (Pair l r) :: [(Symbol, *)]

type Shape (Pair l r) o :: Constraint

Methods

build :: (Applicative i, GivesThese (Fields (Pair l r)) i rc) => rc -> Compose * * Eval i (Pair l r)

buildNonStrict :: GivesThese (Fields (Pair l r)) Identity rc => rc -> Pair l r

type FieldType s (Pair l r)

type FieldType s (Pair l r)

type Fields (Pair l r)

type Fields (Pair l r) = (++) (Symbol, *) (Fields l) (DifferenceByFst Symbol * (Fields r) (FieldNames l))

type Shape (Pair l r) o

type Shape (Pair l r) o

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

Equations

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

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

SearchBoth _ _ = Nothing

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

Generics

class GArgsHas dn ml rep s a

Minimal complete definition

gArgsExtricate1

Instances

TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a

Methods

gArgsExtricate1 :: rep x -> Eval (s :@ a)

GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a

Methods

gArgsExtricate1 :: (l :*: r) x -> Eval (s :@ a)

GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a

Methods

gArgsExtricate1 :: (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

Methods

gArgsExtricate1 :: M1 S (MetaSel (Just Symbol s) su ss ds) rep x -> Eval (s :@ a)

class GBox isABox t

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

Methods

fromEval :: t -> Eval (Rep t x)

Generic t => GBox True t

Methods

fromEval :: t -> Eval (Rep t x)

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

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

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

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

Minimal complete definition

gRupConArgs, gBuildNonStrictConArgs

Instances

GenericBuildConArgs top dn U1

Methods

gRupConArgs :: (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)

Methods

gRupConArgs :: (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)

Methods

gRupConArgs :: (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)

Methods

gRupConArgs :: (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 ...

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

Generic defintion of rup.

Minimal complete definition

gRup, gBuildNonStrict

Instances

GenericBuildConArgs top dn rep => GenericBuild top (M1 D (MetaData dn mn pn nt) (M1 C c rep))

Methods

gRup :: (Applicative i, GivesThese (GFields (M1 D (MetaData dn mn pn nt) (M1 C c rep))) i rc) => rc -> Compose * * Eval i (M1 D (MetaData dn mn pn nt) (M1 C c rep) x)

gBuildNonStrict :: GivesThese (GFields (M1 D (MetaData dn mn pn nt) (M1 C c rep))) Identity rc => rc -> M1 D (MetaData dn mn pn nt) (M1 C c rep) x

TypeError Constraint (TooManyConstructors dn) => GenericBuild top (M1 D (MetaData dn mn pn nt) ((:+:) l r))

Methods

gRup :: (Applicative i, GivesThese (GFields (M1 D (MetaData dn mn pn nt) (l :+: r))) i rc) => rc -> Compose * * Eval i (M1 D (MetaData dn mn pn nt) (l :+: r) x)

gBuildNonStrict :: GivesThese (GFields (M1 D (MetaData dn mn pn nt) (l :+: r))) Identity rc => rc -> M1 D (MetaData dn mn pn nt) (l :+: r) x

TypeError Constraint (NoConstructors dn) => GenericBuild top (M1 D (MetaData dn mn pn nt) V1)

Methods

gRup :: (Applicative i, GivesThese (GFields (M1 D (MetaData dn mn pn nt) V1)) i rc) => rc -> Compose * * Eval i (M1 D (MetaData dn mn pn nt) V1 x)

gBuildNonStrict :: GivesThese (GFields (M1 D (MetaData dn mn pn nt) V1)) Identity rc => rc -> M1 D (MetaData dn mn pn nt) V1 x

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

GHC.Generics implementation of FieldType.

type GenericFields t = GFields (Rep t)

GHC.Generics implementation of Fields.

class GenericHas rep s a

Generic definition of has.

Minimal complete definition

gExtricate1

Instances

TypeError Constraint (Not1ConstructorMessage dn) => GenericHas (M1 D (MetaData dn mn pn nt) V1) s a

Methods

gExtricate1 :: 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

Methods

gExtricate1 :: 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

Methods

gExtricate1 :: M1 D (MetaData dn mn pn nt) (M1 C c conargs) x -> Eval (s :@ a)

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

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)

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

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

GHC.Generics implementation of buildNonStrict.

It is maximally non-strict.

Proxied

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

hoid but with a proxy argument.

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

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

Miscellancy

newtype s :@ a infix 1

A record type with a single field.

Constructors

Dub a

Instances

(~) Symbol s1 s2 => Has s1 ((:@) s2 a)

Associated Types

type FieldType (s1 :: Symbol) ((:@) s2 a) :: *

Methods

extricate1 :: Label s1 -> (s2 :@ a) -> Eval (FieldType s1 (s2 :@ a))

Functor ((:@) s)

Methods

fmap :: (a -> b) -> (s :@ a) -> s :@ b

(<$) :: a -> (s :@ b) -> s :@ a

Generic1 ((:@) s)

Associated Types

type Rep1 ((:@) s :: * -> *) :: * -> *

Methods

from1 :: (s :@ a) -> Rep1 ((:@) s) a

to1 :: Rep1 ((:@) s) a -> s :@ a

Eq a => Eq ((:@) s a)

Methods

(==) :: (s :@ a) -> (s :@ a) -> Bool

(/=) :: (s :@ a) -> (s :@ a) -> Bool

(Data a, KnownSymbol s) => Data ((:@) s a)

Methods

gfoldl :: (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)

Methods

compare :: (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)

Methods

showsPrec :: Int -> (s :@ a) -> ShowS

show :: (s :@ a) -> String

showList :: [s :@ a] -> ShowS

Generic ((:@) s a)

Associated Types

type Rep ((:@) s a) :: * -> *

Methods

from :: (s :@ a) -> Rep (s :@ a) x

to :: Rep (s :@ a) x -> s :@ a

(Lift a, KnownSymbol s) => Lift ((:@) s a)

Methods

lift :: (s :@ a) -> Q Exp

Binary a => Binary ((:@) s a)

Methods

put :: (s :@ a) -> Put

get :: Get (s :@ a)

putList :: [s :@ a] -> Put

Serialize a => Serialize ((:@) s a)

Methods

put :: Putter (s :@ a)

get :: Get (s :@ a)

NFData a => NFData ((:@) s a)

Methods

rnf :: (s :@ a) -> ()

Build ((:@) s a)

Associated Types

type Fields ((:@) s a) :: [(Symbol, *)]

type Shape ((:@) s a) o :: Constraint

Methods

build :: (Applicative i, GivesThese (Fields (s :@ a)) i rc) => rc -> Compose * * Eval i (s :@ a)

buildNonStrict :: GivesThese (Fields (s :@ a)) Identity rc => rc -> s :@ a

type FieldType s1 ((:@) s2 a)

type FieldType s1 ((:@) s2 a) = a

type Rep1 ((:@) s)

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)

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)

type Fields ((:@) s a) = (:) (Symbol, *) ((,) Symbol * s a) ([] (Symbol, *))

type Shape ((:@) s _) o

type Shape ((:@) s _) o = Hoid * (* -> *) ((:@) s) o

type FieldNames t = MapFst (Fields t)

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

The width subtyping relation, with evidence.

type IsSymmetricRecordOf t rc = (t `IsSubtypeOf` rc, NoExtraFields t rc (FieldNames t) (FieldNames rc))

class Gives s a i rc where

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

Instances

(Applicative i, (~) * a (FieldType s rc), Has s rc) => Gives s a i (GiveAllItHas rc)

Methods

get :: GiveAllItHas rc -> Compose * * Eval i a

newtype GiveAllItHas rc

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)

Methods

get :: GiveAllItHas rc -> Compose * * Eval i a

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

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

Equations

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

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

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

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

Or use mkLabel.

Constructors

MkLabel

Instances

(~) Symbol s1 s2 => IsLabel s1 (Label s2)

Methods

fromLabel :: Proxy# Symbol s1 -> Label s2

class Lemma_AppendGivesThese fs1

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

Minimal complete definition

lemmaFst, lemmaSnd

Instances

Lemma_AppendGivesThese ([] (Symbol, *))

Methods

lemmaFst :: GivesThese (((Symbol, *) ++ [(Symbol, *)]) fs2) i rc => Proxy# (* -> *) i -> Proxy# [(Symbol, *)] fs2 -> (GivesThese [(Symbol, *)] i rc -> rc -> a) -> rc -> a

lemmaSnd :: 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)

Methods

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

lemmaSnd :: 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))

data Tup1 a

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)

Associated Types

type FieldType (s :: Symbol) (Tup1 a) :: *

Methods

extricate1 :: Label s -> Tup1 a -> Eval (FieldType s (Tup1 a))

Show a => Show (Tup1 a)

Methods

showsPrec :: Int -> Tup1 a -> ShowS

show :: Tup1 a -> String

showList :: [Tup1 a] -> ShowS

Build a => Build (Tup1 a)

Associated Types

type Fields (Tup1 a) :: [(Symbol, *)]

type Shape (Tup1 a) o :: Constraint

Methods

build :: (Applicative i, GivesThese (Fields (Tup1 a)) i rc) => rc -> Compose * * Eval i (Tup1 a)

buildNonStrict :: GivesThese (Fields (Tup1 a)) Identity rc => rc -> Tup1 a

type FieldType s (Tup1 a)

type FieldType s (Tup1 a) = FieldType s a

type Fields (Tup1 a)

type Fields (Tup1 a) = Fields a

type Shape (Tup1 a) o

type Shape (Tup1 a) o

mkLabel :: forall s. Label s

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

rup = runEval . rupEval

rupEval = build . MkGiveAllItHas

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

rupNonStrict = buildNonStrict . MkGiveAllItHas