Long compile times and big 'ss' files for concrete but long types

[redfish64]

When creating a highly nested, but concrete type and using it within a do statement, idris2 generates very long ss files, and typechecking and compilation becomes very slow.

Not sure if this is a bug or not, but I ran into this while coding a rather large application with a complex chain of monad transformers.

sslen.ipkg: https://gist.github.com/redfish64/324e3fa587f885d61db6b39b920e0a46

package sslen

depends = contrib

modules = SSLen
main = SSLen
executable = ssl

SSLen.idr: https://gist.github.com/redfish64/932e5991715e9f514c80e1cb6e450166

module SSLen

import Control.Monad.Identity
import Control.Monad.Either
import Control.Monad.Trans

EM : Type -> Type
-- by adding additional outer "EitherT String (...)" constructs you can increase the size
-- of the resulting .ss file by about 2.7x and speed of compilation will decrease about
-- 4x.

-- $ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss
-- 1/1: Building SSLen (SSLen.idr)

-- real 0m1.659s
-- user 0m1.533s
-- sys  0m0.126s
-- -rwxr-xr-x 1 tim users 584978 Aug 31 10:10 ./build/exec/ssl_app/ssl.ss
-- EM = EitherT String (EitherT String (EitherT String (EitherT String Identity))) 

-- $ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss
-- 1/1: Building SSLen (SSLen.idr)

-- real 0m4.774s
-- user 0m4.490s
-- sys  0m0.282s
-- -rwxr-xr-x 1 tim users 1669083 Aug 31 10:09 ./build/exec/ssl_app/ssl.ss
-- EM = EitherT String (EitherT String (EitherT String (EitherT String (EitherT String Identity)))) 

-- $ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss
-- 1/1: Building SSLen (SSLen.idr)

-- real 0m17.049s
-- user 0m16.035s
-- sys  0m1.011s
-- -rwxr-xr-x 1 tim users 5086112 Aug 31 10:08 ./build/exec/ssl_app/ssl.ss

EM = EitherT String (EitherT String (EitherT String (EitherT String (EitherT String (EitherT String Identity))))) 

-- $ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss 
-- ls -l ./build/exec/ssl_app/ssl.ss
-- n

-- real 1m10.672s
-- user 1m6.686s
-- sys  0m3.967s
-- -rwxr-xr-x 1 tim users 16422697 Aug 31 10:06 ./build/exec/ssl_app/ssl.ss

-- EM = EitherT String (EitherT String (EitherT String (EitherT String (EitherT String (EitherT String (EitherT String Identity)))))) 

foo : EM Int
foo =
  do 
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    x <- pure 5
    pure x

main : IO ()
main =
  putStrLn $ show $ foo

Steps to Reproduce

idris2 --build sslen.idr

Expected Behavior

a small quickly built executable.

Observed Behavior

very long typechecking and compiling time, and large intermediate '.ss' files.

---

Note: Edited SSLen.idr so it actually compiles, thanks to Stefan

[stefan-hoeck]

This might be a duplicate of #1614, for which a potential fix (#1869) is in the making. If you find the time to do so, could you please try and compile your project with the fix from #1869 and report back, whether it solves this issue? Note, that the fix mainly addresses the generated file sizes but not the time taken for typechecking.

[stefan-hoeck]

OK, I had to slightly adjust the code above:

main : IO ()
main =
  putStrLn $ show $ foo { m = EM }

That right? With this and the fix mentioned above, the example in the OP builds in about 4 s on my system, producing a 44K ssl.ss file. When using the biggest transformer stack, build time increases to 16s, but the produced ssl.ss remains at 45K.

So, it looks like the main culprit will be fixed by #1869, yes?

[stefan-hoeck]

Just realized, that probably the following was intended in the OP:

foo : EM Int

This takes slightly longer to build (20 s on my system with the largest transformer stack), mainly because the CSE optimizer will have more work to do. The generated ssl.ss file remains around 45K, though.

[redfish64]

Yes, you are right. I was trying to find a workaround and unfortunately forgot to change the type of foo back to EM Int. I will fix this in the description when I have a chance.

Tim

On Tue, Aug 31, 2021, 11:04 AM Stefan Höck @.***> wrote:

Just realized, that probably the following was intended in the OP:

foo : EM Int

This takes slightly longer to build (20 s on my system with the largest transformer stack), mainly because the CSE optimizer will have more work to do. The generated ssl.ss file remains around 45K, though.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/idris-lang/Idris2/issues/1879#issuecomment-908858848, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAOVNUXVRI4MBXLLWM2ONOTT7RBELANCNFSM5DDCTNEQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[redfish64]

This might be a duplicate of #1614, for which a potential fix (#1869) is in the making. If you find the time to do so, could you please try and compile your project with the fix from #1869 and report back, whether it solves this issue? Note, that the fix mainly addresses the generated file sizes but not the time taken for typechecking.

Just tested this. With the last EM definition uncommented (with 7 EitherT's), this patch it reduces the compile time and size to:

$ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss 
1/1: Building SSLen (SSLen.idr)

real    0m12.729s
user    0m12.084s
sys 0m0.645s
-rwxr-xr-x 1 tim users 44940 Aug 31 13:03 ./build/exec/ssl_app/ssl.ss

compared to the original of:

$ time idris2 --build sslen.ipkg ; ls -l ./build/exec/ssl_app/ssl.ss 
ls -l ./build/exec/ssl_app/ssl.ss

real    1m10.672s
user    1m6.686s
sys 0m3.967s
-rwxr-xr-x 1 tim users 16422697 Aug 31 10:06 ./build/exec/ssl_app/ssl.ss

[stefan-hoeck]

So, it looks like we solved the issue with the huge generated files. However, from my own experiments it looks like time for typechecking still grows exponentially with the size of the transformer stack...