[#27] Introduce Terminating constraint for preventing hanging showMemory #46

yigitozkavci · 2019-10-01T21:46:13Z

Resolves #27

Factorizes and validates input to showMemory at compile time, eliminating risk for a hanging showMemory call.

✅ Check list

New/fixed features work as expected (Bonus points for the new tests).
There are no warnings during compilation.
hlint . output is: No Hints (there are 4, none of which was caused by this PR).
The code is formatted with the [stylish-haskell][stylish-tool] tool
using [stylish-haskell.yaml][stylish] file in the repository.
The code style of the files you changed is preserved (for more specific
details on our style guide check [this document][style-guide]).
Commit messages are in the proper format.
Start the first line of the commit with the issue number in square parentheses.

Demonstraition in ghci:

> :set -XDataKinds
> :set -XTypeFamilies
> type instance UnitSymbol 3000 = "invalid1"
> type instance UnitSymbol 7000 = "invalid2"

> showMemory (toMemory @3000 $ bit 4)
<interactive>:5:1: error:
    • Value 3000 should be a terminating decimal with only factors 2 and 5 (ie. should be in form 2^x.5^y)
      but it has factor 3
    • In the expression: showMemory (toMemory @3000 $ bit 4)
      In an equation for ‘it’: it = showMemory (toMemory @3000 $ bit 4)

> showMemory (toMemory @7000 $ bit 4)
<interactive>:6:1: error:
    • Value 7000 should be a terminating decimal with only factors 2 and 5 (ie. should be in form 2^x.5^y)
      but it has factor 7
    • In the expression: showMemory (toMemory @7000 $ bit 4)
      In an equation for ‘it’: it = showMemory (toMemory @7000 $ bit 4)

> showMemory (toMemory @8192 $ bit 4)
"0.00048828125KiB"

…owMemory

yigitozkavci · 2019-10-02T05:28:39Z

Hi, a little bit context on why reduction length has increased from 201 to 250:

If left as 201, reduction depth prevents ghc from calculating "Terminating" condition for Yobibyte, which is the largest unit available in the library.

We need a depth of at least 250 for reducing Yobibyte. I don't know if more units will be added to the library, in which case we will need to increase this option again.

vrom911 · 2019-10-02T05:48:17Z

membrain.cabal

@@ -50,6 +50,7 @@ common common-options
                       -fhide-source-paths
                       -Wmissing-export-lists
                       -Wpartial-fields
+                       -freduction-depth=250


Sorry, I can't find documentation for this. (I'm looking into https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/flags.html )
Could you please explain why this is needed?

I want to add from my side that adding custom and rare flags (that apparently doesn't have documentation) might be a stopper for merging. This constant might work for natural 7000. But GHC might require a much higher constant for bigger naturals. This can slow down compilation significantly for the membrain users or produce difficult errors. The fact that this constant needs to patched to make the library work looks like an undesirable property to me.

Hi, answers inline.

Sorry, I can't find documentation for this

Yes, flag not being documented is in fact a ghc bug: https://gitlab.haskell.org/ghc/ghc/issues/15756

GHC manpage seems to have this documented though:
https://manpages.debian.org/stretch/ghc/haskell-compiler.1.en.html#Language_options

This flag controls how many steps GHC is allowed to take for simplifying a single type expression.

Could you please explain why this is needed?

In order to understand whether large Nats are only dividable by 5 or 2, but not by any other number, we need to continuously divide them by 5 and 2 and see if we end up with 1.
This creates a type expression like (((((7000 Div 5) Div 5) Div 5) Div 5)... for ghc to simplify and ghc simply has a limit on number of reductions it wants to perform.

For Yobibyte, currently the largest unit, this reduction size is exactly 250, hence the -freduction-depth=250 flag.

src/Membrain/Units.hs

vrom911 · 2019-10-02T05:51:40Z

src/Membrain/Memory.hs

+#if ( __GLASGOW_HASKELL__ >= 804 )
+type IsMemory mem = (KnownNat mem, KnownUnitSymbol mem, Terminating mem)
+#else
+type IsMemory mem = (KnownNat mem, KnownUnitSymbol mem)


I can be a bit picky, but I would call it KnownMem for better description of what this alias is.

vrom911

Also, could you please provide some tests for that. At least doctests of the examples you wrote in the PR body would be really appreciated.

vrom911

What does "factor" mean? I can't really follow your thoughts...

src/Membrain/Units.hs

chshersh

@yigitozkavci thanks for your attempt in solving this problem. But I believe that current implementation contains some serious usability issues and will make membrain less approachable. The chances of introducing a wrong memory unit are very small but the overhead of this feature is quite significant.

chshersh · 2019-10-02T06:30:15Z

membrain.cabal

@@ -50,6 +50,7 @@ common common-options
                       -fhide-source-paths
                       -Wmissing-export-lists
                       -Wpartial-fields
+                       -freduction-depth=250


I want to add from my side that adding custom and rare flags (that apparently doesn't have documentation) might be a stopper for merging. This constant might work for natural 7000. But GHC might require a much higher constant for bigger naturals. This can slow down compilation significantly for the membrain users or produce difficult errors. The fact that this constant needs to patched to make the library work looks like an undesirable property to me.

yigitozkavci · 2019-10-02T06:41:33Z

The chances of introducing a wrong memory unit are very small but the overhead of this feature is quite significant.

I completely agree with this and I'm perfectly fine with not proceeding with this PR.

This is one of the times where one should stop and think about whether introduced complexity solves a significant problem at all. This is often not the case with type level solutions, and I'm used to that.

I'm okay with closing this PR and keeping it as an attempt and demonstration of ghc's ability to prove this property at compile time.

Thanks for the review :)

vrom911 · 2019-10-03T05:15:38Z

Thanks for your work anyway! We really appreciate the effort and your time ❤️

[kowainik#27] Introduce Terminating constraint for prevent hanging sh…

2753488

…owMemory

yigitozkavci changed the title ~~[#27] Introduce Terminating constraint for prevent hanging showMemory~~ [#27] Introduce Terminating constraint for preventing hanging showMemory Oct 1, 2019

yigitozkavci added 7 commits October 1, 2019 23:07

[kowainik#27] Increase reduction depth from 201 to 500

5a7ed23

Disable GHC reduction check alltogether

8099c54

Disable reduction-depth check in library

0b72d16

Attempt to disable reduction depth check in tests

1b5e0d3

Disable reduction depth check for doctests

a401d47

Make Cabal tests also pass by giving ghc-option

040cda0

Enable terminating feature only for ghc >=8.4

906b4dd

vrom911 requested review from vrom911 and chshersh October 2, 2019 03:55

vrom911 assigned yigitozkavci Oct 2, 2019

vrom911 added enhancement New feature or request Hacktoberfest https://hacktoberfest.digitalocean.com/ type-magic Type families, type-level numbers labels Oct 2, 2019

Use reduction depth of 250 instead of unlimited

6803e23

vrom911 reviewed Oct 2, 2019

View reviewed changes

vrom911 requested changes Oct 2, 2019

View reviewed changes

src/Membrain/Units.hs Show resolved Hide resolved

yigitozkavci added 3 commits October 2, 2019 07:14

Rename IsMemory type alias to KnownMem

b6eca88

Add comments for Terminating type family

c1170f3

Improve type errors for non terminating nats

b98c9b6

chshersh suggested changes Oct 2, 2019

View reviewed changes

yigitozkavci closed this Oct 2, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[#27] Introduce Terminating constraint for preventing hanging showMemory #46

[#27] Introduce Terminating constraint for preventing hanging showMemory #46

yigitozkavci commented Oct 1, 2019 •

edited

Loading

yigitozkavci commented Oct 2, 2019

vrom911 Oct 2, 2019

chshersh Oct 2, 2019

yigitozkavci Oct 2, 2019

vrom911 Oct 2, 2019

vrom911 left a comment

vrom911 left a comment

chshersh left a comment

chshersh Oct 2, 2019

yigitozkavci commented Oct 2, 2019

vrom911 commented Oct 3, 2019

[#27] Introduce Terminating constraint for preventing hanging showMemory #46

[#27] Introduce Terminating constraint for preventing hanging showMemory #46

Conversation

yigitozkavci commented Oct 1, 2019 • edited Loading

✅ Check list

yigitozkavci commented Oct 2, 2019

vrom911 Oct 2, 2019

Choose a reason for hiding this comment

chshersh Oct 2, 2019

Choose a reason for hiding this comment

yigitozkavci Oct 2, 2019

Choose a reason for hiding this comment

vrom911 Oct 2, 2019

Choose a reason for hiding this comment

vrom911 left a comment

Choose a reason for hiding this comment

vrom911 left a comment

Choose a reason for hiding this comment

chshersh left a comment

Choose a reason for hiding this comment

chshersh Oct 2, 2019

Choose a reason for hiding this comment

yigitozkavci commented Oct 2, 2019

vrom911 commented Oct 3, 2019

yigitozkavci commented Oct 1, 2019 •

edited

Loading