Use Data.Fix to make the recursion of Expr explicit

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

I'm thinking of one task that might lie ahead for you. It's to generalize the expression syntax tree. So far, it has four type parameters: the encoding of names, the type system (so far I handle multi-sorted first order, because of Z3, and polymorphic ML type, for the reasoning in the specification and also no type system), the type annotation (similar to the type system) and quantifier type (first order (without lambdas, sums, etc) and higher order (with lambdas, etc))

I would like to add one degree of flexibility. I would like to use Data.Fix to handle the recursion of expression trees explicitly. If I simplify the expression tree,

data Expr = Var VarName | FunApp FunName Expr

would become

data Expr' expr = Var VarName | FunApp FunName expr type Expr = Fix Expr'

The new version of Expr would be isomorphic to the old one (i.e. it contains the same information) but now Expr' is more flexible. We can use it to create expression trees with holes waiting to be filled:

type ExprWithHole = Fix (Compose Maybe Expr') -- (Compose Maybe Expr' a) is isomorphic to Maybe (Expr' a) -- the difference is that in Compose Maybe Expr' a the last -- type parameter is 'a' while in Maybe (Expr' a) the last type -- parameter is Expr a.

In the above, every subexpression is basically optional: you can fill them up with 'Nothing' if you have a procedure that will fill them up later. For example, we could imagine a monadic action on an ExprWithHole as "fillHoles":

fillHoles :: Monad m => (Maybe Expr -> m Expr) -> (ExprWithHoles -> m Expr) What really interests me about this type definition is adding LineInfo to the nodes of an expression tree. This way, when we do type checking, we can generate exact messages about which expression and subexpressions are badly typed and output the line info of the beginning and end of the problematic subexpressions.

It would be defined as:

type ExprLI = Fix (Compose ((,,) LineInfo LineInfo) Expr') -- ((,,) LineInfo LineInfo) is the type of triples applied to two arguments, -- which leaves one argument open to be filled by a subexpression.

It is not urgent as my current approach can still serve for the moment. What I currently do is render problematic expressions as S-expressions (as if I would feed them to Z3). It's not the best but it's ok. The task is not easy so you can start thinking about how you would do it and get started only when you feel ready.

Bitbucket: https://bitbucket.org/literateunitb/literate-unitb/issue/6

unitb / literate-unitb

Use Data.Fix to make the recursion of Expr explicit #6