search

byorgey / enumeration

Simple Haskell package for efficiently indexable finite and infinite enumerations.
BSD 3-Clause "New" or "Revised" License
11 stars 2 forks source link

functionOf with unit or void codomain could be more permissive #1

Closed shaylew closed 4 years ago

shaylew commented 4 years ago

Right now functionOf is an error whenever the domain is infinite. But even for infinite domains, it's easy to give a well-defined answer when the codomain has cardinality 0 or 1 -- there are zero maps into void and one (constant) map into unit.

byorgey commented 4 years ago

Let's definitely fix this. Do you want to tackle it, or should I?

shaylew commented 4 years ago

Could you? I haven't stuck my fingers into this particular pie very far :P

One more decision that fixing this is going to expose is what to do when the codomain is 0 or 1 and the domain enumeration isn't well-defined, e.g. in functionOf (functionOf nat nat) void. For unit it's possible to be lazy in the first argument, but for void it looks like there's no getting around matching on the cardinality.

byorgey commented 4 years ago

Sure, I'll take a look at it.

byorgey commented 4 years ago

Hmm, you're right, that's tricky. I can think of various ways to change things so that e.g. functionOf nat nat doesn't throw an error, but instead returns a valid Enumeration which has a cardinality but blows up if you try to use it for anything else. However, that might be unexpected in other ways, and I don't know if it's worth it.

byorgey commented 4 years ago

@shaylew What do you think of #2 ? I decided in the context of a general-purpose enumeration library it doesn't make sense to try to do something special with functionOf nat nat just in case we later decide to use it as the first argument to functionOf _ void. But we can handle that case in Disco. The difference is that in Disco we have syntax for describing types, and we can ask whether they are empty or infinite or whatever independently of enumerating them. In this library, on the other hand, all we have are enumerations, so we can't really talk about things like "functions from N to N" at all.

shaylew commented 4 years ago

Doing the remaining cases on the Disco side makes sense to me -- its probably better to fail cleanly when there's no sensible answer to give.