Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Think about sum types #20

Open
3noch opened this issue Apr 15, 2020 · 6 comments
Open

Think about sum types #20

3noch opened this issue Apr 15, 2020 · 6 comments

Comments

@3noch
Copy link

3noch commented Apr 15, 2020

I haven't thought about them in the context of higgledy but I want to get the ball rolling. Have you already considered what this would look like?

@i-am-tom
Copy link
Owner

It's a really tricky one for a number of reasons. The short answer is "yes, and I have a good idea how I'd go about it". The long answer? Well, it's maybe easier to consider this question in terms of each function in this library:

construct / destruct (fine?)

These functions would actually be fine, and would generalise quite nicely to sum types with very little effort (as in, about 3 or 4 lines of code). We can tell which constructor we're using in both functions by looking at the input, and reusing it in the output.

labels / labelsWhere (fine?)

Again, this is fine - I suspect this is a similarly small amount of code.

position / field (needs duplicating / weakening)

This is where things start getting tricky, and it's worth looking at how GHC (according to the Haskell spec) currently deals with these things:

Two constructors with the same field but different types

data Test = C { a :: Bool } | D { a :: Int }

-- <interactive>:3:1: error:
--     • Constructors C and D give different types for field ‘a’
--     • In the data type declaration for ‘Test’

Perfect! Our API could similarly reject this, and we wouldn't need to worry ourselves about figuring out the type of the a accessor.

Two constructors with the same position but different types

data Test = C Bool | D Int

OK, now we're in trouble: what's the type of position @1 in the context of this type? It depends on the constructor we're accessing! So, for a start, we're going to need some sort of dependent type, but we're also going to need to weaken position from a Lens to a Traversal, which means that access now always involves a Maybe around the result. We could have a separate optic, of course, that produces a Traversal over any of the types within, and maybe that's the answer.

Two constructors with different numbers of arguments

data Test = C Bool | D Int String

Now, what's the type of position @2? Again, we're in a similar situation: the validity of this optic depends on the constructor, so we have to fall back on a Traversal again.

All of the above is to say: yes, you could absolutely achieve this (and I think @kcsongor has already gone to the effort of writing the types traversal that could effectively replace position for sum types), but you would end up having a separate API.

build (maybe fine, maybe needs duplicating)

This is where, I think, it becomes a bit hairy. Right now, there are a few ways one can create an HKD value:

  • mempty, which relies on a Monoid instance for the f-wrapped version of all your field types.
  • destruct, which relies on you already having a complete version of the "base type" you want to HKD-ify. Not super convenient if you're building up a "partial" version of your type, for example.
  • build, which is the only one free of these restrictions.

build is the closest we can get to the standard Haskell syntax:

-- Ideal
eg = Test { name = Just "Tom", friends = Just "loads" }

-- Actual - one field at a time
eg = build @Test (Just "Tom") Nothing

The problem here, unlike in the "ideal" situation, is that we don't mention the constructor we're populating. As I see it, there are a couple ways around this:

  • Try to infer the constructor from the arguments given. This is fine until we're constructing something like Either Int Int, where the constructors' arguments are identical.

  • Type-apply some identifier of the constructor (e.g. the type-level string of its name - build @Either @"Left"). This is fine, but now we've introduced a secondary variable, and there's no functional dependency between the two. This means we (most likely) end up having to supply the constructor name even for single-constructor types, as we've told GHC the desired constructor can't always be inferred, and therefore it will probably never try. I'm sprinkling caveats as I suspect there's a glorious INCOHERENT solution here, but I'd need to think more about it.

So, this one is certainly also doable: worst case, we need a separate function, and best case, we need some heavy type-level machinery.

named (maybe fine, maybe needs duplicating)

I'll be honest, my understanding of this one is quite limited - I suspect @neongreen is far more qualified to tell you whether named works for sum types. In principle, I can't see any reason it wouldn't, but this one's a bit out of my control.

barbies (mostly not fine)

A lot of this API - bprod is a very clear example - is simply designed for product types, and the functions don't make a lot of sense with sums generally. Perhaps this isn't an issue - we can just not permit instances for sum types?

Semigroup / Monoid (not fine)

The regular instances for HKD become a bit tricky. These classes are preserved for products, but not for sums - what's mempty for HKD (Either Int String) IO? Again, we probably just don't have instances when we spot sums.


Overall, I think this is definitely something we could implement. My concern is largely that the addition of sum types would double the size of the library, but I guess any category theorist will tell you that makes perfect sense. The main reason I haven't done it yet is simply that no one's ever mentioned a use case!

If you do have a use case, I'd be happy to look into this, as I think you could definitely tick off a few of these quickly and without losing any of the (currently quite good) type inference.

I hope something in between the short and long version answers your question? 😅

@3noch
Copy link
Author

3noch commented Apr 15, 2020

That's a much more thorough answer than I was expecting! Thank you.

@3noch
Copy link
Author

3noch commented Apr 15, 2020

Some initial cursory thoughts. position @2 already seems like a questionable API in general considering ADTs are always able to contain sums and in that case the function doesn't really even make sense. Trying to find a clever meaning for it just seems counter productive. So restricting it to products seems like the only sensible thing to do, and it really is a sensible thing to do anyway. I think this same intuition applies to build which does not specify the ctor at all. Because of that, it is like position in that it doesn't really make sense in the context of a full ADT but only in the case of records. So all that said, I don't find the idea of "doubling" the API surface area troubling at all.

@3noch
Copy link
Author

3noch commented Apr 15, 2020

Regarding use cases, let's just say: We've thought about using higgledy numerous times but couldn't because we needed support for sum types!

One example is Obelisk Routes in which just about everything is HKD. We would love to share sums between routes and other parts of the app. Higgledy-style APIs would make that easier, but alas we can't use it.

@i-am-tom
Copy link
Owner

Do you have an example of current usage that you can link me? I've never seen Obelisk and the Route module is... a little overwhelming 😄

@3noch
Copy link
Author

3noch commented Apr 16, 2020

@xplat pointed out that another use case would be using Reflex's factorDyn. We often need to make higher-kinded copies of normal sums in order to use it: http://hackage.haskell.org/package/reflex-0.7.0.0/docs/Reflex-Dynamic.html#v:factorDyn

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants