Could not deduce (b ~ a)

Question

So I have the following code, I'm trying to write an abstract syntax tree for an interpreter, & I prefer not to jam everything in the same data type, so I was going to write a typeclass that had the basic behaviour (in this case AST).

{-# LANGUAGE ExistentialQuantification #-}

import qualified Data.Map as M

-- ...    

data Expr = forall a. AST a => Expr a
type Env = [M.Map String Expr]

class AST a where
  reduce :: AST b => a -> Env -> b
  -- when i remove the line below, it compiles fine
  reduce ast _ = ast 

-- ...

When I remove the default implementation of reduce in the typeclass AST it compiles fine, but when ever I provide an implementation that returns it's self it complains. I get the following compiler error

src/Data/AbstractSyntaxTree.hs:13:18:
  Could not deduce (b ~ a)
  from the context (AST a)
    bound by the class declaration for `AST'
    at src/Data/AbstractSyntaxTree.hs:(11,1)-(13,20)
  or from (AST b)
    bound by the type signature for reduce :: AST b => a -> Env -> b
    at src/Data/AbstractSyntaxTree.hs:12:13-36
    `b' is a rigid type variable bound by          
        the type signature for reduce :: AST b => a -> Env -> b
        at src/Data/AbstractSyntaxTree.hs:12:13
    `a' is a rigid type variable bound by
        the class declaration for `AST'
        at src/Data/AbstractSyntaxTree.hs:11:11
  In the expression: ast
  In an equation for `reduce': reduce ast _ = ast

The behaviour of AST's reduce will evaluate an AST, and occasionally return a different type of AST, and sometimes the same type of AST.

Edit: Regarding data Expr = forall a. AST a => Expr a & GADTs

I originally went with data Expr = forall a. AST a => Expr a because I wanted to represent types like this.

(+ 2 true) -> Compound [Expr (Ref "+"), Expr 2, Expr true]

(+ a 2) -> Compound [Expr (Ref "+"), Expr (Ref "a"), Expr 2]

(eval (+ 2 2)) -> Compound [Expr (Ref "eval"), 
                     Compound [
                       Expr (Ref "+"), 
                       Expr 2, 
                       Expr 2]]

((lambda (a b) (+ a b)) 2 2) -> Compound [Expr SomeLambdaAST, Expr 2, Expr 2]

Since I'm generating ASTs from text I feel it would be a burden to represent a strictly typed ASTs in a GADT, although I do see where they could be useful in case like DSLs in Haskell.

But since I'm generating the AST from text (which could contain some of the examples above), it might be a bit hard to predict what AST I'll end up with. I don't want to start juggling between Eithers & Maybes. That is what I ended up doing last time & it was a mess, & I gave up trying to attempt this in Haskell.

But again I'm not the most experienced Haskell programmer so maybe I'm looking at this the wrong way, maybe I can implement an AST with so more rigours typing, so I'll have a look and see if I can come up with GADTs, but I have my doubts & I have a feeling that it might end the way it did last time.

Ultimately I'm just trying to learn Haskell at the moment with a fun finish able project, so I don't mind if my first Haskell project isn't really idiomatic Haskell. Getting something working is a higher priority just so I can make my way around the language and have something to show for it.

Update:

I've taken @cdk's & @bheklilr advice and ditched the existential type, although I've gone with a much simpler type, as opposed to utilising GADTs (also suggested by @cdk's & @bheklilr). It could possibly be a stronger type but again I'm just trying to get familiar with Haskell, so I gave up up after a few hours & went with a simple data type like so :P

import qualified Data.Map as M

type Environment = [M.Map String AST]

data AST
  = Compound [AST]
  | FNum Double
  | Func Function
  | Err  String
  | Ref  String

data Function
  = NativeFn ([AST] -> AST)
  | LangFn   [String] AST

-- previously called reduce
eval :: Environment -> AST -> AST
eval env ast = case ast of
  Ref ref -> case (lookup ref env ) of
    Just ast -> ast
    Nothing  -> Err ("Not in scope `" ++ ref ++ "'")

  Compound elements -> case elements of
    []              -> Err "You tried to invoke `()'"
    function : args -> case (eval env function) of
      Func fn -> invoke env fn args
      other   -> Err $ "Cannot invoke " ++ (show other)

  _ -> ast

-- invoke & lookup are defined else where 

Although I will still probably look at GADTs as they seem to be pretty interesting & have lead me to some interesting reading material regarding implementing abstract syntax trees in haskell.

Answer 1

What part of the error message are you having difficulties understanding? I think it's quite clear.

The type of reduce is

reduce :: AST b => a -> Env -> b

The first argument has type a and GHC expects reduce to return something of type b, which may be entirely different from a. GHC is correct to complain that you've tried to return a value of a when it expects b.

The "existential quantification with type class" is (as noted by bheklilr) an anti-pattern. A better approach would be to create an Algebraic Data Type for AST:

data AST a

now reduce becomes a simple function:

reduce :: Env -> AST a -> AST b

if you want reduce to be able to return a different type of AST, you could use Either

reduce :: Env -> AST a -> Either (AST a) (AST b)

but I don't think this is what you really want. My advice is to take a look at the GADT style of creating ASTs and re-evaluate your approach.

Answer 2

You are interpreting this type signature incorrectly (in a way that is common to OO programmers):

reduce :: AST b => a -> Env -> b

This does not mean that reduce can choose any type it likes (that is a member of AST) and return a value of that type. If it did, your implementation would be valid. Rather, it means that for any type b the caller likes (that is a member of AST), reduce must be able to return a value in that type. b could well be the same as a sometimes, but it's the caller's choice, not the choice of reduce.

If your implementation returns a value of type a, then this can only be true if b is always equal to a, which is what the compiler is on about when it reports failing to prove that b ~ a.

Haskell does not have subtypes. Type variables are not supertypes of all the concrete types that could instantiate them, as you might be used to using Object or abstract interface types in OO languages. Rather type variables are parameters; any implementation which claims to have a parametric type must work regardless of what types are chosen for the parameters.

If you want to use a design where reduce can return a value in whatever type of AST it feels like (rather than whatever type of AST is asked of it), then you need to use your Expr box again, since Expr is not parameterized by the type of AST it contains, but can still contain any AST:

reduce :: a -> Env -> Expr
reduce ast _ = Expr ast

Now reduce can work regardless of the types chosen for its type parameters, since there's only a. Consumers of the returned Expr will have no way of constraining the type inside the Expr, so they'll have to be written to work regardless of what that type is.

Answer 3

Your default implementation doesn't compile, because it has the wrong definition.

reduce :: AST b => a -> b -> Env -> b
reduce ast _ = ast

Now ast has the type a and reduce function returns type b but according to your implementation you return ast which is of type a but the compiler expects b.

Even something like this will work:

reduce :: AST b => a -> b -> Env -> b
reduce _ ast _  = ast