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

Exponential runtime due to defaulting? #1761

Open
weaversa opened this issue Oct 3, 2024 · 1 comment
Open

Exponential runtime due to defaulting? #1761

weaversa opened this issue Oct 3, 2024 · 1 comment
Labels
design needed We need to specify precisely what we want

Comments

@weaversa
Copy link
Collaborator

weaversa commented Oct 3, 2024

Here we find a simple sequence comprehension that exhibits exponential runtime when Cryptol defaults a type, though when we explicitly type the sequence (to the same that Cryptol defaulted the sequence to) we see the expected linear time runtime. The traceVal is added to more easily demonstrate this odd behavior, but the behavior happens w/out it (feel free to remove traceVal and experience the runtime with both fibs@20. I could not get fibs@30 (with defaulting) to even finish.)

Main> let fibs = [0, 1] # [ traceVal "a + b" (a + b) | a <- fibs | b <- tail fibs ]
Main> fibs@6
Showing a specific instance of polymorphic result:
  * Using 'Integer' for 1st type argument of '<interactive>::fibs'
a + b 1
a + b 1
a + b 2
a + b 3
a + b 1
a + b 2
a + b 1
a + b 1
a + b 2
a + b 3
a + b 5
a + b 8
8
Main> let fibs = [0:Integer, 1] # [ traceVal "a + b" (a + b) | a <- fibs | b <- tail fibs ]
Main> fibs@6
a + b 1
a + b 2
a + b 3
a + b 5
a + b 8
8
@mccleeary-galois mccleeary-galois added the bug Something not working correctly label Oct 11, 2024
@yav
Copy link
Member

yav commented Oct 28, 2024

So, that's not exactly a bug, although clearly it's undesirable.

The issue is that even though the first fib looks like a value, it is a polymorphic value, and as such it is actually a function of the type (note the fibs can behave quite differently depending on what type it is instantiated with, for example try fibs`{[1]}).

In contrast, the second example is indeed just an ordinary value and it would be cached, as expected.

Note that the defaulting that's happening here is too late---fibs is still a polymorphic function, the defaulting just provides its type parameter: we do not, however, rewrite the body of the function, it is still a polymorphic function.

This is an issue in Haskell too, and the choice the designers made in that context is to have the "monomorphism restriction", which says that things that don't look like functions (e.g., fibs above) cannot be polymorphic, unless they have an explicit type signature, so that it is obvious what's happening. While we could implement some such thing, the experience with Haskell has been that this restriction can be quite annoying, and folks tend to disable it. This is likely to be even more the case in Cryptol, where being polymorphic in numeric types is quite common.

I think we have a few possible choices:
A) Easiest: emit a warning when something looks like a value but is actually a function, and there is no explicit type signature (so like a "weak" monomorphism restriction)
B) Medium: like (A) but instead of issuing a warning default the definition if possible, so it would become automatically monomorphic
C) Most complicated: modify the interpreter to somehow cache functions that only have type arguments.

My vote would be for (A) or (B), because replicating (C) would be pretty hard to do in the Cryptol compiler

@mccleeary-galois mccleeary-galois removed the bug Something not working correctly label Oct 28, 2024
@yav yav added the design needed We need to specify precisely what we want label Oct 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
design needed We need to specify precisely what we want
Projects
None yet
Development

No branches or pull requests

3 participants