How to create a well-typed function that returns two different types?

Question

I'm highly interested in compiling Formality-Core modules to Haskell libraries. While I could use unsafeCoerce everywhere, it would be more interesting if I could preserve the type information, allowing compiled modules to be published on Cabal and used by other Haskell projects. The problem is that dependent types allow programs that are forbidden by Haskell. For example, the function foo below:

foo: (b : Bool) -> If(b)(Nat)(Bool)
  (b)
  b<(b) If(b)(Nat)(Bool)>
  | zero;
  | false;

Returns a different type depending on the input. If the input is false, it returns the number zero. If the input is true, it returns the boolean false. It seems like a function like this can't be translated to Haskell. I believe that, on the last years, Haskell has made good progress towards dependent type, so, I wonder: is there any way to write functions that return different types based on the input value?

Answer 1

GADTs + TypeFamilies (optionally, + DataKinds) can do roughly this. So:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data GADTBool a where
    GADTFalse :: GADTBool False
    GADTTrue :: GADTBool True

type family If cond t f where
    If False t f = f
    If True  t f = t

foo :: GADTBool b -> If b Int Bool
foo GADTTrue = 0
foo GADTFalse = False

Of course, you'll probably actually want foo :: GADTBool b -> If b (GADTInt 0) (GADTBool False) if you plan to do this kind of thing pervasively. The search term you want for seeing more examples of this kind of hackery is "singleton types", often abbreviated just "singletons".

Answer 2

The state of the art remains the singleton approach.

data SBool b where
  SFalse :: SBool 'False
  STrue :: SBool 'True

type family If (b :: Bool) (t1 :: k) (t2 :: k) :: k where
  If 'False x _ = x
  If 'True _ y = y

foo :: SBool b -> If b Natural Bool
foo SFalse = 0
foo STrue = False