Let clauses make execution about 300 times slower

[nicolabotta]

The program

> module Main

> import NatGCD
> import NatGCDOperations
> import NatGCDProperties
> import NatGCDAlgorithm
> import NatDivisor
> import NatDivisorOperations
> import NatDivisorProperties
> import PNat
> import PNatOperations
> import PNatProperties
> import NatPositive

> %default total

> m  : Nat
> m  = 2067
> %freeze m

> x  : (Nat, PNat)
> x  = (Main.m, fromNat 616 (LTESucc LTEZero))

> d'     : PNat
> d'     = snd Main.x
> d      : Nat
> d      = toNat Main.d'
> g      : Nat
> g      = gcdAlg Main.m Main.d
> prf    : (GCD Main.g Main.m Main.d)
> prf    = gcdAlgLemma Main.m Main.d
> gDm    : (Main.g `Divisor` Main.m)
> gDm    = gcdDivisorFst Main.prf
> gDd    : (Main.g `Divisor` Main.d)
> gDd    = gcdDivisorSnd Main.prf
> qmg    : Nat
> qmg    = quotient Main.m Main.g Main.gDm
> qdg    : Nat
> qdg    = quotient Main.d Main.g Main.gDd
> zLTd   : (Z `LT` Main.d)
> zLTd   = toNatLTLemma Main.d'
> zLTqdg : (Z `LT` Main.qdg)
> zLTqdg = quotientPreservesPositivity Main.d Main.g Main.gDd Main.zLTd
> y      : (Nat, PNat)
> y      = (Main.qmg, fromNat Main.qdg Main.zLTqdg)

> main : IO ()               
> main = do putStrLn (show y)

executes in about 0.5 seconds. But it takes about 150 seconds for

> module Main

> import NatGCD
> import NatGCDOperations
> import NatGCDProperties
> import NatGCDAlgorithm
> import NatDivisor
> import NatDivisorOperations
> import NatDivisorProperties
> import PNat
> import PNatOperations
> import PNatProperties
> import NatPositive

> %default total

> m  : Nat
> m  = 2067
> %freeze m

> x  : (Nat, PNat)
> x  = (Main.m, fromNat 616 (LTESucc LTEZero))

> y  : (Nat, PNat)
> y  = let m      : Nat
>                 = fst Main.x in 
>      let d'     : PNat
>                 = snd Main.x in 
>      let d      : Nat
>                 = toNat d' in 
>      let g      : Nat
>                 = gcdAlg m d in
>      let prf    : (GCD g m d)
>                 = gcdAlgLemma m d in
>      let gDm    : (g `Divisor` m)
>                 = gcdDivisorFst prf in
>      let gDd    : (g `Divisor` d)
>                 = gcdDivisorSnd prf in
>      let qmg    : Nat
>                 = quotient m g gDm in
>      let qdg    : Nat
>                 = quotient d g gDd in
>      let zLTd   : (Z `LT` d)
>                 = toNatLTLemma d' in 
>      let zLTqdg : (Z `LT` qdg)
>                 = quotientPreservesPositivity d g gDd zLTd in
>      (qmg, fromNat qdg zLTqdg)

> main : IO ()               
> main = do putStrLn (show y)

to execute. Similarly,

> module Main

> import Fraction
> import FractionOperations
> import FractionProperties
> import PNat
> import PNatOperations
> import PNatProperties

> %default total

> x : Fraction
> x = (2067, fromNat 616 (LTESucc LTEZero)) 
> %freeze x

> y : Fraction
> y = normalize x

> main : IO ()               
> main = do putStrLn (show y)

runs in about 150 seconds. Here, normalize is implemented in terms of let expressions as in the second example. Thus, it appears that the execution speed worsens by a factor of about 300 if the same computation is expressed in terms of let clauses. The three programs can be downloaded from

https://github.com/nicolabotta/SeqDecProbs/tree/master/frameworks/14-

as NatGCDAlgorithmTest.1.lidr, NatGCDAlgorithmTest.2.lidr and FractionTest.lidr, respectively. The function normalize is implemented in FractionOperations.lidr. What is going on here?

[ziman]

It's probably the fact that let-bound values are excluded from erasure, and thus always evaluated.

I'm afraid you're stuck with where instead of let, unless we put in a workaround or extend the analysis.

[nicolabotta]

Thanks Matúš,

I was not aware of the fact that let-bound values are excluded from
erasure, blame on me!

In implementing rational numbers, I have in fact moved away from the
'where' idiom and found it easier to implement proofs via equational
reasoning in terms of 'let' clauses. Too bad.

If this is not a temporary state of affairs, it would be perhaps useful
to issue a warning if potentially erasable values are used in clauses
which are excluded from erasure analysis. This would save a lot of time
ad allow users to avoid idioms which are, from the point of view of
run-time efficiency, potentially unusable.

Best,
Nicola

Matúš Tejiščák notifications@github.com wrote:

It's probably the fact that let-bound values are excluded from erasure, and thus always evaluated.

I'm afraid you're stuck with where instead of let, unless we put in a workaround or extend the analysis.

—
Reply to this email directly or view it on GitHub.*

[ziman]

The blame is really on me because it's just feature-incompleteness of erasure analysis. There's no fundamental reason that let-bindings should be excluded from erasure, except for the fact that there has to be a point where you have to stop adding features and actually ship it.

By the way, it is not that let-bindings are completely excluded from erasure. In let x = T in M, erasure does happen inside both T and M, it's just that x is always considered used, and therefore (erased) T is always evaluated, too.

I am not sure what exactly you mean about the warning but if something does not undergo erasure analysis, you can't tell whether it is potentially erasable.

Anyway, this ought to work and I definitely don't want to discourage users from using parts of the language for no reason other than incomplete support. In (longer-term) future, let-bound values will undergo erasure, too.

[nicolabotta]

Matúš Tejiščák notifications@github.com wrote:

Anyway, this ought to work and I definitely don't want to discourage
users from using parts of the language for no reason other than
incomplete support. In (longer-term) future, let-bound values will
undergo erasure, too.

Well a factor of about 300 (we can provide examples for which this
figure is much higher) in execution speed seems a very good reason to me
for avoiding specific language constructs.

This is particularly true in libraries which implements numerical types.

I have spent a few months (ok, say a few smartman-days or weeks)
implementing rationals to get to the point that it takes minutes to
compute 2067/616 + 32/11 when, in fact, it should take almost
nothing. This just because I started to find long sequences of 'where'
clauses a bit boring ...

Maybe you can have a look at lines 266-374 of

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/FractionProperties.lidr

and then tell me if you think it makes any sense to stick to 'let'
clauses or whether I should better start the rewriting exercise.

[nicolabotta]

As it turns out, it is possible to recover the expected run-time behavior by just reimplementing normalize in FractionOperations.lidr. In the current revision, I have left the let-based implementation commented out for testing purposes. With normalize implemented in terms of where one obtains

nicola@cirrus:/github/SeqDecProbs/frameworks/14-$ idris -p contrib FractionTest.lidr -o a.out
nicola@cirrus:/github/SeqDecProbs/frameworks/14-$ time ./a.out
(2067, 616)
real 0m0.574s
user 0m0.560s
sys 0m0.008s

With normalize implemented in terms of let one gets

nicola@cirrus:/github/SeqDecProbs/frameworks/14-$ idris -p contrib FractionTest.lidr -o a.out
nicola@cirrus:/github/SeqDecProbs/frameworks/14-$ time ./a.out
(2067, 616)
real 2m49.747s
user 2m49.812s
sys 0m0.040s

From my perspective the issue is closed. I have learned a useful lesson and, for the time being, I will stay away from let clauses.

I believe that the potential drawbacks of using 'let' clauses should be documented and that developers should be made aware of the essential differences between where and let clauses w.r.t. erasure but I do not have a concrete suggestion as to how to do so.

Thanks to Matus who essentially contributed to solve my problem! I leave it to him or to those who better know, to decide whether to close the issue or to keep it open.

If you are interested in using non-negative rational numbers in Idris, please get in touch.

[ahmadsalim]

I think this is related to #172 and #3199, so I will close it as a duplicate if it is OK.

[ahmadsalim]

Sorry, it seems I misunderstood from the title. In any case the problem was solved and so it needs to close.

[ziman]

This problem is still not solved. The two bugs you linked are related to typechecking. However, the problem in this issue is that runtime is slower.

With TTstar, let bindings are properly erased as well. When that will land in Idris, I don't know. As a hotfix, we could probably reduce let bindings away by substitution, but I'm not sure whether that's worth it.

[ahmadsalim]

@ziman Yeah, I already apologized for that :).

[ahmadsalim]

I will reopen the issue, as I think I thought you provided an answer, but it was only a workaround.