Questions

[markandrus]

Hi,

I've been playing around with some toy code that overlaps with some of the problems this library solves. In looking at it, I had a few questions:

1. cardinality has type proxy a -> Integer. Should it be proxy a -> Natural instead?

2. universe has type [a]. Sometimes you may want the inhabitant at an index i. With the current API, I guess you would do genericIndex universe i. Would it make sense to have some function foo with type Natural -> Maybe a or Natural -> a, too? universe could perhaps have a default implementation in terms of this function, e.g.

   universe = takeWhile isJust $ map foo [1..]

   My feeling is that a class-specific implementation of Natural -> Maybe a could be more performant than genericIndex universe i.

3. Would it make sense to have a function Maybe a -> Natural on Universe or a related class? (For more context, my dissatisfaction with Enum's toEnum and fromEnum using Int led me here...)

4. Finite says

   Creating an instance of this class is a declaration that your universe eventually ends.

   This seems very similar to Bounded. Would it make sense to be able to recover something like a minBound and maxBound with this class? Such that

   minBound == universe `genericIndex` 0
   maxBound == universe `genericIndex` (cardinality (Proxy :: Proxy a))

   Although there is a law about universeF terminating, would such bounds with laws like the above give stronger guarantees about Finite? I worry that universeF versus universe don't tell me very much, since they have the same type [a].

5. Would an Infinite class make sense, e.g.

   class Universe a => Infinite a where
       infinite :: Stream a

   Reading this library, I see Universe could be finite or infinite, based on the [a] API. I see Finite should be finite (although I must trust universeF terminates). Something like infinite with a Stream a-based API could make clear that the Stream returned by infinite does not terminate. There could also be a law

   universe == toList infinite

Thanks for your consideration, Mark

[phadej]

1. I guess it's -> Integer because Natural is only a recent addition to base. Makes sense to change, if @dmwit is ok with adding (conditional) dependency on nats for older GHC

2. What about products? Or Universe a => Universe [a]. Try to implement indexUniverse! Even next is difficult.

3. The same as above.

instance Universe Void where universe = []

5. Where it could be useful?

Then we'll have a combinatorial problem

instance (Infinite a, Universe a) => Infinite (a, b) where
-- or?
instance (Universe a, Infinite a) => Infinite (a, b) where
-- as it's enough that only other argument is infinite.

Note: Finite is easy, as only combination of finite things is finite.

[markandrus]

1. I guess it's -> Integer because Natural is only a recent addition to base. Makes sense to change, if @dmwit is ok with adding (conditional) dependency on nats for older GHC

👍

2. What about products? Or Universe a => Universe [a]. Try to implement indexUniverse! Even next is difficult.

3. The same as above.

Hmm, I haven't tried this yet, but I figured if you can produce a [a] for some a, then you have a partial isomorphism between a and Natural...

universe = [x0, x1, x2, ...]
-- Naturals: 0,  1,  2, ...

And so you could write...

indexUniverse :: Natural -> Maybe a
indexUniverse 0 = x0
indexUniverse 1 = x1
indexUniverse 2 = x2
...

For products like (Universe a, Universe b) we have universe +*+ universe, where +*+ is a pairing function operating over lists, but I was wondering if it could be tweaked to have a type like the following:

(+*+) :: (Natural -> Maybe a) -> (Natural -> Maybe b) -> (Natural -> Maybe (a, b))

Maybe this is where the rub is. I'm not sure about Universe a => Universe [a].

4.

instance Universe Void where universe = []

Ah, didn't realize this was an instance. :-)

5. Where it could be useful?

I was just thinking: for the same reason it might make sense to have a more precise type for cardinality (Natural instead of Integer) would it also make sense to use a more precise type for infinite Universes. But I think you showed why this instance would be problematic.

[dmwit]

No big objection to Natural, I guess, especially since it's not even released yet (hence can't break compatibility with anything). I think Oleg did a great job of summarizing the tricky bits of the other problems.

Pairing functions are not enough: when one domain is finite, you no longer want a bijection between (N,N) and N, but between (X, N) and N where X is some finite set. It's not impossible to cook up, but it is hecking annoying, especially if you don't have a really solid compile-time test for the size of X (instances can't be conditional on whether a type is Finite or not). The "pairing function" analog of diagonals is similarly tricky to define. I encourage you to try to push your intuitions about how to do it down to the level of detail needed to actually write code for it!

[markandrus]

@dmwit @phadej thanks for the push to try it out myself. I have created a Gist here. I still need to test and compare to the results of this library, but when playing around in GHCi it seems... OK.

I think the instances for Either a b and (a, b) are correct. For [a], I tried handling Fix (ListF a) instead, and then translate to/from that representation.

[dmwit]

This seems a bit buggy:

> fromNatural 0 :: Maybe (Either Void ())
Nothing
> toNatural (Left C :: Either Alpha OneTwoOrThree)
5
> toNatural (Right Three :: Either Alpha OneTwoOrThree)
5
> cardinality :: Cardinality [Void]
Infinite

Relatedly, the implementations here seem significantly more complex/fragile. I would definitely want to see analogs of the helpers in http://hackage.haskell.org/package/universe-base-1.0.2.1/docs/Data-Universe-Helpers.html at least for people writing new instances.

It seems like a fun idea, though.

[markandrus]

Dang, good catches. I'll keep playing with this and try to land some tests.

Relatedly, the implementations here seem significantly more complex/fragile. I would definitely want to see analogs of the helpers in http://hackage.haskell.org/package/universe-base-1.0.2.1/docs/Data-Universe-Helpers.html at least for people writing new instances.

Yes, it certainly felt that way writing it... Agree about helpers. I haven't really worked through what supporting these APIs would mean when it comes to writing new instances. Could be tricky.

Thanks for taking a look :-)

[treeowl]

I really like the idea of offering a Natural -> Maybe a method ... or maybe more than one. The tricky bit is that sometimes the order that's efficient for generating all of the values isn't so efficient for generating just one of them. It would also be nice to have a method of type Maybe Natural, that may or may not offer up the size of the universe. It would always give Nothing for an infinite universe, but it could also do so for a finite universe, indicating that it's hard to calculate the size.

I also wish for an InfiniteUniverse subclass offering an explicitly infinite stream instead of a list; that should help users avoid writing unreachable code.

[phadej]

Is there the go to Stream (with stream fusion) ?