Generic function result in Haskell based on some predicates

Question

Is it possible to write a function in haskell, which returns a generic type when:

• in the body of this function we output as a result 2 separate types A and B (based on some computations)
• types A and B have a common type class C

Lets see the sample code. The type checker SHOULD be able to check, that this code is correct - function test outputs instance of type A or B, so we can perform f on the result.

data A = A 
data B = B

class C a where
    f :: a -> Int

instance C A where
    f x = 2

instance C B where
    f x = 3

-- This function fails to compile:
-- I want something like:
-- test :: C a => Int -> a
test x = if x < 1  
        then A
        else B

main = do
    print $ f $ test 0
    print $ f $ test 1

I know this could look like anti-pattern or something like that, but I want to know the answer because I love to test Haskell features, especially when it comes to the type system.

Answer 1

The problem here is that you Haskell's type variables are universally quantified.

This means that they can be read as

forall a. C a => Int -> a

This means that the caller chooses the concrete type of a. Not the callee.

To fix this, you'd need something called "existential" variables. Universally quantified variables should be read as "forall", existentially quantified variables should be read as "there exists".

Quick sketch of how to do this

{-# LANGUAGE ExistentialQuantification, GADTs #-}

-- Use existentials 
data Box = forall a. C a => Box a

-- Use GADTs
data Box' where
  Box' :: C a => a -> Box'

instance C Box where
    f (Box a) = f a

test :: Int -> Box
test x = if x < 1  
    then Box A
    else Box B

The essence of this is that we hide our concrete C instance behind this Box data type and then we pass that around instead of a universally quantified type variable.

Alternatively, you can avoid the Box type for Rank2Types with simple continuations.

test :: Int -> (forall a. C a => a -> r) -> r
test x c = if x < 1 then c A else c B
main = do
  test 1 (print . f)
  test 0 (print . f)

Fun quirk of existential variables, try this code with GHC

fun = foo
  where (Box foo) = test 1