unexpected slowness (non-recursive)

[zraffer]

trafficstars

There are files with terms in this directory (to be root) in the commit https://github.com/groupoid/om/tree/ac585365a69d8dcd6c43a31a424486d5718c2522/priv/barbers/Hurkens/lambda (also available as a gist here https://gist.github.com/zraffer/dc90b5d076eda6156277 ), a few of which take a very long time to typecheck and normalize. Especially ShadowTrans and Shadow-MkOk. The terms do not use recursion and need just a few reductions to normalize. Moreover, usage of this terms in simple expressions (call id for example --- file test/Shadow-MkOk as well as othes files in that directory) take much more time, so typechecking seems to have exponential time complexity in such cases. Therefore long typechecking time for simple terms makes morte unusable for development.

Older versions (since 1.1) from hackage were tested producing the same time results. However fully normalized versions of the terms (from morte output, at https://github.com/groupoid/om/tree/ac585365a69d8dcd6c43a31a424486d5718c2522/priv/barbers/Hurkens/output ) have got typechecked immediately (no slowness).

[Gabriella439]

I have a pretty good guess at what the problem is and how to fix it. The issue is (probably) this line of code:

https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Import.hs#L285

Whenever morte embeds a remote expression morte type-checks the expression first, for two separate reasons:

• First, morte needs to verify that the imported expression is closed (i.e. no free variables). morte requires this invariant in these two places:

  https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs#L488 https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs#L510

• Second, morte type-checks expressions upon import to give better error messages. This is how morte can give you the import trace to the expression in the import graph that failed to type-check like:

  morte: 
  ⤷ #foo
  ⤷ #bar
  {some type error here}
  

However, in the worst case this type-checking of imports can lead to quadratic behavior, type-checking the exact same expression multiple times.

The fix is simple: instead of type-checking imports we only verify that they are closed expressions. This means that error messages will be a little bit worse for imports, but we can always re-implement that later more efficiently once I add support for annotating expressions with source/import locations.

This also explains why fully resolved expressions are type-checked much more quickly. It's actually not the normalization process that's slow, but rather the import resolution step that is slow.

A really easy way to verify that this is indeed the problem for you is to just delete the type-checking step that I linked to above and check to see if type-checking gets much faster. Later I can fix this code to only check that the import is closed (or you can contribute the pull request if you get to it before me).

[Gabriella439]

Actually, I found an even better solution, which was to just not even type-check an import if it was already cached (since being in the cache implies that it was already type-checked). See the associated commit for more details

[5HT]

On old version:

$ time ./morte < Shadow-MkOk
real    3m29.352s
user    3m26.926s
sys    0m1.753s

On latest version:

$ time ./morte < Shadow-MkOk
real    11m16.725s
user    10m59.802s
sys 0m8.546s

[zraffer]

@Gabriel439 , did you checked your fix on the proposed gist? It seems that fixed Morte is more slow.

[Gabriella439]

No, I haven't checked on the proposed gist. However, the slowdown is unusual since it should always be doing strictly less work. See the diff to see what I mean.

Are you checking exactly before and after that commit (i.e. on ba318b262240fe1aafb89c8ba91737fe899d6249 vs 6b363de017adc58543c77868d3955b176728729f)? The reason I ask is that I made another change a few commits earlier that might also affect performance, which was changing how Context manipulation worked, and I want to make sure that's not causing the performance degradation.

[Gabriella439]

Okay, so the latest commit to add support for caching was not responsible for the slowdown; it had no effect on speed in my test:

$ time morte < ShadowTrans # after caching
...
real    2m33.028s
user    2m32.568s
sys 0m0.512s
$ time morte < ShadowTrans # before caching
...
real    2m32.917s
user    2m7.512s
sys 0m25.488s

I'm now testing whether or not the recent changes to the Context type are responsible for the slowdown.

[Gabriella439]

Yep, it looks like the changes to Context handling contributed to the slowdown. Here is the timing when I switch to the old Context implementation:

$ time morte < ShadowTrans
...
real    0m57.867s
user    0m57.692s
sys 0m0.196s

I did this change to Context to improve the time complexity of some expensive Context-related operations (such as for encoding strings) but it looks like it gave a constant factor slowdown. I'll see if I can get it to match the old performance.

[5HT]

Me too removed caching as it has no drastical effect on tests running. BTW:

$ time om type a "#ShadowTrans" , mode src-hurkens
real    0m4.972s
user    0m3.897s
sys 0m1.666s

[Gabriella439]

Alright, so I reverted back to the old Context implementation on master so that it should at least be the same speed as before.

I'm still investigating the source of the slowness and profiling has narrowed this down to the type-checking step