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

SuperComposition instance resolution is brittle #265

Open
treeowl opened this issue May 9, 2022 · 2 comments · May be fixed by #267
Open

SuperComposition instance resolution is brittle #265

treeowl opened this issue May 9, 2022 · 2 comments · May be fixed by #267

Comments

@treeowl
Copy link

treeowl commented May 9, 2022

In GHCi:

ghci> :t ("b"++)
("b"++) :: [Char] -> [Char]
ghci> :t ('b':)
('b':) :: [Char] -> [Char]

ghci> :t (++"a") ... ("b"++)
(++"a") ... ("b"++) :: [Char] -> [Char]
ghci> :t (++"a") ... ('b': )

<interactive>:1:9: error:
    • Couldn't match type: [Char]
                     with: [Char] -> [Char]
        arising from a use of ‘...’
    • In the expression: (++ "a") ... ('b' :)

Ouch! I'd be tempted to go with something simpler:

infixl 8 ...

class SuperComposition x y b r | x y b -> r where
  (...) :: (x -> y) -> b -> r

instance {-# OVERLAPPABLE #-} (x ~ b, y ~ r) => SuperComposition x y b r where
  f ... g = f g
  {-# INLINE (...) #-}

instance {-# OVERLAPPING #-} (SuperComposition x y d r1, r ~ (c -> r1)) => SuperComposition x y (c -> d) r where
  (f ... g) c = f ... g c
  {-# INLINE (...) #-}

I used four parameters instead of three to be able to infer directly that the first argument of (...) is a function. We could do that with three parameters too, but it gets a little hacky and I don't see a real advantage.

treeowl added a commit to treeowl/universum that referenced this issue May 9, 2022
* Use overlapping instances instead of incoherent ones. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
treeowl added a commit to treeowl/universum that referenced this issue May 9, 2022
* Use overlapping instances instead of incoherent ones. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
treeowl added a commit to treeowl/universum that referenced this issue May 9, 2022
* Use overlapping instances instead of incoherent ones. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
@treeowl
Copy link
Author

treeowl commented May 10, 2022

I'm struggling to find a solution that doesn't break too much code. As I understand it, we want

(...) :: (x -> y) -> x -> y
(...) :: (x -> y) -> (m -> x) -> (m -> y)
(...) :: (x -> y) -> (m -> n -> x) -> (m -> n -> y)
-- etc.

I see two basic approaches to this, starting from

class SuperComposition x y b r | x y b -> r where
  (...) :: (x -> y) -> b -> r

Analyze the second argument type

This requires the type checker to be able to determine exactly how many arrows
are in the second argument. This is, roughly speaking, what we currently do, but with more principled overlap to avoid brittleness.

instance {-# OVERLAPPABLE #-} (x ~ b, y ~ r) => SuperComposition x y b r where
  f ... g = f g

instance {-# OVERLAPPING #-} (SuperComposition x y d r1, r ~ (c -> r1)) => SuperComposition x y (c -> d) r where
  (f ... g) c = f ... g c

Compare the result types

This requires the type checker to know the result type (or at least a whole lot about it), but it works great in that case.

instance {-# OVERLAPPABLE #-} (b ~ (b1 -> b'), r ~ (b1 -> r'), SuperComposition x y b' r') => SuperComposition x y b r where
  (f ... g) c = f ... g c

instance {-# OVERLAPPING #-} x ~ b => SuperComposition x r b r where
  f ... g = f g

There are different trade-offs, and neither of them seems to "just work" in an intuitive way. When they don't work out, the error messages can be rather bad, because of the way GHC picks an instance to complain about in the face of overlap. I suspect we might be able to combine the approaches: use an auxiliary class that takes as an argument the result of a type family comparing the results, and play some {-# INCOHERENT #-} tricks. It will require some care to get this right, and I am not terribly optimistic about the user experience even if we succeed, but the current situation is just awful.

treeowl added a commit to treeowl/universum that referenced this issue May 11, 2022
* Use overlapping instances instead of incoherent ones. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
treeowl added a commit to treeowl/universum that referenced this issue May 11, 2022
* Use type families and an auxiliary class to make instance resolution
  for `SuperComposition` more robust and predictable. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
@treeowl treeowl linked a pull request May 11, 2022 that will close this issue
9 tasks
treeowl added a commit to treeowl/universum that referenced this issue May 11, 2022
* Use type families and an auxiliary class to make instance resolution
  for `SuperComposition` more robust and predictable. Fixes serokell#265.

* Make the first argument of `...` a function unconditionally, before
  instance selection. This can theoretically improve inference slightly,
  though it probably doesn't have much impact in practice.
@treeowl
Copy link
Author

treeowl commented May 11, 2022

OK, I think I've come up with a fairly reasonable solution in #267. It's not beautiful, and it's not friendly, but I believe it offers exactly as much type inference as possible without losing polymorphism.

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