[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