[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

Roel van Dijk vandijk.roel at gmail.com
Wed Oct 14 05:25:10 EDT 2009

You can help ghci out a bit with type synonyms:

type T   a = (a, a)
type T2  a = T  (T a)
type T4  a = T2 (T2 a)
type T8  a = T4 (T4 a)
type T16 a = T8 (T8 a)

f0 :: a -> T a
f1 :: a -> T2 a
f2 :: a -> T4 a
f3 :: a -> T8 a
f4 :: a -> T16 a

f0 x = (x,x)
f1   = f0 . f0
f2   = f1 . f1
f3   = f2 . f2
f4   = f3 . f3
f5   = f4 . f4

With newtypes I can probably abstract even more. (newtype X a b = X (a (a b))

Inferring the type of f5 also stops my machine in its tracks. But I
*was* able to infer the type of (f4 . f4).

:t (f4 . f4)
(f4 . f4) :: a -> T16 (T16 a)

:t f5
-- buy new computer

Even when you only specify a type for f0 in terms of T you'll get more
readable types:

:t f3
f3 :: a -> T (T (T (T (T (T (T (T a)))))))

But the amount of computation required seems the same.

More information about the Haskell-Cafe mailing list