Haskell: Understanding generalised algebraic data types

Question

I have the following code, which outlines a language of boolean and arithmetic expressions:

data Exp a where
     Plus :: Exp Int -> Exp Int -> Exp Int
     Const :: (Show a) => a -> Exp a 
     Not :: Exp Bool -> Exp Bool
     And :: Exp Bool -> Exp Bool -> Exp Bool
     Greater :: Exp Int -> Exp Int -> Exp Bool

The evaluation function for the above language has the following type:

eval :: Exp a -> a

I am trying to understand what are the possible types the eval function can return. The above code uses GADTs which enable the type Exp a to be defined in terms of the type signatures of its constructors. The return type of the constructors is not always Exp a. I believe that the types eval can return include Int, Bool, or a value of any type implementing Show. However, is it possible for eval to return any other type besides the three I mentioned previously (since the return type of the function is a)? Any insights are appreciated.

Answer 1

To be clear, given your definition of Exp above, the answer is "yes": any function with type signature eval :: Exp a -> a can only return a (defined) value of type Int, Bool, or some other type with a Show instance. Because any type (of kind *) can be given a Show instance, that technically means that eval can return any type, but within a particular program that has a fixed set of Show instances, eval will be limited to returning values from this set of types.

You can see that this must be true as follows. Suppose that eval e returned a value of some fixed type t for some expression e. By the type signature of eval, that would imply that e must have type Exp t. However, data type declarations are "closed" meaning that the set of constructors given in the data Exp a declaration is exhaustive, and they represent the only methods of constructing a (defined) value of type Exp a. It's clear from the set of constructors that the only possible values of type Exp a are those that appear in the rightmost positions of the constructors' signatures: Exp Int, Exp Bool, and Exp a with the constraint Show a. Therefore, these are the only types possible for e implying that t must be Int, Bool, or some other a satisfying the constraint Show a.

As always in reasoning about Haskell types, we have to be a little bit careful in considering undefined/bottom values. If you consider "returning an undefined value" to be meaningful, then, indeed, eval can "return" an undefined value of any type, even one without a Show instance. For example, the following will typecheck:

stupid :: Exp (Int -> Int)
stupid = eval undefined

However, if your reason for asking the question is to determine whether you'd ever be in a position where the expression eval e might unexpectedly have a type other than Int, Bool, or some Show a => a that you would somehow have to handle, then no. The form of the GADT places limits on the possible types a in the signature eval :: Exp a -> a.

Answer 2

Exp a -> a is a type that could have many possible functions. For example, a valid function that probably isn't the one you are thinking of as "the" eval function is

foo :: Exp a -> a
foo (Plus _ _) = 3
foo (Const x) = x
foo (Not _) = True
foo (And _ _) = True
foo (Greater _ _) = True

The image of a function is the set of values it can return. This example demonstrates that the function foo and the eval you are expecting have different images, despite having the same return type forall a. a.

You are asking, in essence, what the union of all possible images of functions of type Exp a -> a is. This depends greatly on the actual definition of Exp. As currently defined, that would be the union of Int, Bool, and Show a => a.

Exp the type constructor, though, is capable of defining uninhabited types. The type Exp (Int -> Int) exists, even though you haven't defined a constructor which can create values of that type. Since you can't provide a value of type Exp (Int -> Int) for any potential eval function, it can't affect the image of any such function, either.

Changing the definition of Exp to include such a constructor would increase the set of values that could be passed to a function of type Exp a -> a, thus increase the set of values that could occur in the image of such a function.