Associated Labeled AST

Question

I have been trying to create tagged AST for a while. Let's look at the problem:

data E a = V a | LitInt Int | LitBool Bool | FooIntBool (E a) (E a) -- er… deriving (Eq,Show) 

The problem with this code, for me, is in FooIntBool . The idea is that it takes an int expression and a bool expression and glues them together. But E a can be anything. This would be true given the above definition of E :

 FooIntBool (LitInt 3) (LitInt 0) 

You can see this problem. Then what do we want? Tag expression. This is not possible given the current definition of E, so let's introduce some GADTs:

 data E :: * -> * -> * where V :: a -> E la LitInt :: Int -> E Int a LitBool :: Bool -> E Bool a FooIntBool :: E Int a -> E Bool a -> E (Int,Bool) a 

It is very nice! Now I can fix this code:

 FooIntBool (V "x") (LitBool False) 

The problem is when I want to make it a monad or applicative. It is simply not possible. Consider the implementation of the monad:

 instance Monad (E l) where return = V 

It was obvious and straightforward. Let's look at the implementation of the binding:

  V x >>= f = fx -- obvious as well LitInt a >>= _ = LitInt a -- obvious yeah LitBool a >>= _ = LitBool a -- … FooIntBool ab >>= f = FooIntBool (a >>= ?) (b >>= ?) -- AH? 

We cannot write a >>= f and b >>= f , since f :: a -> E lb I have not yet found a solution to this problem, and I am very curious how to deal with it and you can still use the Bruijn indices (via binding).

Answer 1

I think your typed AST is unlikely to work the way you want. The fact that the variables are untyped will be painful. Try to imagine what it would be like to write an interpreter with the environment; you will need to look for variables in the environment, and not cast the results to the correct types or crash with an error. Therefore, I am going to propose a slightly different AST with typed variables and an inexplicable reordering of type parameters.

 data E va where V :: va -> E va LitInt :: Int -> E v Int LitBool :: Bool -> E v Bool FooIntBool :: E v Int -> E v Bool -> E v (Int, Bool) 

Now, as far as I know, it is impossible to determine the regular instance of Monad for this. Note that type E is equal to (* -> *) -> * -> * ; for our purposes it may be more understandable to consider (* -> *) -> (* -> *) . This is superficially compatible with what Monad expects * -> * , at least if you partially apply E to some v , but then the types get weird. I believe that you already know about this, so you put your parameter type variable last; the intended effect of this is that (>>=) will be a substitution. However, if we did this with this new type that I proposed, it is not compatible with Monad at all.

There is another form of monad that can work. We can generalize its form from * -> * to (k -> *) -> (k -> *) (where k in this case is just * ). Once again, I used parentheses to emphasize that, like most instances of Monad , E , should be considered as a unary type constructor. We will work with natural transformations, not with any old Haskell function:

 type a ~> b = forall x. ax -> bx 

(By the way, type (~>) is (k -> *) -> (k -> *) -> * .)

To build our new class like HMonad , we can simply copy Monad and replace (->) with (~>) . One complication is that we need to reverse the order of the arguments (>>=) to make the types:

 class HMonad m where hreturn :: a ~> ma hbind :: (a ~> mb) -> (ma ~> mb) 

I will just show you an instance of HMonad for E , and then try to explain it:

 instance HMonad E where hreturn = V hbind fe = case e of V v -> fv LitInt x -> LitInt x LitBool x -> LitBool x FooIntBool ab -> FooIntBool (hbind fa) (hbind fb) 

Actually, it looks exactly like the Monad example for an untyped version of AST. Note that, as expected, hreturn simply enters a variable, and hbind does some sort of safe type substitution by looking for variables and applying a function to them. This works due to higher types of ranks.

You cannot do this with a bundled package, because instead of> it uses Monad . It is possible (and even done several times) to write a version of the binding that works for typed ASTs like this, but it's unclear if it really costs.

Answer 2

If you really want to, you can write a typed instance of Monad . I have not tested whether this complies with the laws of the monad.

 instance Monad (E l) where return = VV x >>= f = fx LitInt a >>= _ = LitInt a LitBool a >>= _ = LitBool a FooIntBool ab >>= f = FooIntBool (a >>= qf) (b >>= rf) where q :: E (Int, Bool) t -> E Int t q (V x) = V xq (FooIntBool x _) = x r :: E (Int, Bool) t -> E Bool t r (V x) = V xr (FooIntBool _ x) = x