dmwit / universe

Classes for types where we know all the values
BSD 3-Clause "New" or "Revised" License
37 stars 17 forks source link

Stack overflow when computing `universe` of `Map Word Word`. #64

Open jonathanknowles opened 2 years ago

jonathanknowles commented 2 years ago

Hi there!

Many thanks for making this library.

I encountered the following issue while experimenting within ghci:

> :set -XTypeApplications
> import Data.Map.Strict (Map)
> import Data.Universe.Class
> take 1 $ universe @(Map Word Word)
*** Exception: stack overflow

The issue seems to be related to the cardinality of the key type, since:

> take 1 $ universe @(Map Word ())
*** Exception: stack overflow 

Additionally:

> cardinality @(Map Word Word)
Tagged

(does not terminate, and CPU spins at 100%)

Perhaps I'm using the library incorrectly?

Using a type with a much smaller cardinality works as I would expect:

> cardinality @(Map Bool Bool)
Tagged 9

Details of my environment:

Let me know if you need me to provide any more details, am happy to help.

Many thanks again!

Jonathan

dmwit commented 2 years ago

You are using the library correctly. I don't... really think it's reasonable to expect the computer to be able to answer cardinality @(Map Word Word), as the answer is something like (2^64)^(2^64), which takes more memory to represent than the entire world's supply of RAM by about two orders of magnitude. (Smaller factor than I was expecting before I did my back-of-the-envelope, TBH!) It does seem reasonable to be able to start enumerating values with either universe or universeF, though. Let me think about how to make that work a bit better.

jonathanknowles commented 2 years ago

I don't... really think it's reasonable to expect the computer to be able to answer cardinality @(Map Word Word), as the answer is something like (2^64)^(2^64), which takes more memory to represent than the entire world's supply of RAM by about two orders of magnitude.

That's a very good point. I hadn't performed the calculation here, but you're right. My apologies!

It does seem reasonable to be able to start enumerating values with either universe or universeF, though. Let me think about how to make that work a bit better.

I'm wondering, does the library have a generalized notion of the "complexity" of a value, and does universe follow the principle of generating values in increasing order of complexity, from the simplest first?

If we assume that it's possible to build an integral measure of complexity (for example, complexity :: a -> Natural), then perhaps it could be arranged that universe will generate a sequence such that complexity <$> universe is always a monotonically increasing sequence.

For example, for some type Foo (which could be a tree-like structure):

>>> take 10 (complexity <$> universe @Foo)
[0, 1, 1, 2, 2, 2, 3, 3, 3, 3]

If we could rely on the property that evaluating elements earlier in the list will be less expensive than evaluating items later in the list, then perhaps it would be easier to reason about how much evaluation will be required to evaluate some prefix of the list.

Apologies if you've already thought of such a solution and it's impractical, or if the library already does this.

Many thanks for replying, and for making this library!