Implement Natural/subtract

[ocharles]

... as standardized in dhall-lang/dhall-lang#650

[AndrasKovacs]

The commented-out qApp should be there.

If you implement something as a curried constant with a type, then you need to qApp the appropriate number of parameters, which is the number of VPrim constructors in the implementation of eval for the constant.

[ocharles]

Oh, it wasn't commented out before but it still fails to terminate with it. Let me push that.

[ocharles]

Ok, pushed that corrected version (but it still gets stuck)

[f-f]

@ocharles shouldn't NaturalTruncatedSubtract constructor be more like NaturalPlus (i.e. containing two values) than like NaturalShow? (with no values attached, which is how it is currently)

[AndrasKovacs]

@f-f yeah that would work. It's also possible to do the curried version (I'm going to paste here that in a minute), but if partial application is not possible in the syntax, there is no reason to define NaturalTruncatedSubtract as curried.

[ocharles]

I believe it's because partial application should be allowed. All the other terms are infix operators, I believe.

[AndrasKovacs]

OK, give me some time plz I'm a bit confused why this loops

[ocharles]

Of course, no rush from my part!

[sjakobi]

I guess I'm a bit late to the discussion. But wouldn't a function Natural -> Natural -> Optional Natural be slightly more useful? I mean

2 - 1 = Some 1
1 - 1 = Some 0
1 - 2 = None Natural

You could then use Optional/fold to derive truncated subtraction.

Less-than and equals operations would be very straightforward to implement.

(I suspect this was considered before but decided against for some reason?)

[ocharles]

@sjakobi See dhall-lang/dhall-lang#602 (comment) - I believe I'm implementing faithfully to the linked comment.

[AndrasKovacs]

@ocharles You forgot to add NaturalTruncatedSubtract to prettyPrimitiveExpression in Pretty/Internal.hs. There's an evil default case there suppressing the pattern match warning. It works if you fix this.

[ocharles]

Oh man, that's horrific. I knew it must have been a type class spinning somewhere, thanks for taking the time to dig into that for me!

[Gabriella439]

Yeah, the pretty-printing infinite loop is a common land-mine that people stumble upon when making contributions (myself included). If anybody knows how to fix it I'll make the change

[joneshf]

One option is to remove the default and handle the 20 other cases explicitly.

[Gabriella439]

This pull request seems to have the Lift-related work. Is that intentional?

[ocharles]

Sort of. I was lazy and didn't start from master. I could debase, but I assumed the Lift stuff would go through

[ocharles]

Note that I planned to merge them sequentially, so they will still be split into separate commits

[Gabriella439]

@ocharles: I still think we should unbundle the Lift-related changes from this pull request, otherwise we'll have to block this pull request on the other one being merged first

[ocharles]

Yep, will do. I was lazy and just thought that would have been merged by now, but it's turning out more complicated!

[ocharles]

@Gabriel439 good to merge now that the new version is out?

[ocharles]

Just remembered I need to bump the submodule, I'll do that before merging and make sure the tests pass.

[Gabriella439]

I think if you merge in master it will fix the test failure that you are running into

[ocharles]

@Gabriel439 Nope. I'm not sure dhall-lang master works with dhall-haskell yet.

[sjakobi]

@ocharles I think you should checkout dhall-lang/dhall-lang@c7082d9 for dhall-lang. The change in the failing parser test is more recent.

I believe isNormalized needs a bit more work too. Maybe up the frequency of NaturalSubtracts a bit and increase the maxSuccesses for the quickcheck test.

[sjakobi]

I believe isNormalized needs a bit more work too. Maybe up the frequency of NaturalSubtracts a bit and increase the maxSuccesses for the quickcheck test.

…at least temporarily so you can see the failing cases more reliably.

[ocharles]

Thanks for the tip @sjakobi! That did indeed reveal a problem. I think we're good to go now.