Improve inference #16

treeowl · 2019-07-24T19:02:19Z

The original concept of this API is to work "over", "under", or
"a la" a single newtype, potentially changing its type arguments
but not changing it wholesale. Back in the day, Haskell couldn't
express that idea, but now it can (for the most part). We can take
advantage of that to improve inference and typed hole error messages.

Fixes #15

Additionally, remove support for GHC versions before 8.4. These have pretty horribly brittle support for Coercible (7.10 being especially different and 8.2 being especially flaky), so supporting them is a bit nightmarish.

treeowl · 2019-07-24T20:05:52Z

Whew! Looks like I got this, pretty much. There are some ugly tricks to pull for 7.10, and I have no idea why 8.2 rejects my example (presumably a compiler bug), but it looks like the overall idea works. I'm guessing this is probably pretty close to McBride's original intention, which wasn't yet expressible in Haskell at the time. Inference should be quite powerful.

treeowl · 2019-07-24T20:42:55Z

The major limitation of this version is that newtypes with kind arguments aren't fully supported. That is, given newtype Foo k (a :: k) = ..., n and n' must have the same k. I think that's okay. The main point of this module is convenience, and giving up rarely-needed flexibility for good inference seems appropriate in that context.

treeowl · 2019-07-24T21:00:53Z

@sjakobi, @chessai, do you think it would be okay to require GHC ≥ 8.4? Coercible seems pretty darn brittle in earlier versions. When faced with my test case, 8.2 complains it can't match the representation of Sum Int with that of Int. Clearly I've run into some dark corner there.... But even without the fancy inference machinery, things seem pretty sensitive until 8.4.

src/Control/Newtype/Generic.hs

chessai · 2019-07-24T22:51:51Z

I am definitely okay with that.

src/Control/Newtype/Generic.hs

treeowl · 2019-07-25T00:38:14Z

@chessai any general opinions on this PR?

treeowl · 2019-07-25T02:20:46Z

@kcsongor has a filthy trick that can probably improve some of the type errors when people misuse these functions.

treeowl · 2019-07-25T17:50:58Z

@sjakobi Have you any thoughts?

The original concept of this API is to work "over", "under", or "a la" a *single* newtype, potentially changing its type arguments but not changing it wholesale. Back in the day, Haskell couldn't express that idea, but now it can (for the most part). We can take advantage of that to improve inference and typed hole error messages. Fixes love-haskell#15

treeowl · 2019-07-25T21:07:28Z

The error messages actually turned out to be much more reasonable than I feared! I do with that :t were a little friendlier to this module, but at least :i. is good. I don't know if there are good tricks for improving :i or not...

`Coercible` seems to be really fragile under GHC versions before 8.4. 8.2 seems especially fussy: even when the package compiles, use cases may fail mysteriously.

treeowl · 2019-07-25T21:49:43Z

I am having a bit of trouble getting my custom type error to fire. I'll have to see if I can fix that.

The custom "not a newtype" error wasn't showing up where I wanted it to. Make that happen.

treeowl · 2019-07-25T23:26:28Z

All right. I think I fixed the custom error issue. I couldn't get @kcsongor's dirty trick to improve things here without simultaneously making other things worse, so I think we should skip that. The basic annoyance is that GHC (in :t and type errors) really wants to simplify constraints, which expands friendly-looking things like Newtype n o into garbage. Csongor's trick uses overlapping instances for an otherwise completely unused type to delay the simplification. But this causes us other trouble that seems more serious; we really want GHC to simplify constraints when doing so actually reveals new information. Oh well.

treeowl · 2019-07-26T00:02:34Z

Is that extra flexibility of not requiring n to be a direct newtype around o sufficiently useful to justify the extra documentation complexity? I don't have a clear feeling about it one way or the other.

sjakobi

Wow, cool stuff! The type inference is great!

The whole thing goes a bit over my head though so I hope you don't mind if I ping you if issues come up, @treeowl.

sjakobi · 2019-07-26T00:31:54Z

src/Control/Newtype/Generic.hs

+-- @Const Int Char@ and @Const Int Maybe@ are not @Similar@
+-- because they have different kind arguments.
+class Similar (n :: k) (n' :: k)
+instance (Similar' n n', Similar' n' n) => Similar n n'


I think this would be easier to read if the name Similar was easier to distinguish from the name for Similar'.

Unfortunately, users will end up seeing Similar', which is fundamentally an implementation detail, in error messages and GHCi :t responses. I don't know of any way to avoid this without causing other problems. So either I can document that internal thing or I can pick a name that's close enough for people to guess the meaning. Bleh!

I'd appreciate a bit of documentation for Similar' in any case!

treeowl · 2019-07-26T01:21:31Z

The whole thing goes a bit over my head though so I hope you don't mind if I ping you if issues come up, @treeowl.

For sure. I should add some more comments. The trickiest bit is Similar. We really want n to give us information about n'. It's also nice (for typed holes and error messages, particularly) if n' gives us information about n. Since we may know nothing, a priori, about one of those, we have to be a bit careful not to force a match on one when the other is the one with information. The horrible way to do that (even worse :t results!) is with INCOHERENT typeclass instances. Ignoring that awfulness, the thing to do is to require n' to have a structure calculated from n and the other way around, "in parallel". Similar' n n' matches on n, producing a constraint. Suppose we have n ~ F a b. Then we get

Similar' (F a b) n'
==>
(Similar' (F a) (GetFun n'), n' ~ GetFun n' (GetArg n'))

We have now constrained things only a little: n' is required to have the form p q for some p and q, where F a and p have the same kind and b and q have the same kind. Substituting in p and q, we continue:

(Similar' (F a) p, n' ~ p q)
((Similar' F (GetFun p), p ~ GetFun p (GetArg p)), n' ~ p q)

Let's set r ~ GetFun p and s ~ GetArg p. Then

((Similar' F r, p ~ r s), n' ~ p q)

We've now reached the base case! Yay! So the last step is

((F ~ r, p ~ r s), n' ~ p q)

which then simplifies to

n' ~ F s q

Undoing the substitutions we made,

n' ~ F (GetArg (GetFun n')) (GetArg n')

The arguments in that constraint are completely useless (as far as I know), but we need to put it all together like that to get what we're after: an equality constraint on n' itself that lets GHC know it's F x y for some x and y to be determined. Very often, those are then fixed by the type o' and the Newtype n' o' constraint, which at first seems backwards. Say we consider Sum. We have

type Rep (Sum a) = M1 _ _ (M1 _ _ (M1 _ _ (K1 _ a)))

This can reduce as soon as GHC sees we have Sum whatever! So then the NewtypeF-calculated constraint can constrain the type argument to whatever's required to wrap the new contents. Magic! Yeah, this comment should go in the code.....

treeowl · 2019-07-26T01:42:55Z

I'm definitely leaning toward requiring Newtype n o as well as Newtype n' o', even though it's not strictly necessary. I think it makes for a better story to tell users about an already somewhat intimidating API. Please let me know what you think about that.

Force `o` to be the underlying type of `n`. I think this makes for a better story to tell users.

treeowl · 2019-07-26T16:05:51Z

I've expanded the documentation considerably, and, in a separate commit, imposed the tighter constraints I mentioned. Let me know what you think.

treeowl · 2019-07-28T17:09:51Z

@sjakobi, have you had a chance to consider this further? Do you have any more questions?

sjakobi · 2019-07-29T09:47:49Z

Thank you @treeowl!

chessai · 2019-07-29T10:51:14Z

Sorry for not helping out here; I've been indisposed recently and didn't want to devote too much brainpower to any one task.

sjakobi · 2019-07-29T11:49:12Z

@chessai No worries! Get well soon! :)

treeowl commented Jul 24, 2019

View reviewed changes

src/Control/Newtype/Generic.hs Outdated Show resolved Hide resolved

treeowl commented Jul 24, 2019

View reviewed changes

src/Control/Newtype/Generic.hs Outdated Show resolved Hide resolved

src/Control/Newtype/Generic.hs Outdated Show resolved Hide resolved

treeowl force-pushed the patch-2 branch from ae15484 to dc44224 Compare July 25, 2019 21:02

treeowl force-pushed the patch-2 branch from dc44224 to b29241a Compare July 25, 2019 21:04

treeowl changed the title ~~WIP similarity~~ Improve inference Jul 25, 2019

Remove support for older GHC

bc6a74b

`Coercible` seems to be really fragile under GHC versions before 8.4. 8.2 seems especially fussy: even when the package compiles, use cases may fail mysteriously.

treeowl force-pushed the patch-2 branch from b29241a to bc6a74b Compare July 25, 2019 21:08

Improve errors a bit

e32c3fb

The custom "not a newtype" error wasn't showing up where I wanted it to. Make that happen.

More documentation

483c865

sjakobi reviewed Jul 26, 2019

View reviewed changes

treeowl added 2 commits July 26, 2019 11:49

More comments

85b80b3

Constrain all the newtypes

96e6cc8

Force `o` to be the underlying type of `n`. I think this makes for a better story to tell users.

sjakobi merged commit 3e7a3ee into love-haskell:master Jul 29, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve inference #16

Improve inference #16

treeowl commented Jul 24, 2019 •

edited

Loading

treeowl commented Jul 24, 2019

treeowl commented Jul 24, 2019

treeowl commented Jul 24, 2019

chessai commented Jul 24, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 26, 2019

sjakobi left a comment •

edited

Loading

sjakobi Jul 26, 2019

treeowl Jul 26, 2019

sjakobi Jul 26, 2019

treeowl commented Jul 26, 2019 •

edited

Loading

treeowl commented Jul 26, 2019 •

edited

Loading

treeowl commented Jul 26, 2019

treeowl commented Jul 28, 2019

sjakobi commented Jul 29, 2019

chessai commented Jul 29, 2019

sjakobi commented Jul 29, 2019

Improve inference #16

Improve inference #16

Conversation

treeowl commented Jul 24, 2019 • edited Loading

treeowl commented Jul 24, 2019

treeowl commented Jul 24, 2019

treeowl commented Jul 24, 2019

chessai commented Jul 24, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 25, 2019

treeowl commented Jul 26, 2019

sjakobi left a comment • edited Loading

Choose a reason for hiding this comment

sjakobi Jul 26, 2019

Choose a reason for hiding this comment

treeowl Jul 26, 2019

Choose a reason for hiding this comment

sjakobi Jul 26, 2019

Choose a reason for hiding this comment

treeowl commented Jul 26, 2019 • edited Loading

treeowl commented Jul 26, 2019 • edited Loading

treeowl commented Jul 26, 2019

treeowl commented Jul 28, 2019

sjakobi commented Jul 29, 2019

chessai commented Jul 29, 2019

sjakobi commented Jul 29, 2019

treeowl commented Jul 24, 2019 •

edited

Loading

sjakobi left a comment •

edited

Loading

treeowl commented Jul 26, 2019 •

edited

Loading

treeowl commented Jul 26, 2019 •

edited

Loading