Generics.MRSOP.Holes

Annotating a Mutually Recursive Family with Holes

It is often the case that we must perform some sort of symbolic processing over our datatype. Take unification for example. For that to work, we must either have a dedicated constructor in the datatype for representing a metavariable, which would be difficult to access in a generic fashion, or we must augment the definition an add those.

In this module we provide the Holes datatype, which enables this very functionality. Imagine the following family:

data Exp     = Add Exp Exp | Let Decls Exp | Var Exp
data Decls   = Decl VarDecl Decls | Empty
data VarDecl = VarD String Exp

The values that inhabit the type Holes ki FamExp phi are essentially isomorphic to:

data Exp'     = Add Exp' Exp' | Let Decls' Exp' | Var Exp' | EHole (phi IdxExp)
data Decls'   = Decl VarDecl' Decls' | Empty | DHole (phi IdxDecls)
data VarDecl' = VarD String Exp' | VHole (phi IdxVarDecl)

If we want to, say, forbid holes on the declaration bit, we can do so in the definition of phi. For example:

data OnlyExpAndVarHoles :: Atom kon -> * where
  ExpHole :: OnlyExpAndVarHoles ('I IdxExp)
  VarHole :: OnlyExpAndVarHoles ('I IdxVar)

data HolesAnn :: (Atom kon -> *) -> (kon -> *) -> [[[Atom kon]]] -> (Atom kon -> *) -> Atom kon -> * where

A value of type HolesAnn augments a mutually recursive family with holes. This is useful for writing generic unification-like algorithms.

Essentially, we have the following isomorphism:

Holes ann ki codes phi at
  =~= (ann at :*: (phi :+: NA ki (Rep ki (Holes ann ki codes phi))))

That is, we are extending the representations with values of type phi, and adding annotations of type ann at everywhere. A simpler variant of this type is given in Holes, where the annotationsare defaulted to Const ()

The annotations are ignored in most of the functions and are here only as a means of helping algorithms keep intermediate values directly in the datatype. They have no semantic meaning.

Note that HolesAnn ann ki codes, of kind (Atom kon -> *) -> Atom kon -> * forms an indexed free monad.

Constructors

Hole :: ann at -> phi at -> HolesAnn ann ki codes phi at

A "hole" contains something of type phi

HOpq :: ann (K k) -> ki k -> HolesAnn ann ki codes phi (K k)

An opaque value

HPeel :: (IsNat n, IsNat i) => ann (I i) -> Constr (Lkup i codes) n -> NP (HolesAnn ann ki codes phi) (Lkup n (Lkup i codes)) -> HolesAnn ann ki codes phi (I i)

A view over a constructor with its fields replaced by treefixes. This already comes in a SOP flavour.

Instances

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f) => ShowHO (Holes ki codes f :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

showHO :: Holes ki codes f k -> String

(EqHO phi, EqHO ki) => EqHO (Holes ki codes phi :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

eqHO :: Holes ki codes phi k -> Holes ki codes phi k -> Bool

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f, ShowHO ann) => ShowHO (HolesAnn ann ki codes f :: Atom kon -> Type)

Defined in Generics.MRSOP.Holes

Methods

showHO :: HolesAnn ann ki codes f k -> String

(EqHO phi, EqHO ki) => Eq (Holes ki codes phi ix)

Defined in Generics.MRSOP.Holes

Methods

(==) :: Holes ki codes phi ix -> Holes ki codes phi ix -> Bool

(/=) :: Holes ki codes phi ix -> Holes ki codes phi ix -> Bool

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f) => Show (Holes ki codes f at)

Defined in Generics.MRSOP.Holes

Methods

showsPrec :: Int -> Holes ki codes f at -> ShowS

show :: Holes ki codes f at -> String

showList :: [Holes ki codes f at] -> ShowS

(HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f, ShowHO ann) => Show (HolesAnn ann ki codes f at)

Defined in Generics.MRSOP.Holes

Methods

showsPrec :: Int -> HolesAnn ann ki codes f at -> ShowS

show :: HolesAnn ann ki codes f at -> String

showList :: [HolesAnn ann ki codes f at] -> ShowS

holesAnn :: HolesAnn ann ki codes phi at -> ann at

Extracts the annotation from the topmost HolesAnn constructor.

Mapping Over HolesAnn

holesMapAnnM

Arguments

:: Monad m

=> (forall a. f a -> m (g a))

Function to map over holes

-> (forall a. ann a -> m (bnn a))

Function to map over annotations

-> HolesAnn ann ki codes f at

-> m (HolesAnn bnn ki codes g at)

Our HolesAnn is a higher order functor and can be mapped over.

holesMapM :: Monad m => (forall a. f a -> m (g a)) -> HolesAnn ann ki codes f at -> m (HolesAnn ann ki codes g at)

Maps over the index part, not the annotation

holesMapAnn :: (forall a. f a -> g a) -> (forall a. ann a -> ann' a) -> HolesAnn ann ki codes f at -> HolesAnn ann' ki codes g at

Non-monadic version of holesMapM

holesMap :: (forall a. f a -> g a) -> HolesAnn ann ki codes f at -> HolesAnn ann ki codes g at

Non-monadic version of holesMapM

holesJoin :: HolesAnn ann ki codes (HolesAnn ann ki codes f) at -> HolesAnn ann ki codes f at

Since HolesAnn is just a free monad, we can join them!

Extracting Annotations and HolesAnn from HolesAnn

holesGetHolesAnnWith

Arguments

:: f r

Empty structure

-> (r -> f r -> f r)

Insertion function

-> (forall ix. phi ix -> r)

How to get rid of the existential type

-> HolesAnn ann ki codes phi at

-> f r

Returns the set of holes in a value of type HolesAnn. The _getter_ argument is there to handle the existantial type index present in the holes and the insertion function is used to place the holes in a datastructure of choice. The treefix is taversed in a pre-order style and the holes inserted in the sturcture as they are visited.

holesGetHolesAnnWith' :: (forall ix. phi ix -> r) -> HolesAnn ann ki codes phi at -> [r]

Instantiates holesGetHolesAnnWith to use a list. It's implementation is trivial:

holesGetHolesAnnWith' = holesGetHolesAnnWith [] (:)

holesGetHolesAnnWith'' :: Ord r => (forall ix. phi ix -> r) -> HolesAnn ann ki codes phi at -> Set r

Instantiates holesGetHolesAnnWith to use a set instead of a list.

Refining HolesAnn

holesRefineAnnM :: Monad m => (forall ix. ann ix -> f ix -> m (HolesAnn ann ki codes g ix)) -> (forall k. ann (K k) -> ki k -> m (HolesAnn ann ki codes g (K k))) -> HolesAnn ann ki codes f at -> m (HolesAnn ann ki codes g at)

Similar to holesMapM, but allows to refine the structure of a treefix if need be. One could implement holesMapM as:

holesMapM f = holesRefineAnn (\a h -> Hole a <$> f h) HOpq'

holesRefineVarsM

Arguments

:: Monad m

=> (forall ix. ann ix -> f ix -> m (HolesAnn ann ki codes g ix))

How to produce a HolesAnn from the previous hole.

-> HolesAnn ann ki codes f at

-> m (HolesAnn ann ki codes g at)

Just like holesRefineM, but only refines variables. One example is to implement holesJoin with it.

holesJoin = runIdentity . holesRefineVarsM (\_ -> return)

holesRefineAnn

Arguments

:: (forall ix. ann ix -> f ix -> HolesAnn ann ki codes g ix)

-> (forall k. ann (K k) -> ki k -> HolesAnn ann ki codes g (K k))

-> HolesAnn ann ki codes f at

-> HolesAnn ann ki codes g at

Pure version of holesRefineM

Annotation Catamorphism and Synthesized Attributes

holesAnnCataM

Arguments

:: Monad m

=> (forall at. ann at -> phi at -> m (res at))

Action to perform at Hole

-> (forall k. ann (K k) -> ki k -> m (res (K k)))

Action to perform at HOpq

-> (forall i n. (IsNat i, IsNat n) => ann (I i) -> Constr (Lkup i codes) n -> NP res (Lkup n (Lkup i codes)) -> m (res (I i)))

Action to perform at HPeel

-> HolesAnn ann ki codes phi ix

-> m (res ix)

Standard monadic catamorphism for holes. The algebra can take the annotation into account.

holesAnnCata

Arguments

:: (forall at. ann at -> phi at -> res at)

Action to perform at Hole

-> (forall k. ann (K k) -> ki k -> res (K k))

Action to perform at HOpq

-> (forall i n. (IsNat i, IsNat n) => ann (I i) -> Constr (Lkup i codes) n -> NP res (Lkup n (Lkup i codes)) -> res (I i))

Action to perform at HPeel

-> HolesAnn ann ki codes phi ix

-> res ix

Pure variant of holesAnnCataM

holesSynthesizeM

Arguments

:: Monad m

=> (forall at. ann at -> phi at -> m (res at))

Action to perform at Hole

-> (forall k. ann (K k) -> ki k -> m (res (K k)))

Action to perform at HOpq

-> (forall i n. (IsNat i, IsNat n) => ann (I i) -> Constr (Lkup i codes) n -> NP res (Lkup n (Lkup i codes)) -> m (res (I i)))

Action to perform at HPeel

-> HolesAnn ann ki codes phi atom

Input value

-> m (HolesAnn res ki codes phi atom)

Synthesizes attributes over a value of type HolesAnn. This is extremely useful for easily annotating a value with auxiliar annotations.

holesSynthesize

Arguments

:: (forall at. ann at -> phi at -> res at)

-> (forall k. ann (K k) -> ki k -> res (K k))

-> (forall i n. (IsNat i, IsNat n) => ann (I i) -> Constr (Lkup i codes) n -> NP res (Lkup n (Lkup i codes)) -> res (I i))

-> HolesAnn ann ki codes phi ix

-> HolesAnn res ki codes phi ix

Pure variant of holesSynthesize

Using Holes with no annotations

type Holes = HolesAnn (Const ())

Ignoring the annotations is easy; just use Const ()

pattern Hole' :: phi at -> Holes ki codes phi at

pattern HOpq' :: ki k -> Holes ki codes phi (K k)

pattern HPeel' :: () => (IsNat n, IsNat i) => Constr (Lkup i codes) n -> NP (Holes ki codes phi) (Lkup n (Lkup i codes)) -> Holes ki codes phi (I i)

holesLCP :: EqHO ki => Holes ki codes f at -> Holes ki codes g at -> Holes ki codes (Holes ki codes f :*: Holes ki codes g) at

Factors out the largest common prefix of two treefixes. This is also known as the anti-unification of two treefixes.

It enjoys naturality properties with holesJoin:

 holesJoin (holesMap fst (holesLCP p q)) == p
 holesJoin (holesMap snd (holesLCP p q)) == q

We use a function to combine annotations in case it is necessary.

Translating between NA and HolesAnn

na2holes :: NA ki (Fix ki codes) at -> HolesAnn (Const ()) ki codes f at

A stiff treefix is one with no holes anywhere.

holes2naM

Arguments

:: Monad m

=> (forall ix. f ix -> m (NA ki (Fix ki codes) ix))

-> Holes ki codes f at

-> m (NA ki (Fix ki codes) at)

Reduces a treefix back to a tree; we use a monadic function here to allow for custom failure confitions.

holesArity :: HolesAnn ann ki codes f at -> Int

Returns how many holes are inside a treefix

holesSize :: HolesAnn ann ki codes f at -> Int

Returns the size of a treefix. Holes have size 0.

holesSNat :: IsNat ix => HolesAnn ann ki codes f (I ix) -> SNat ix

Returns the singleton identifying the index of a HolesAnn

holesShow :: forall ki ann f fam codes ix. (HasDatatypeInfo ki fam codes, ShowHO ki, ShowHO f) => Proxy fam -> (forall at. ann at -> ShowS) -> HolesAnn ann ki codes f ix -> ShowS