Making the type of a function depend on input

Question

So I noticed that after n=20 the factorial function given in LearnYouAHaskell (below) craps out because of the finite work range of the Int type.

factorial :: Int -> Int
factorial 0 = 1
factorial n * factorial (n-1)

Using factorial :: Integer -> Integer fixes the issue nicely, but it brought to mind the question. Supposedly Integer is slightly slower than Int so ideally (and I know I'm pinching pennies here) I'd want my factorial function to only resort to Integer when the input is greater than 20 and retain the Int->Int type for the smaller numbers. Seems like there should be an elegant solution for this using if-then-else or guards, but keep running into syntactic pepper (error messages)

Answer 1

You can make a hackish solution without dependent types by using either a sum type and growing when needed or delaying the cast to Integer till the end in some cases. I don't expect either solution would perform better than using Integer - do not fear the Integer, gmp and mpir are quite good.

The casting solution is something like:

selectiveFactorial :: Integer -> Integer
selectiveFactorial i
    | i < 20 = fromIntegral $ factorial (fromIntegral i :: Int)
    | otherwise = factorial i

factorial :: Integral a => a -> a
factorial 0 = 1
factorial n = n * factorial (n - 1)

Answer 2

As Rein Henrichs said you could do these things in a language with dependent types, which Haskell does not (yet, quite) have. In Idris, say, it would look something like

factorial : (n : Int) -> if n <= 20 then Int else Integer
factorial n with (n <= 20)
  factorial n | True = thisfactorial n
  factorial n | False = thatfactorial n

But how will you use this result? Well, you'll need to do the comparison to figure out what type to expect, and when all is said and done, I don't see how you've won anything. For completeness, the use site could look something like this:

use : Int -> Integer
use n with (factorial n)
  use n | fn with (n <= 20)
    use n | fn | False = fn
    use n | fn | True = cast fn

Note that the order of the with clauses is significant! The fn binding gets type if n <= 20 then Int else Integer; for reasons I don't entirely understand, the n <= 20 test must be to the right of that in order for the pattern match to affect its type.