Search code examples
haskellgadtuniplate

How can holes and contexts be implemented for higher-kinded types in a lens style uniplate library?


András Kovács proposed this question in response to an answer to a previous question.

In a lens-style uniplate library for types of kind * -> * based on the class

class Uniplate1 f where
    uniplate1 :: Applicative m => f a -> (forall b. f b -> m (f b)) -> m (f a)

analogous to the class for types of kind *

class Uniplate on where
    uniplate :: Applicative m => on -> (on -> m on) -> m on

is it possible to implement analogs to contexts and holes, which both have the type Uniplate on => on -> [(on, on -> on)] without requiring Typeable1?

It's clear that this could be implemented in the old-style of the uniplate library which used Str to represent the structure of the data by returning a structure with a type-level list of the types of the children.

A hole could be represented by the following data type, which would replace (on, on -> on) in the signatures for contexts and holes

data Hole f a where
    Hole :: f b -> (f b -> f a) -> Hole f a

holes :: Uniplate1 f => f a -> [Hole f a]
...

However, it is unclear if there is an implementation for holes which doesn't require Typeable1.


Solution

  • The suggested type Hole is needlessly restrictive in the return type of the function. The following type can represent everything the former Hole represents, and more, without loss of any type information.

    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE GADTs #-}
    
    data Hole f a where
        Hole :: f b -> (f b -> a) -> Hole f a
    

    If we need to have a return type of f a, we can use Hole f (f a) to represent it. Since we will be using Holes a lot, it'd be nice to have a few utility functions. Because the return type of the function in Hole is no longer constrained to be in f, we can make a Functor instance for it

    instance Functor (Hole f) where
        fmap f (Hole b g) = Hole b (f . g)
    

    contexts1 can be written for either version of Hole by replacing the constructors for tuples in the uniplate library's contexts with Hole:

    contexts1 :: Uniplate1 f => f a -> [Hole f (f a)]
    contexts1 x = Hole x id  : f (holes1 x)
        where    
            f xs = [ Hole y (ctx . context)
                   | Hole child ctx <- xs
                   , Hole y context <- contexts1 child]
    

    holes1 is trickier, but can still be made by modifying holes from the uniplate library. It requires a new Replace1 Applicative Functor that uses Hole instead of a tuple. Everyhwere the second field of the tuple was modified by second (f .) we replace with fmap f for the Hole.

    data Replace1 f a = Replace1 {replaced1 :: [Hole f a], replacedValue1 :: a}
    
    instance Functor (Replace1 f) where
        fmap f (Replace1 xs v) = Replace1 (map (fmap f) xs) (f v)
    
    instance Applicative (Replace1 f) where
        pure v = Replace1 [] v
        Replace1 xs1 f <*> Replace1 xs2 v = Replace1 (ys1 ++ ys2) (f v)
            where ys1 = map (fmap ($ v)) xs1
                  ys2 = map (fmap (f)) xs2
    
    holes1 :: Uniplate1 f => f a -> [Hole f (f a)]
    holes1 x = replaced1 $ descendM1 (\v -> Replace1 [Hole v id] v) x
    

    decendM1 is defined in the preceding answer. Replace and Replace1 can be unified; how to do so is described after the examples.

    Let's try some examples in terms of the code in the previous question. The following utility functions on Holes will be useful.

    onHole :: (forall b. f b -> c) -> Hole f a -> c
    onHole f (Hole x _) = f x
    
    inHole :: (forall b. f b -> f b) -> Hole f a -> a
    inHole g (Hole x f) = f . g $ x
    

    Examples

    We'll use the following example data and function, based on the code from the preceding questions:

    example = If (B True) (I 2 `Mul` I 3) (I 1)
    
    zero :: Expression b -> Expression b
    zero x = case x of
        I _ -> I 0
        B _ -> B False
        Add _ _ -> I 0
        Mul _ _ -> I 0
        Eq  _ _ -> B False
        And _ _ -> B False
        Or  _ _ -> B False
        If  _ a _ -> zero a
    

    Holes

    sequence_ . map (onHole print) . holes1 $ example
    
    B True
    Mul (I 2) (I 3)
    I 1
    

    Contexts

    sequence_ . map (onHole print) . contexts1 $ example
    
    If (B True) (Mul (I 2) (I 3)) (I 1)
    B True
    Mul (I 2) (I 3)
    I 2
    I 3
    I 1
    

    Replacement of each context

    sequence_ . map print . map (inHole zero) . contexts1 $ example
    
    I 0
    If (B False) (Mul (I 2) (I 3)) (I 1)
    If (B True)  (I 0)             (I 1)
    If (B True)  (Mul (I 0) (I 3)) (I 1)
    If (B True)  (Mul (I 2) (I 0)) (I 1)
    If (B True)  (Mul (I 2) (I 3)) (I 0)
    

    Unifying Replace

    The Replace Applicative Functor can be refactored so that it doesn't know about the type of holes for either Uniplate or Uniplate1, and instead only knows that the hole is a Functor. Holes for Uniplate were using the type (on, on -> a) and essentially using fmap f = second (f .); this is the composition of the (on, ) and on-> functors.

    Instead of grabbing Compose from the transformers library, we'll make a new type for a Hole for Uniplate, which will make the example code here be more consistent and self-contained.

    data Hole on a = Hole on (on -> a)
    
    instance Functor (Hole on) where
        fmap f (Hole on g) = Hole on (f . g)
    

    We'll rename our Hole from before to Hole1.

    data Hole1 f a where
        Hole1 :: f b -> (f b -> a) -> Hole1 f a
    
    instance Functor (Hole1 f) where
        fmap f (Hole1 b g) = Hole1 b (f . g)
    

    Replace can drop all knowledge of either type of hole.

    data Replace f a = Replace {replaced :: [f a], replacedValue :: a}
    
    instance Functor f => Functor (Replace f) where
        fmap f (Replace xs v) = Replace (map (fmap f) xs) (f v)
    
    instance Functor f => Applicative (Replace f) where
        pure v = Replace [] v
        Replace xs1 f <*> Replace xs2 v = Replace (ys1 ++ ys2) (f v)
            where ys1 = map (fmap ($ v)) xs1
                  ys2 = map (fmap (f)) xs2
    

    Both holes and holes1 can be implemented in terms of the new Replace.

    holes :: Uniplate on => on -> [Hole on on]
    holes x = replaced $ descendM (\v -> Replace [Hole v id] v) x
    
    holes1 :: Uniplate1 f => f a -> [Hole1 f (f a)]
    holes1 x = replaced $ descendM1 (\v -> Replace [Hole1 v id] v) x