Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Wednesday 14 October 2009 5:25:10 am Roel van Dijk wrote:
With newtypes I can probably abstract even more. (newtype X a b = X (a (a
b))
In fact, with GHC extensions, you don't need newtypes:
{-# LANGUAGE LiberalTypeSynonyms #-}
type T a = (a,a)
type X f a = f (f a)
f0 :: a - T a
f0 x = (x,x)
f1 :: a - X T a
f1 = f0 . f0
f2 :: a - X (X T) a
f2 = f1 . f1
f3 :: a - X (X (X T)) a
f3 = f2 . f2
f4 :: a - X (X (X (X T))) a
f4 = f3 . f3
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
Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms,
while checking f5 does for some reason. I'm perplexed that having f5 defined
in the file doesn't trigger the explosion unless you declare a type (even in
terms of X and T) or ask for its type at the prompt.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Wed, Oct 14, 2009 at 11:53 AM, Dan Doel dan.d...@gmail.com wrote:
In fact, with GHC extensions, you don't need newtypes:
{-# LANGUAGE LiberalTypeSynonyms #-}
Ah, I completely forgot about that language extension. Thanks!
Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms,
while checking f5 does for some reason. I'm perplexed that having f5 defined
in the file doesn't trigger the explosion unless you declare a type (even in
terms of X and T) or ask for its type at the prompt.
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
:-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones simo...@microsoft.com wrote: | Is there any way to define type-level multiplication without requiring | undecidable instances? | | No, not at the moment. The reasons are explained in the paper Type | Checking with Open Type Functions (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances. It's also worth noting that while undecidable instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad. Simon I have written code that makes heavy use of multi-parameter type classes in the ``finally tagless'' tradition, which takes several seconds and many megabytes of memory for GHCI to infer its type. However, that example is rather complicated, and I am not sure its type inference complexity is exponential---it is at least very bad. Are there any simple, well-known examples where Haskell type inference has exponential complexity? Or Hindley-Milner type inference, for that matter? (Haskell 98 is not quite Hindley-Milner?) Sincerely, Brad Larsen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. -- Lennart On Tue, Oct 13, 2009 at 6:04 PM, Brad Larsen brad.lar...@gmail.com wrote: On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones simo...@microsoft.com wrote: | Is there any way to define type-level multiplication without requiring | undecidable instances? | | No, not at the moment. The reasons are explained in the paper Type | Checking with Open Type Functions (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances. It's also worth noting that while undecidable instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad. Simon I have written code that makes heavy use of multi-parameter type classes in the ``finally tagless'' tradition, which takes several seconds and many megabytes of memory for GHCI to infer its type. However, that example is rather complicated, and I am not sure its type inference complexity is exponential---it is at least very bad. Are there any simple, well-known examples where Haskell type inference has exponential complexity? Or Hindley-Milner type inference, for that matter? (Haskell 98 is not quite Hindley-Milner?) Sincerely, Brad Larsen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
2009/10/13 Lennart Augustsson lenn...@augustsson.net: Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will be 2^(number of dup's). I experimented and found that GHC can stand pretty long line of dup's. More than 20, at least. One part of our program took too much time to typecheck some time ago. 3 and half minutes for ~900 lines module. Most of operations was inside heavily parametrized monad (5 parameters, each is a Peano number). Then my colleague moved parameters into associated types of relevant type class and now it typechecks in ten seconds. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tue, Oct 13, 2009 at 12:32 PM, Serguey Zefirov sergu...@gmail.com wrote: 2009/10/13 Lennart Augustsson lenn...@augustsson.net: Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will be 2^(number of dup's). I experimented and found that GHC can stand pretty long line of dup's. More than 20, at least. One part of our program took too much time to typecheck some time ago. 3 and half minutes for ~900 lines module. Most of operations was inside heavily parametrized monad (5 parameters, each is a Peano number). Then my colleague moved parameters into associated types of relevant type class and now it typechecks in ten seconds. Good example! I have a feeling that the `dup' example is a bit contrived, not something that one would be likely to find in the wild. Heavily parameterized type classes, on the other hand, are more common in real code. Hence, that is more likely where someone would run into really awful type inference performance without expecting it. Brad ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tuesday 13 October 2009 1:06:41 pm Brad Larsen wrote: Good example! I have a feeling that the `dup' example is a bit contrived, not something that one would be likely to find in the wild. This is, after all, why HM is useful. In general, there are programs that take exponential time/space to type check, but those programs don't come up much in real code. Also, you can do better than 2^n: f0 x = (x,x) f1 = f0 . f0 f2 = f1 . f1 f3 = f2 . f2 ... Here, if fN results in a nested tuple of size M, then f(N+1) results in a tuple of size M^2, since we replace all the variables with a copy of the tuple. So we have 2, 4, 16, 256, ... 2^(2^N) Turning f0 into an M-tuple gets you M^(2^N), I believe, and composing K times at each step would get you M^(K^N). But anyhow, we have not merely an exponential, but a double exponential. :) f4 takes a noticeable amount of time to check here (in ghci), and f5 makes my machine start swapping. Of course, one isn't likely to write code like this, either. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
