Using fold-interpreter on GADT

Question

Several weeks ago, I read Writing an interpreter using fold. I tried to apply this method on the project I am working on, but there was a errors because of GADTs. Here is the toy code that generates same problem.

{-# LANGUAGE GADTs, KindSignatures #-} 


data Expr :: * -> * where
    Val  :: n ->                Expr n
    Plus :: Expr n -> Expr n -> Expr n

data Alg :: * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg a

fold :: Alg a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

Here is the error message.

/home/mossid/Code/Temforai/src/Temforai/Example.hs:16:36: error:
    • Couldn't match expected type ‘n1’ with actual type ‘n’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          fold :: forall a n. Alg a -> Expr n -> a
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:15:9
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          Alg :: forall a n. (n -> a) -> (a -> a -> a) -> Alg a,
        in an equation for ‘fold’
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:11
    • In the first argument of ‘val’, namely ‘n’
      In the expression: val n
      In an equation for ‘fold’: fold alg@(Alg val _) (Val n) = val n
    • Relevant bindings include
        n :: n
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:27)
        val :: n1 -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:15)
        fold :: Alg a -> Expr n -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:1)

I think the compiler cannot deduce that the n and n1 are same types, so the answer might be lifting inner variable to the signature of data type. However, not like in this example, it cannot be used on the original code. The original code is having forall-quantified type variable in Expr, and the type signature must handle specific information.

+ Here is the original code

data Form :: * -> * where
    Var     :: Form s
    Prim    :: (Sat s r) => Pred s -> Marker r          -> Form s
    Simple  :: (Sat s r) => Pred s -> Marker r          -> Form s
    Derived ::              Form r -> Suffix r s        -> Form s
    Complex :: (Sat s r, Sat t P) => 
                            Form s -> Infix r -> Form t -> Form s

data FormA a where
    FormA :: (Pred s -> Marker t -> a) 
          -> (Pred u -> Marker v -> a)
          -> (a -> Suffix w x    -> a)
          -> (a -> y -> a        -> a)
          -> FormA a

foldForm :: FormA a -> Form s -> a
foldForm alg@(FormA prim _ _ _) (Prim p m) = prim p m
foldForm alg@(FormA _ simple _ _) (Simple p m) = simple p m
foldForm alg@(FormA _ _ derived _) (Derived f s) = 
    derived (foldForm alg f) s
foldForm alg@(FormA _ _ _ complex) (Complex f1 i f2) = 
    complex (foldForm alg f1) i (foldForm alg f2)

The proper definition is Alg :: (n -> a) -> ... -> Alg n a - the type exists n . n -> a is isomorphic to a since the only thing you can do with a function is apply it, but you know nothing about the type n, so you can only apply this function to undefined. But it seems like you are aware of this - "so the answer might be lifting inner variable to the signature of data type". "However, not like in this example, it cannot be used on the original code" - then it is the original code you should post. — user2407038

chi chi · Accepted Answer · 2017-02-18T09:52:26

To ensure the n inside Alg is the right one, you can expose it as a parameter to the Alg type constructor.

data Alg :: * -> * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg n a

fold :: Alg n a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

In the Form code, this looks harder. There are a lot of existentially-quantified type variables there. One needs to find a way to expose all of them in the type, so that they can be required to be the same in Form and FormA.

Using fold-interpreter on GADT

1 Answers