AtLeastOne a b c d ...

Question

AtLeastOne a b c d ...

Closed this issue 8 years ago · 5 comments

I was wondering if you could point me to anything on constructing larger 'Inclusive Or' types.

We're often provided with an ergonomic way of creating large XOR types

-- Elm
type OnlyOne a b c = ThisOne a | ThatOne b | AnotherA a | Nobody | Hello c ...

and large AND types

-- Haskell
data AllOfThese a b c d = AllOfThese a b c d

or

-- Elm
type alias AllOfThese =
  { FirstOne : a
  , SecondOne : b
  ...
  }

Large analogues of Maybe also seem relatively comfortable

data MaybeSomeOfThese a b = MaybeSomeOfThese (Maybe a) (Maybe b) ...

Is there anything like this for OR? Does it have to be included at the syntax level or can a construction like MaybeSomeOfThese be OK?

Of course, we can

data AtLeastOneOfThese a b c = AtLeastOneOfThese (These a (These b c))

But that gets unwieldy, and the fact that there's no difference depending on which way we bracket is uncomfortable.

Thank you very much and doubly so if you get a chance to respond!

Answer 1 · 2016-08-31T15:55:22.000Z

I'm sorry, I don't know of any nice sugar here. I imagine there's something like an injection that might work here though.

But that gets unwieldy,

Yeah, it's a bit of a pain to construct and destruct these values whole cloth. But it's pretty straight forward if you break the problem into pieces and create a solution from those pieces.

Like in your example, if you have some functions

foo : a -> e
bar : b -> d
baz : c -> d
qux : a -> d -> e
quux : b -> c -> d

then you can form destructors pretty easily

barBaz : These b c -> d
barBaz =
  these bar baz quux

fooBarBaz : These a (These b c) -> e
fooBarBaz =
  these foo barBaz qux

atLeastOneOfThese : AtLeastOneOfThese a b c -> e
atLeastOneOfThese (AtLeastOneOfThese x) =
  fooBarBaz x

It pushes you to make small simple functions. And I think small simple functions are good :).

and the fact that there's no difference depending on which way we bracket is uncomfortable.

This is actually a pretty important thing. It's the associative property. It means that you don't lose any expressive power if you make a These a (These b c) vs a These (These a b) c. Or, equivalently, if someone gives you a These a (These b c) and you only have functions that work with These (These a b) c, you can still work with their data.

A function for that here might be useful...

Answer 2 · 2016-08-31T16:08:32.000Z

This is actually a pretty important thing. It's the associative property. It means that you don't lose any expressive power if you make a These a (These b c) vs a These (These a b) c

Sorry I might have been a bit unclear. I find it uncomfortable because I don't want there to be any additional degrees of freedom in my representation / syntax to my semantics. So if I were to "pick my ontology" of nTheses, it would be of equivalence classes of nested These or something.

It pushes you to make small simple functions. And I think small simple functions are good :).

That's awesome! Correct me if I'm wrong, but that still leaves us needing to nest our These if we want a type like AtLeastOneOf a b c d e f g h i, right? Is there a way to break down a type that looks like that into smaller pieces as well?

Answer 3 · 2016-09-01T04:02:37.000Z

can a construction like MaybeSomeOfThese be OK?

I missed this sentence earlier. It should be noted that MaybeSomeOfThese a b /= These a b

MaybeSomeOfThese a b
  == MaybeSomeOfThese (Maybe a) (Maybe b)
  == MaybeSomeOfThese (Result () a) (Result () b)
  == (Result () a, Result () b)
  == (() + a) * (() + b)
  == (() * ()) + (() * b) + (a * ()) + (a * b)
  == () + b + a + (a * b)
  == () + a + b + (a * b)
  /=      a + b + (a * b)
  == Result a (Result b (a, b))
  == a | b | (a, b)
  == This a | That b | These a b
These a b

So, it's not okay to directly substitute one for the other.

That's awesome! Correct me if I'm wrong, but that still leaves us needing to nest our These if we want a type like AtLeastOneOf a b c d e f g h i, right? Is there a way to break down a type that looks like that into smaller pieces as well?

Hmm, I don't know of any best way to do that.

Probably the simplest thing to do is pull out some pieces to their own type and recompose them together only where you actually need them. My gut tells me that probably whatever your real problem would be where you have multiple different types probably has some form of grouping between certain types.

What I mean by that is if you want to display Foos, Bars, Bazs and Quuxs all at once, then probably in other parts of the program you also use Foos and Quuxs a lot together. So you might want to make a type FooQuux = FooQuux (These Foo Quux) and then that makes your displaying all of them together slightly easier.
Perhaps you could try breaking it down binarily rather than associating to one side. You're kind of making a tree of types, and if you associate all to one side it's an unbalanced tree. A.k.a a list.

So instead of:
```
type AtLeastOneOf a b c d e f g h i
  = AtLeastOneOf (These a (These b (These c (These d (These e (These f (These g (These h i))))))))
```
You might have something like this:
```
type AtLeastOneOf a b c d e f g h i
  = AtLeastOneOf (These (These (These a b) (These c d)) (These (These e f) (These g (These h i))))
```
It's more of a pain to understand (similarly for regular trees vs lists), but when you go to construct one, the maximum depth is three rather than seven.
That probably also makes your destruction easier as well, since you don't have to combine as many.

Another thing you could do is make a larger or type to start with.

type Things a b c
  = This a
  | That b
  | Thing c
  | These a b
  | Those b c
  | TheOther a c
  | Things a b c

type AtLeastOneOf a b c d e f g h i
  = AtLeastOneOf (Things (Things a b c) (Things d e f) (Things g h i))

Then the deepest you have to go to construct or destruct something is two. Of course, now you've got seven cases to deal with, so the problem shifts 😄. It's trade-offs all the way down...

Answer 4 · 2016-09-01T07:59:47.000Z

I missed this sentence earlier. It should be noted that MaybeSomeOfThese a b /= These a b

Yes, sorry. What I meant was, if I want to express () ∨ a ∨ b ∨ c ..., it's fairly easy to do with a big product of Maybe. I was wondering if it were possible to do combine ergonomic sums / products with these to do the same thing.

But now I'm slightly worried I'm wrong. Is this equality right?

   (() ∨ a) ∧ (() ∨ b)
== () ∨ (a ∧ b)

It seems right from a propositional logic standpoint, but MaybeSomeOfThese a b could be MaybeSomeOfThese (Just a) Nothing.

Thank you so much for the guidance, Hardy! I will mull over your wisdom

Answer 5 · 2016-09-01T08:27:21.000Z

You're absolutely right, that is incorrect. We're dealing with sums and products and as such the sum doesn't distribute over the product.

Good catch!