free-foil-0.4.0: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads)
Safe HaskellNone
LanguageHaskell2010

Data.ZipMatchK.Generic

Synopsis

Documentation

class ZipMatchK (f :: k) where Source #

Kind-polymorphic syntactic (first-order) unification of two values.

Note that f is expected to be a traversable n-functor. There is no TraversableK constraint to say so at the moment.

The default implementation is generic, via RepK. It is convenient, but it reflects each node into a representation and back on every comparison, and a constructor is represented as a chain of L1/R1 wrappers as long as its index, so the cost grows with the size of the signature. Comparing terms is most of what a typechecker does, and on a large signature the generic instance costs roughly twice what the written-out one does. Use deriveZipMatchK (or deriveZipMatchK2, for a signature bifunctor with extra parameters) to generate the written-out instance instead.

Since: 0.2.0

Minimal complete definition

Nothing

Methods

zipMatchWithK :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). Mappings as bs cs -> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs) Source #

Perform one level of equality testing:

  • when k = Type, values are compared directly (e.g. via Eq);
  • when k = Type -> Type, term constructors are compared. Unequal constructors give Nothing, and equal ones have all their components paired up with a given function.

Since: 0.2.0

default zipMatchWithK :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs) => Mappings as bs cs -> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs) Source #

Instances

Instances details
ZipMatchK Either Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (Either :@@: as) -> (Either :@@: bs) -> Maybe (Either :@@: cs) Source #

ZipMatchK (,) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> ((,) :@@: as) -> ((,) :@@: bs) -> Maybe ((,) :@@: cs) Source #

ZipMatchK NonEmpty Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (NonEmpty :@@: as) -> (NonEmpty :@@: bs) -> Maybe (NonEmpty :@@: cs) Source #

ZipMatchK Maybe Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (Maybe :@@: as) -> (Maybe :@@: bs) -> Maybe (Maybe :@@: cs) Source #

ZipMatchK [] Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> ([] :@@: as) -> ([] :@@: bs) -> Maybe ([] :@@: cs) Source #

ZipMatchK a => ZipMatchK (Either a :: Type -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (Either a :@@: as) -> (Either a :@@: bs) -> Maybe (Either a :@@: cs) Source #

ZipMatchK a => ZipMatchK ((,) a :: Type -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> ((,) a :@@: as) -> ((,) a :@@: bs) -> Maybe ((,) a :@@: cs) Source #

(ZipMatchK ann, ZipMatchK sig) => ZipMatchK (AnnSig ann sig :: Type -> Type -> Type) Source #

Matching for AnnSig is derived, not left to the generic default.

The generic default would rebuild the Generics.Kind view of every node on every comparison, and comparing terms is most of what a typechecker does, so for an annotated signature, where it lands on the hottest path, that is a measurable cost. deriveZipMatchK2 generates the written-out instance instead: the annotation matched with the term zipper (an annotation is a functor of the term), and the inner signature with both. Write deriveZipMatchK2 ''YourAnnSig for a bespoke annotated signature.

Instance details

Defined in Control.Monad.Free.Foil.Annotated

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (AnnSig ann sig :@@: as) -> (AnnSig ann sig :@@: bs) -> Maybe (AnnSig ann sig :@@: cs) Source #

(Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f g :: Type -> Type) Source #

Note: instance is limited to Type-kinded bifunctors f and g.

Instance details

Defined in Data.ZipMatchK.Functor

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (Product f g :@@: as) -> (Product f g :@@: bs) -> Maybe (Product f g :@@: cs) Source #

(Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f g :: Type -> Type) Source #

Note: instance is limited to Type-kinded bifunctors f and g.

Instance details

Defined in Data.ZipMatchK.Functor

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (Sum f g :@@: as) -> (Sum f g :@@: bs) -> Maybe (Sum f g :@@: cs) Source #

(Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f g :: Type -> Type -> Type) Source #

Note: instance is limited to Type-kinded bifunctors f and g.

Instance details

Defined in Data.ZipMatchK.Bifunctor

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (Product f g :@@: as) -> (Product f g :@@: bs) -> Maybe (Product f g :@@: cs) Source #

(Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f g :: Type -> Type -> Type) Source #

Note: instance is limited to Type-kinded bifunctors f and g.

Instance details

Defined in Data.ZipMatchK.Bifunctor

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (Sum f g :@@: as) -> (Sum f g :@@: bs) -> Maybe (Sum f g :@@: cs) Source #

genericZipMatchK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k). (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs) => (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: ZipLoT as bs) Source #

Generic implementation of zipMatchK.

Since: 0.2.0

genericZipMatchWithK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k). (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs) => Mappings as bs cs -> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs) Source #

Generic implementation of zipMatchWithK.

Since: 0.2.0

type ReqsZipMatch (f :: LoT k -> Type) (as :: LoT k) (bs :: LoT k) = ReqsZipMatchWith f as bs (ZipLoT as bs) Source #

What gzipMatchWith requires when the components are paired up.

Since: 0.2.0

class GZipMatch (f :: LoT k -> Type) where Source #

Matching on the Generics.Kind representation of a type, which is what the default ZipMatchK instance goes through.

Since: 0.2.0

Associated Types

type ReqsZipMatchWith (f :: LoT k -> Type) (as :: LoT k) (bs :: LoT k) (cs :: LoT k) Source #

What matching this representation requires of its components.

Since: 0.2.0

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs) Source #

Match two representations, pairing up their components with the given functions.

Since: 0.2.0

Instances

Instances details
GZipMatch (U1 :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (U1 :: LoT k -> Type) as bs cs => Mappings as bs cs -> U1 as -> U1 bs -> Maybe (U1 cs) Source #

GZipMatch (V1 :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (V1 :: LoT k -> Type) as bs cs => Mappings as bs cs -> V1 as -> V1 bs -> Maybe (V1 cs) Source #

ZipMatchFields t => GZipMatch (Field t :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (Field t) as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs) Source #

(GZipMatch f, GZipMatch g) => GZipMatch (f :*: g :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (f :*: g) as bs cs => Mappings as bs cs -> (f :*: g) as -> (f :*: g) bs -> Maybe ((f :*: g) cs) Source #

(GZipMatch f, GZipMatch g) => GZipMatch (f :+: g :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (f :+: g) as bs cs => Mappings as bs cs -> (f :+: g) as -> (f :+: g) bs -> Maybe ((f :+: g) cs) Source #

GZipMatch f => GZipMatch (c :=>: f :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (c :=>: f) as bs cs => Mappings as bs cs -> (c :=>: f) as -> (c :=>: f) bs -> Maybe ((c :=>: f) cs) Source #

(TypeError ('Text "Existentials are not supported") :: Constraint) => GZipMatch (Exists k2 f :: LoT k1 -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k1) (bs :: LoT k1) (cs :: LoT k1). ReqsZipMatchWith (Exists k2 f) as bs cs => Mappings as bs cs -> Exists k2 f as -> Exists k2 f bs -> Maybe (Exists k2 f cs) Source #

GZipMatch f => GZipMatch (M1 i c f :: LoT k -> Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k). ReqsZipMatchWith (M1 i c f) as bs cs => Mappings as bs cs -> M1 i c f as -> M1 i c f bs -> Maybe (M1 i c f cs) Source #

class ZipMatchFields (t :: Atom d Type) where Source #

Matching a single field of a constructor, by the shape of its type.

Since: 0.2.0

Associated Types

type ReqsZipMatchFieldsWith (t :: Atom d Type) (as :: LoT d) (bs :: LoT d) (cs :: LoT d) Source #

What matching this field requires.

Since: 0.2.0

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs) Source #

Match two fields, pairing up their contents.

Since: 0.2.0

Instances

Instances details
(TypeError (('Text "Atom :=>>: is not supported by ZipMatchFields" ':$$: 'Text " when attempting to use a generic instance for") ':$$: 'ShowType (c ':=>>: a)) :: Constraint) => ZipMatchFields (c ':=>>: a :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith (c ':=>>: a) as bs cs => Mappings as bs cs -> Field (c ':=>>: a) as -> Field (c ':=>>: a) bs -> Maybe (Field (c ':=>>: a) cs) Source #

(TypeError (('Text "Atom Eval is not supported by ZipMatchFields" ':$$: 'Text " when attempting to use a generic instance for") ':$$: 'ShowType ('Eval a)) :: Constraint) => ZipMatchFields ('Eval a :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ('Eval a) as bs cs => Mappings as bs cs -> Field ('Eval a) as -> Field ('Eval a) bs -> Maybe (Field ('Eval a) cs) Source #

(TypeError (('Text "Atom ForAll is not supported by ZipMatchFields" ':$$: 'Text " when attempting to use a generic instance for") ':$$: 'ShowType ('ForAll a)) :: Constraint) => ZipMatchFields ('ForAll a :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ('ForAll a) as bs cs => Mappings as bs cs -> Field ('ForAll a) as -> Field ('ForAll a) bs -> Maybe (Field ('ForAll a) cs) Source #

ZipMatchK k => ZipMatchFields ('Kon k :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ('Kon k :: Atom d Type) as bs cs => Mappings as bs cs -> Field ('Kon k :: Atom d Type) as -> Field ('Kon k :: Atom d Type) bs -> Maybe (Field ('Kon k :: Atom d Type) cs) Source #

ApplyMappings v => ZipMatchFields ('Var v :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ('Var v) as bs cs => Mappings as bs cs -> Field ('Var v) as -> Field ('Var v) bs -> Maybe (Field ('Var v) cs) Source #

(ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((('Kon k :: Atom d (Type -> Type -> Type)) ':@: t1) ':@: t2 :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ((('Kon k :: Atom d (Type -> Type -> Type)) ':@: t1) ':@: t2) as bs cs => Mappings as bs cs -> Field ((('Kon k :: Atom d (Type -> Type -> Type)) ':@: t1) ':@: t2) as -> Field ((('Kon k :: Atom d (Type -> Type -> Type)) ':@: t1) ':@: t2) bs -> Maybe (Field ((('Kon k :: Atom d (Type -> Type -> Type)) ':@: t1) ':@: t2) cs) Source #

(ZipMatchFields t, ZipMatchK k) => ZipMatchFields (('Kon k :: Atom d (Type -> Type)) ':@: t :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith (('Kon k :: Atom d (Type -> Type)) ':@: t) as bs cs => Mappings as bs cs -> Field (('Kon k :: Atom d (Type -> Type)) ':@: t) as -> Field (('Kon k :: Atom d (Type -> Type)) ':@: t) bs -> Maybe (Field (('Kon k :: Atom d (Type -> Type)) ':@: t) cs) Source #

(TypeError ((('Text "Atom :@: is not supported by ZipMatchFields is a general form:" ':$$: 'Text " when attempting to use a generic instance for") ':$$: 'ShowType (f ':@: t)) ':$$: (('ShowType f ':<>: 'Text " : ") ':<>: 'ShowType (Atom d (k1 -> Type)))) :: Constraint) => ZipMatchFields (f ':@: t :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith (f ':@: t) as bs cs => Mappings as bs cs -> Field (f ':@: t) as -> Field (f ':@: t) bs -> Maybe (Field (f ':@: t) cs) Source #

(TypeError (((('Text "The type constructor is kind-polymorphic:" ':$$: ((('Text " " ':<>: 'ShowType k) ':<>: 'Text " : ") ':<>: 'ShowType (kk -> Type))) ':$$: 'Text "Possible fix:") ':$$: 'Text " add an explicit kind signature") ':$$: ((('Text " " ':<>: 'ShowType k) ':<>: 'Text " : ") ':<>: 'ShowType (Type -> Type))) :: Constraint) => ZipMatchFields (('Kon k :: Atom d (kk -> Type)) ':@: t :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith (('Kon k :: Atom d (kk -> Type)) ':@: t) as bs cs => Mappings as bs cs -> Field (('Kon k :: Atom d (kk -> Type)) ':@: t) as -> Field (('Kon k :: Atom d (kk -> Type)) ':@: t) bs -> Maybe (Field (('Kon k :: Atom d (kk -> Type)) ':@: t) cs) Source #

(TypeError (((('Text "The type constructor is kind-polymorphic:" ':$$: ((('Text " " ':<>: 'ShowType k) ':<>: 'Text " : ") ':<>: 'ShowType (kk1 -> kk2 -> Type))) ':$$: 'Text "Possible fix:") ':$$: 'Text " add an explicit kind signature") ':$$: ((('Text " " ':<>: 'ShowType k) ':<>: 'Text " : ") ':<>: 'ShowType (Type -> Type -> Type))) :: Constraint) => ZipMatchFields ((('Kon k :: Atom d (kk1 -> kk2 -> Type)) ':@: t1) ':@: t2 :: Atom d Type) Source # 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). ReqsZipMatchFieldsWith ((('Kon k :: Atom d (kk1 -> kk2 -> Type)) ':@: t1) ':@: t2) as bs cs => Mappings as bs cs -> Field ((('Kon k :: Atom d (kk1 -> kk2 -> Type)) ':@: t1) ':@: t2) as -> Field ((('Kon k :: Atom d (kk1 -> kk2 -> Type)) ':@: t1) ':@: t2) bs -> Maybe (Field ((('Kon k :: Atom d (kk1 -> kk2 -> Type)) ':@: t1) ':@: t2) cs) Source #

Orphan instances

GenericK (,) Source # 
Instance details

Associated Types

type RepK (,) 
Instance details

Defined in Data.ZipMatchK.Generic

type RepK (,) = Field (Var0 :: Atom (Type -> Type -> Type) Type) :*: Field (Var1 :: Atom (Type -> Type -> Type) Type)

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). ((,) :@@: x) -> RepK (,) x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK (,) x -> (,) :@@: x #

GenericK NonEmpty Source # 
Instance details

Associated Types

type RepK NonEmpty 
Instance details

Defined in Data.ZipMatchK.Generic

Methods

fromK :: forall (x :: LoT (Type -> Type)). (NonEmpty :@@: x) -> RepK NonEmpty x #

toK :: forall (x :: LoT (Type -> Type)). RepK NonEmpty x -> NonEmpty :@@: x #

GenericK ((,) a :: Type -> Type) Source # 
Instance details

Associated Types

type RepK ((,) a :: Type -> Type) 
Instance details

Defined in Data.ZipMatchK.Generic

type RepK ((,) a :: Type -> Type) = Field ('Kon a :: Atom (Type -> Type) Type) :*: Field (Var0 :: Atom (Type -> Type) Type)

Methods

fromK :: forall (x :: LoT (Type -> Type)). ((,) a :@@: x) -> RepK ((,) a) x #

toK :: forall (x :: LoT (Type -> Type)). RepK ((,) a) x -> (,) a :@@: x #