[Haskell-cafe] Exponential complexity of type checking (Was:
Type-level naturals & multiplication)
Dan Doel
dan.doel at gmail.com
Wed Oct 14 07:45:34 EDT 2009
On Wednesday 14 October 2009 6:15:11 am Roel van Dijk wrote:
> If you declare a type for f5 then ghci must check if that type is
> correct, which triggers the explosion. If you don't declare a type
> then it won't infer the type until necessary. Basically, ghci is lazy
Well, that may be the explanation, but it's a bit more convoluted than I'd
have initially thought. For instance, if I write:
e = head ()
it fails immediately with a type error, so clearly it must be doing some level
of checking immediately. However, it only needs to check 'head' and '()' to
notice that they're incompatible, so I suppose it may not need to compute the
type of e (were it well-typed). But then, adding:
f6 = f5 . f5
produces no more delay than before. Nor does:
g = snd . f5
So ghci is able to verify that f5 can be instantiated to the forms a -> b and
b -> c in the first case, and that it is of the form a -> (b,c) in the second
case, without blowing up. However, either of:
e = f5 ()
e' () = f5 ()
does blow up, so it must be verifying more than the fact that f5 is of the
form a -> b, where a can be instantiated to (), which is odd if it's smart
enough to only compute the portion of the type necessary to verify that
applications can be well typed.
-- Dan
More information about the Haskell-Cafe
mailing list