Can I have a polymorphic function argument that may not need to be supplied for some types?

Question

I have a datatype F with a special-case for Int:

{-# LANGUAGE GADTs, RankNTypes #-}
data F a where
   FGen :: a -> F a
   FInt :: F Int

Without exposing the details of this datatype to callers - the real datatype is more complicated containing internal implementation details - I want to provide an API for using it:

transform :: (a -> b) -> b -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i

If I'm going to call transform on a F Int, clearly both of the first two arguments are important:

transformInt :: F Int -> Int
transformInt = transform (+1) 5

But if I'm going to call it on a F Char, the second argument is unnecessary as the value can't be a FInt:

transformChar :: F Char -> Char
transformChar = transform id (error "unreachable code")

Is there a way I can express this in the type of transform?

I tried

transform :: (a -> b) -> (a ~ Int => b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i

but then transformChar doesn't compile with

    Couldn't match type ‘Char’ with ‘Int’
    Inaccessible code in
      a type expected by the context: (Char ~ Int) => Char
    In the second argument of ‘transform’, namely
      ‘(error "unreachable code")’
    In the expression: transform id (error "unreachable code")
    In an equation for ‘transformChar’:
        transformChar = transform id (error "unreachable code")

and anyway I'd still want absurd value I could use instead of the error to properly express that the compiler should be able to prove the code will never be used.

Answer 1

We can use the propositional equality type in Data.Type.Equality and we can also express inaccessibility of code from GHC 7.8, using empty case expressions:

{-# LANGUAGE GADTs, RankNTypes, EmptyCase, TypeOperators #-}

import Data.Type.Equality   

data F a where
   FGen :: a -> F a
   FInt :: F Int

transform :: (a -> b) -> ((a :~: Int) -> b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i Refl

transformChar :: F Char -> Char
transformChar = transform id (\p -> case p of {})
-- or (\case {}) with LambdaCase

transformInt :: F Int -> Int
transformInt = transform (+1) (const 5)

Answer 2

I like the answer with a GADT for the type equality proof better. This answer explains how to do the same thing with TypeFamilies. With closed type families we can write functions from types to the unit () and zero Void of the type system to represent prepositional truth and false.

{-# LANGUAGE TypeFamilies #-}

import Data.Void

type family IsInt a where
    IsInt Int = ()
    IsInt a   = Void

The second argument to transform is () -> b when IsInt a and Void -> b (the type of absurd) when a isn't an integer.

transform :: (a -> b) -> (IsInt a -> b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i ()

transformChar can be written in terms of absurd and transformInt must pass in b as a constant function.

transformChar :: F Char -> Char
transformChar = transform id absurd

transformInt :: F Int -> Int
transformInt = transform (+1) (const 5)

More Reusable

At András Kovács suggestion, we can make this more reusable with a type family for type equality (==) that returns lifted Bools.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}

type family (==) a b :: Bool where
    (==) a a = True
    (==) a b = False

We could provide another type family to convert True to () and False to Void. For this specific problem it reads better to go all the way from True or False and some type b to () -> b or Void -> b.

type family When p b where
    When True  b = ()   -> b
    When False b = Void -> b

The type of transform then reads.

transform :: (a -> b) -> When (a == Int) b -> F a -> b