Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 family (xs :: [k]) ++ (ys :: [k]) :: [k] where ...
- type family Difference (xs :: [k]) (ys :: [k]) :: [k] where ...
- type family DifferenceByFst (xs :: [(k, v)]) (ys :: [k]) :: [(k, v)] where ...
- type family Elem (t :: k) (ts :: [k]) :: Bool where ...
- type family Fst (p :: (a, b)) :: a where ...
- type family Head (xs :: [a]) :: a where ...
- type family Intersection (xs :: [k]) (ys :: [k]) :: [k] where ...
- type family MapFst (ps :: [(a, b)]) :: [a] where ...
- type family Snd (p :: (a, b)) :: b where ...
- type family Tail (xs :: [a]) :: [a] where ...
- type DisjointFields a b = MustBeDisjoint a b (Intersection (FieldNames a) (FieldNames b))
- type family MustBeDisjoint (a :: *) (b :: *) (ss :: [Symbol]) :: Constraint where ...
- type family MustHaveNoExtras (rc :: *) (ss :: [Symbol]) :: Constraint where ...
- type family Find (rc :: *) (s :: Symbol) :: Maybe Loc where ...
- type family FindViaFields (fields :: [(Symbol, *)]) (s :: Symbol) :: Maybe Loc where ...
- data Loc
- type family MergeLoc (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where ...
- class MightHave top mloc rc s a
- data Pair l r = MkPair l r
- type family SearchBoth (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where ...
- unPair :: Pair l r -> (l, r)
- class GArgsHas dn ml rep s a
- class GBox isABox t
- type family GFieldType (ml :: Maybe Loc) (rep :: * -> *) :: * where ...
- type family GFields (rep :: * -> *) :: [(Symbol, *)] where ...
- type family GFind (rep :: * -> *) (s :: Symbol) :: Maybe Loc where ...
- class GenericBuildConArgs top dn rep
- type family IsABox (rep :: * -> *) :: Bool where ...
- class GenericBuild top rep
- type GenericFieldType s t = GFieldType (GFind (Rep t) s) (Rep t)
- type GenericFields t = GFields (Rep t)
- class GenericHas rep s a
- type family GenericShape (t :: k) (o :: *) :: Constraint where ...
- 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)
- 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
- genericBuildNonStrict :: forall t rc. (Fields t ~ GenericFields t, Generic t, GenericBuild t (Rep t), GivesThese (Fields t) Identity rc) => rc -> t
- phoid :: forall t a. Hoid t a => Proxy# t -> a -> a
- 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
- newtype s :@ a = Dub a
- type FieldNames t = MapFst (Fields t)
- type IsSubtypeOf rc t = GivesThese (Fields t) Identity (GiveAllItHas rc)
- type IsSymmetricRecordOf t rc = (t `IsSubtypeOf` rc, NoExtraFields t rc (FieldNames t) (FieldNames rc))
- class Gives s a i rc where
- newtype GiveAllItHas rc = MkGiveAllItHas rc
- type family GivesThese (fields :: [(Symbol, *)]) (i :: * -> *) (rc :: *) :: Constraint where ...
- type family GivesThis (field :: (Symbol, *)) (i :: * -> *) (rc :: *) :: Constraint where ...
- type family Hoid (t :: k) (a :: k2) :: Constraint where ...
- data Label s = MkLabel
- class Lemma_AppendGivesThese fs1
- type SymmetricRecordsA t i rc = (GivesThese (Fields t) i (GiveAllItHasA rc), NoExtraFields t rc (FieldNames t) (FieldNames rc))
- data Tup1 a = MkTup1 a
- mkLabel :: forall s. Label s
- rupEval :: forall t rc. (Build t, rc `IsSubtypeOf` t) => rc -> Eval t
- rupNonStrict :: forall t rc. (Build t, rc `IsSubtypeOf` t) => rc -> t
Type-level basics
type family Difference (xs :: [k]) (ys :: [k]) :: [k] where ... Source #
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 #
DifferenceByFst '[] ys = '[] | |
DifferenceByFst (x ': xs) ys = If (Elem (Fst x) ys) (DifferenceByFst xs ys) (x ': DifferenceByFst xs ys) |
type family Intersection (xs :: [k]) (ys :: [k]) :: [k] where ... Source #
Intersection '[] ys = '[] | |
Intersection (x ': xs) ys = If (Elem x ys) (x ': Intersection xs ys) (Intersection xs ys) |
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 #
type family MustHaveNoExtras (rc :: *) (ss :: [Symbol]) :: Constraint where ... Source #
Search
type family Find (rc :: *) (s :: Symbol) :: Maybe Loc where ... Source #
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 #
FindViaFields '[] s = Nothing | |
FindViaFields ('(s, ty) ': ss) s = Just Here | |
FindViaFields ('(s1, ty) ': ss) s2 = FindViaFields ss s2 |
TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a Source # | |
TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a Source # | |
(Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a Source # | |
GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a Source # | |
GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a Source # | |
MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a Source # | |
MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a Source # | |
(~) (* -> *) rep (K1 i a) => GArgsHas dn (Just Loc Here) (M1 S (MetaSel (Just Symbol s) su ss ds) rep) s a Source # | |
class MightHave top mloc rc s a Source #
mightExtricate1
TypeError Constraint (NoSuchField s top) => MightHave top (Nothing Loc) rc s a Source # | |
(Has s rc, (~) * a (FieldType s rc)) => MightHave top (Just Loc Here) rc s a Source # | |
MightHave top (Just Loc loc) r s a => MightHave top (Just Loc (R loc)) (Pair l r) s a Source # | |
MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a 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
uses Has
s (Pair
l r)
if
Has
s ls
is in
, even if Fields
ls
is also in
.Fields
r
Note the comment on the
instance: unlike
tuples, Build
(Pair
l r)Pair
s are not record types.
MkPair l r infixr 3 |
MightHave (Pair l r) (Find (Pair l r) s) (Pair l r) s (FieldType s (Pair l r)) => Has 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 # | |
MightHave top (Just Loc loc) l s a => MightHave top (Just Loc (L loc)) (Pair l r) s a Source # | |
(Lift l, Lift r) => Lift (Pair l r) Source # | |
(NFData l, NFData r) => NFData (Pair l r) Source # | |
TypeError Constraint NoBuildPair => Build (Pair l r) Source # | This is a non-instance. |
type FieldType s (Pair l r) Source # | |
type Fields (Pair l r) Source # | |
type Shape (Pair l r) o Source # | |
type family SearchBoth (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where ... Source #
SearchBoth (Just loc) _ = Just (L loc) | |
SearchBoth _ (Just loc) = Just (R loc) | |
SearchBoth _ _ = Nothing |
Generics
class GArgsHas dn ml rep s a Source #
gArgsExtricate1
TypeError Constraint (NoSuchSelector dn s) => GArgsHas dn (Nothing Loc) rep s a Source # | |
GArgsHas dn (Just Loc loc) r s a => GArgsHas dn (Just Loc (R loc)) ((:*:) l r) s a Source # | |
GArgsHas dn (Just Loc loc) l s a => GArgsHas dn (Just Loc (L loc)) ((:*:) l r) s a Source # | |
(~) (* -> *) rep (K1 i a) => GArgsHas dn (Just Loc Here) (M1 S (MetaSel (Just Symbol s) su ss ds) rep) s a 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))
fromEval
type family GFieldType (ml :: Maybe Loc) (rep :: * -> *) :: * where ... Source #
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 |
class GenericBuildConArgs top dn rep Source #
gRupConArgs, gBuildNonStrictConArgs
GenericBuildConArgs top dn U1 Source # | |
(Lemma_AppendGivesThese (GFields l), GenericBuildConArgs top dn l, GenericBuildConArgs top dn r) => GenericBuildConArgs top dn ((:*:) l r) Source # | |
(Has s top, (~) (* -> *) rep (K1 i c)) => GenericBuildConArgs top dn (M1 S (MetaSel (Just Symbol s) su ss ds) rep) Source # | |
TypeError Constraint (NotBuildSyntax dn) => GenericBuildConArgs top dn (M1 S (MetaSel (Nothing Symbol) su ss ds) rep) Source # | |
GHC.Generics
defaults
class GenericBuild top rep Source #
Generic defintion of rup
.
gRup, gBuildNonStrict
GenericBuildConArgs top dn rep => GenericBuild top (M1 D (MetaData dn mn pn nt) (M1 C c rep)) Source # | |
TypeError Constraint (TooManyConstructors dn) => GenericBuild top (M1 D (MetaData dn mn pn nt) ((:+:) l r)) Source # | |
TypeError Constraint (NoConstructors dn) => GenericBuild top (M1 D (MetaData dn mn pn nt) V1) Source # | |
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
.
gExtricate1
TypeError Constraint (Not1ConstructorMessage dn) => GenericHas (M1 D (MetaData dn mn pn nt) V1) s a Source # | |
TypeError Constraint (Not1ConstructorMessage dn) => GenericHas (M1 D (MetaData dn mn pn nt) ((:+:) l r)) s a Source # | |
GArgsHas dn (GFind conargs s) conargs s a => GenericHas (M1 D (MetaData dn mn pn nt) (M1 C c conargs)) s a Source # | |
type family GenericShape (t :: k) (o :: *) :: Constraint where ... Source #
requires that GenericShape
t oo
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.
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
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.
Dub a |
(~) Symbol s1 s2 => Has s1 ((:@) s2 a) Source # | |
Functor ((:@) s) Source # | |
Generic1 ((:@) s) Source # | |
Eq a => Eq ((:@) s a) Source # | |
(Data a, KnownSymbol s) => Data ((:@) s a) Source # | |
Ord a => Ord ((:@) s a) Source # | |
(KnownSymbol s, Show a) => Show ((:@) s a) Source # | |
Generic ((:@) s a) Source # | |
(Lift a, KnownSymbol s) => Lift ((:@) s a) Source # | |
Binary a => Binary ((:@) s a) Source # | |
Serialize a => Serialize ((:@) s a) Source # | |
NFData a => NFData ((:@) s a) Source # | |
Build ((:@) s a) Source # | |
type FieldType s1 ((:@) s2 a) Source # | |
type Rep1 ((:@) s) Source # | |
type Rep ((:@) s a) Source # | |
type Fields ((:@) s a) Source # | |
type Shape ((:@) s _) o Source # | |
type FieldNames t = MapFst (Fields t) Source #
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
. This enables
instances like FieldType
s rcMonoid a =>
.Gives
s a MEmpty
(Applicative i, (~) * a (FieldType s rc), Has s rc) => Gives s a i (GiveAllItHas rc) Source # | |
newtype GiveAllItHas rc Source #
(Applicative i, (~) * a (FieldType s rc), Has s rc) => Gives s a i (GiveAllItHas rc) Source # | |
type family GivesThese (fields :: [(Symbol, *)]) (i :: * -> *) (rc :: *) :: Constraint where ... Source #
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 #
type family Hoid (t :: k) (a :: k2) :: Constraint where ... Source #
Do not reuse; consider this an implementation detail of hoid
.
Use -XOverloadedLabels
to create labels. For example, #x ::
Label "x"
.
Or use mkLabel
.
class Lemma_AppendGivesThese fs1 Source #
lemmaFst, lemmaSnd
Lemma_AppendGivesThese ([] (Symbol, *)) Source # | |
Lemma_AppendGivesThese fs1 => Lemma_AppendGivesThese ((:) (Symbol, *) f fs1) Source # | |
type SymmetricRecordsA t i rc = (GivesThese (Fields t) i (GiveAllItHasA rc), NoExtraFields t rc (FieldNames t) (FieldNames rc)) 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!
MkTup1 a |
mkLabel :: forall s. Label s Source #
Creates a label that is determined either by type inference or
via -XTypeApplications
.
rupNonStrict :: forall t rc. (Build t, rc `IsSubtypeOf` t) => rc -> t Source #