Responding to:
Like recursion-schemes, I want a way to construct ASTs, except I want my ASTs to be able to refer to each other - that is a term can contain a type (for a lambda parameter), a type can contain a row-type in it and vice-versa. I'd like the ASTs to be defined with an external fix-point (so one can have "pure" expressions or ones annotated with types after type inference), but I also want these fix-points to be able to contain other types of fix-points (just like terms can contain terms of different types). I don't see how Fix helps me there
I have a method, which maybe is near what you are asking for, that I have been experimenting with. It seems to be quite powerful, though the abstractions around this construction need some development. The key is that there is a kind Label
which indicates from where the recursion will continue.
{-# LANGUAGE DataKinds #-}
import Data.Kind (Type)
data Label = Label ((Label -> Type) -> Type)
type L = 'Label
L
is just a shortcut to construct labels.
Open-fixed-point definitions are of kind (Label -> Type) -> Type
, that is, they take a "label interpretation (type) function" and give back a type. I called these "shape functors", and abstractly refer to them with the letter h
. The simplest shape functor is one that does not recurse:
newtype LiteralF a f = Literal a -- does not depend on the interpretation f
type Literal a = L (LiteralF a)
Now we can make a little expression grammar as an example:
data Expr f
= Lit (f (Literal Integer))
| Let (f (L Defn)) (f (L Expr))
| Var (f (L String))
| Add (f (L Expr)) (f (L Expr))
data Defn f
= Defn (f (Literal String)) (f (L Expr))
Notice how we pass labels to f
, which is in turn responsible for closing off the recursion. If we just want a normal expression tree, we can use Tree
:
data Tree :: Label -> Type where
Tree :: h Tree -> Tree (L h)
Then a Tree (L Expr)
is isomorphic to the normal expression tree you would expect. But this also allows us to, e.g., annotate the tree with a label-dependent annotation at each level of the tree:
data Annotated :: (Label -> Type) -> Label -> Type where
Annotated :: ann (L h) -> h (Annotated ann) -> Annotated ann (L h)
In the repo ann
is indexed by a shape functor rather than a label, but this seems cleaner to me now. There are a lot of little decisions like this to be made, and I have yet to find the most convenient pattern. The best abstractions to use around shape functors still needs exploration and development.
There are many other possibilities, many of which I have not explored. If you end up using it I would love to hear about your use case.