Returning a subset of types in Haskell

Question

I'm trying to restrict the return type of a function to a subset of (kind) constructors. I can use typeclasses to restrict the input types, but when I try the same technique on return types as shown below, I get a Couldn't match type ‘s’ with ‘'A’ error.

Is there a way to restrict the bar function below to return either SomeA or SomeB?

It seems that Liquid Haskell is an alternative, but it seems that this should be possible using only things like DataKinds, GADTs and/or TypeInType.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Test where

data State = A | B | C

class AorB (s :: State)
instance AorB 'A
instance AorB 'B

data Some (s :: State) where
  SomeA :: Some 'A
  SomeB :: Some 'B
  SomeC :: Some 'C

-- This works
foo :: AorB s => Some s -> Bool
foo aorb = case aorb of
  SomeA -> True
  SomeB -> False

-- This fails to compile with ""Couldn't match type ‘s’ with ‘'A’""
bar :: AorB s => Some s
bar = SomeA

Answer 1

A few things here. If you compile with -Wall (which you should!) you would find that your definition of foo gives an inexhaustive patterns warning. And it should, because the way you have defined AorB is "open". That is, somebody in another module is free to declare

instance AorB 'C

and then your definition of foo will suddenly become invalid as it fails to handle the SomeC case. To get what you are looking for, you should use a closed type family:

type family IsAorB s where
    IsAorB 'A = 'True
    IsAorB 'B = 'True
    IsAorB _  = 'False

This family is totally defined on States. We would then define your previous AorB constraint like so:

type AorB s = IsAorB s ~ 'True

However, in a moment we will need to use AorB in curried form, which is not allowed for type synonyms. There is an idiom for declaring curriable synonyms which is a bit clunky, but is the best we have at the moment:

class    (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

Anyway, with this new definition, you will find that the inexhaustive pattern warning goes away for foo. Good.

Now on to your question. The trouble with your definition (with an explicit forall added for clarity)

bar :: forall s. AorB s => Some s
bar = SomeA

is that we are allowed to instantiate bar @B, giving us

bar @B :: AorB B => Some B
bar = SomeA

AorB B is satisfiable, so we should be able to get a Some B, right? But not according to your implementation. So something is logically wrong here. You are probably looking to return an existentially quantified s, in other words, you want the bar function to choose which s it is, not the caller. Informally

bar :: exists s. AorB s <AND> Some s

That is, bar chooses an s, and returns a Some s, together with some evidence that AorB s holds. This is no longer an implication, we would not put the responsibility on the caller to prove that the type bar chose was either A or B -- the caller has no idea what was chosen.

Haskell does not directly support existential types, but we can model them with a GADT (make sure to use PolyKinds and ConstraintKinds)

data Ex c f where
     Ex :: c a => f a -> Ex c f

Ex c f can be read as "there exists a such that c a holds and there is a value f a". This is existential becuase the variable a does not appear in Ex c f, it's hidden by the constructor. And now we can implement bar

bar :: Ex AorB Some
bar = Ex SomeA

We can test that the constraints are correctly propagated by passing this to your foo:

test :: Bool
test = case bar of Ex s -> foo s

There you go.

That said, design-wise I would just say

bar :: Some A

instead. Type signatures should be as informative as possible. Don't hide information that you know -- let abstraction do the hiding. When you hide information about your assumptions/arguments, you are making your signature stronger; when you hide about your results, you are making it weaker. Make it strong.

Answer 2

Here is the full working code based on @luqui's answer, for reference:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}

module Test2 where

data State = A | B | C

type family IsAorB (s :: State) where
  IsAorB 'A = 'True
  IsAorB 'B = 'True
  IsAorB _  = 'False

-- type AorB s = IsAorB s ~ 'True

class (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

data Some (s :: State) where
  SomeA :: Some 'A
  SomeB :: Some 'B
  SomeC :: Some 'C

data Ex c f where
  Ex :: c a => f a -> Ex c f

bar :: Ex AorB Some
bar = Ex SomeA