Folding indexed functors with access to contextual data-CodePudding

This is a question about traversing mutually recursive data types. I am modeling ASTs for a bunch of mutually recursive datatypes using Indexed Functor as described in this gist here. This works well enough for my intended purposes.

Now I need to transform my data structure with data flowing top-down. here is an SoF question asked in the context of Functor where it's shown that the carrier of the algebra can be a function that allows one to push data down during traversal. However, I am struggling to use this technique with Indexed Functor. I think my data type needs to be altered but I am not sure how.

Here is some code that illustrates my problem. Please note, that I am not including mutually recursive types or multiple indexes as I don't need them to illustrate the issue.

setDepth should change every (IntF n) to (IntF depth). The function as written won't type check because kind ‘AstIdx -> *’ doesn't match ‘Int -> Expr ix’. Maybe I am missing something but I don't see a way to get around this without relaxing the kind of f to be less restrictive in IxFunctor but that seems wrong.

Any thoughts, suggestions or pointers welcome!

{-# LANGUAGE PolyKinds #-}

infixr 5 ~>

type f ~> g = forall i. f i -> g i

class IxFunctor (f :: (k -> *) -> k -> *) where
  imap :: (a ~> b) -> (f a ~> f b)

-- Indexed Fix
newtype IxFix f ix = IxIn {ixout :: f (IxFix f) ix}

-- Fold
icata :: IxFunctor f => (f a ~> a) -> (IxFix f ~> a)
icata phi = phi . imap (icata phi) . ixout

-- Kinds of Ast
data AstIdx = ExprAst | TypeAst

-- AST
data ExprF (f :: AstIdx -> *) (ix :: AstIdx) where
  IntF :: Int -> ExprF f ExprAst
  AddF :: f ExprAst -> f ExprAst -> ExprF f ExprAst

type Expr = IxFix ExprF

instance IxFunctor ExprF where
  imap f (IntF n) = IntF n
  imap f (AddF a b) = AddF (f a) (f b)

-- Change (IntF n) to (IntF (n   1)).
add1 :: Expr ix -> Expr ix
add1 e = icata go e
  where
    go :: ExprF Expr ix -> Expr ix
    go (IntF n) = IxIn (IntF (n   1))
    go (AddF a b) = IxIn (AddF a b)

{-
-- Change (IntF n) to (IntF depth)
-- Doesn't type check
setDepth :: Expr ix -> Expr ix
setDepth e = icata ((flip go) 0) e
  where
    --  byDepthF :: TreeF a (Integer -> Tree Integer) -> Integer -> Tree Integer
    --  byDepthF :: TreeF a (Integer -> Tree Integer) -> Integer -> Tree Integer ix
    go :: ExprF (Int -> Expr ix) ix -> Int -> Expr ix
    go (IntF n) d = IxIn (IntF d)
    go (AddF a b) d = IxIn (AddF (a d) (b d))
-}

CodePudding user response：

I'm assuming here that you're trying to set each IntF node to its depth within the tree (like the byDepthF function from the linked question) rather than to some fixed integer argument named depth.

If so, I think you're probably looking for something like the following:

newtype IntExpr ix = IntExpr { runIntExpr :: Int -> Expr ix }

setDepth :: Expr ix -> Expr ix
setDepth e = runIntExpr (icata go e) 0
  where
    go :: ExprF IntExpr ix -> IntExpr ix
    go (IntF n) = IntExpr (\d -> IxIn (IntF d))
    go (AddF a b) = IntExpr (\d -> IxIn (AddF (runIntExpr a (d 1)) (runIntExpr b (d 1)))

That is, you need to define a newtype that serves as the indexed first type parameter to ExprF, passing the index through the Int -> reader. The rest is just wrapping and unwrapping.