Type checking times again!
Opened this issue · 12 comments
I ran into another example which takes ages to type check. Here's the code
> import Syntax.PreorderReasoning
> import NonNegRational
> import NonNegRationalBasicOperations
> import NonNegRationalBasicProperties
> import NatPositive
> import Fraction
> import FractionNormal
> import FractionPredicates
> import FractionBasicProperties
> import PNat
> import PNatOperations
> import PNatProperties
> %default total
> %access public export
> %auto_implicits off
> ||| The sum of n terms of the form 1/(S m) is n/(S m)
> lala : (n : Nat) -> (m : Nat ) ->
> sum (replicate n (fromFraction (1, Element (S m) MkPositive))) = fromFraction (n, Element (S m) MkPositive)
> lala Z m =
> let Sm' = Element (S m) MkPositive in
> let SZ' = Element 1 MkPositive in
> ( sum (replicate Z (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum Nil )
> ={ Refl }=
> ( fromFraction (0, SZ') )
> ={ fromFractionEqLemma (0, SZ') (0, Sm') Refl }=
> ( fromFraction (0, Sm') )
> QED
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
> ={ cong (lala n m) }=
> ( fromFraction (1, Sm') + fromFraction (n, Sm') )
> ={ fromFractionLinear (1, Sm') (n, Sm') }=
> ( fromFraction ((1, Sm') + (n, Sm')) )
> ={ Refl }=
> ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
> ={ cong (sym (multDistributesOverPlusLeft 1 n Sm)) }=
> ( fromFraction ((1 + n) * Sm, Sm' * Sm') )
> ={ multElimRight (1 + n) Sm' Sm' }=
> ( fromFraction (1 + n, Sm') )
> ={ cong (plusOneSucc n) }=
> ( fromFraction (Sn, Sm') )
> QED
On a fresh installation of https://github.com/nicolabotta/SeqDecProbs, you should be able to just do
$ cd SeqDecProbs/frameworks/14-
$ make testTypeCheckingSpeed
On a reasonably fast processor (Xeon E5-2667 v3 8C, 3.2GHz) it should take a few minutes to type check the dependencies of TestTypeCheckingSpeed.lidr
and more than ... one hour to (fail to?) type check TestTypeCheckingSpeed.lidr
itself!
I am not sure that this problem is an instance of #3199. I have tried to prevent expanding features by a careful use of %freeze
directives with no success.
There must be something pathological in the example above. But, generally speaking, I have the impression that type checking proofs of properties of specific Num
implementations has become very time consuming lately.
Again, I have not done any systematic attempt at finding out whether this is a regression (as I did for #3209) but I have the impression that type checking times have worsened over the last weeks. I might be wrong, of course.
Any idea how to get back to acceptable type checking times? This having to wait for hours is starting to become a bit annoying!
I can now confirm that the program eventually fails to type check. But it takes about 5 hours (14 hours on my laptop) to do so! What is going on here?
I think issue is the same as #172 which is that the Idris type checker does complete normalization instead of just to whnf-form. I am unsure if there is a particular satisfying workaround for your current issue.
It would probably take less time if there were less terms in pre-order syntax reasoning, but that affects readability.
I think issue is the same as #172 which is that the Idris type checker does complete normalization instead of just to whnf-form.
You are probably right but there might be something more than #172 (or #3199) at stake here. The facts look like the following: type checking the base case and
> lala (S n) m = ?guga
takes about 2 minutes to succeed. Type checking the base case and
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ ?lala }=
> ( fromFraction (Sn, Sm') )
> QED
takes about two minutes to fail. Here, the error message is
Type checking ./TestTypeCheckingSpeed.lidr
TestTypeCheckingSpeed.lidr:35:6:When checking right hand side of lala with expected type
sum (replicate (S n) (fromFraction (1, Element (S m) MkPositive))) =
fromFraction (S n, Element (S m) MkPositive)
Can't infer type for {letval115}
suggesting that something strange might be happening. Type checking the base case and
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ ?lala }=
> ( fromFraction (Sn, Sm') )
> QED
also fails in about two minutes and with the same error message. Even
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
> ={ cong (lala n m) }=
> ( fromFraction (1, Sm') + fromFraction (n, Sm') )
> ={ ?lala }=
> ( fromFraction (Sn, Sm') )
> QED
fails to type check in only about 4 minutes and, again, with the same error message! It is only when one tries to type check the base case with
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
> ={ cong (lala n m) }=
> ( fromFraction (1, Sm') + fromFraction (n, Sm') )
> ={ fromFractionLinear (1, Sm') (n, Sm') }=
> ( fromFraction ((1, Sm') + (n, Sm')) )
> ={ ?lala }=
> ( fromFraction (Sn, Sm') )
> QED
that type checking times start to diverge to values of the order of hours. At this point, freezing fromFraction
brings type checking times down to about 10 seconds, again, with the above error message. This supports your hypothesis that this issue is just another aspect of #172 or #3199.
However, the base case with
> lala (S n) m =
> let Sm' = Element (S m) MkPositive in
> let Sm = toNat Sm' in
> let Sn = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
> ={ cong (lala n m) }=
> ( fromFraction (1, Sm') + fromFraction (n, Sm') )
> ={ fromFractionLinear (1, Sm') (n, Sm') }=
> ( fromFraction ((1, Sm') + (n, Sm')) )
> ={ ?guga }=
> ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
> ={ ?lala }=
> ( fromFraction (Sn, Sm') )
> QED
fails to type check (again, with frozen fromFraction
, in a few seconds) with another suspicious error message:
When checking argument x to function Syntax.PreorderReasoning.Equal.step:
Type mismatch between
fromFraction (plus (getWitness (fromFraction (1, Sm')))
(getWitness (fromFraction (n, Sm')))) (Inferred value)
and
fromFraction ((1, Sm') + (n, Sm')) (Given value)
Specifically:
Type mismatch between
plus
and
MkPair
Here, it seems that the type checker is using a wrong version of plus
. Thus, it appears that we have to do with problems related with complete normalization but also with possibly erroneous error messages. Any idea what {letval115} means and where the type mismatch between plus
and MkPair
could come from?
The {letval155}
is machine generated name for the assigned value of one of the let
-bindings you have. I am not sure why you get the error message however.
I do not know either but replacing
> let Sm' = Element (S m) MkPositive in
with
> let Sm' : PNat = Element (S m) MkPositive in
makes the
Can't infer type for {letval115}
error disappear. We are now left with the second error (and with the problem of understanding why the type of Sm'
cannot be inferred).
I think issue is the same as #172 ...
You are probably right! The code
> import Syntax.PreorderReasoning
> import NonNegRational
> import NonNegRationalBasicOperations
> import NonNegRationalBasicProperties
> import NatPositive
> import Fraction
> import FractionNormal
> import FractionPredicates
> import FractionBasicOperations
> import FractionBasicProperties
> import PNat
> import PNatOperations
> import PNatProperties
> %default total
> %access public export
> %auto_implicits off
> %freeze fromFractionLinear
> %freeze fromFraction
> ||| The sum of n terms of the form 1/(S m) is n/(S m)
> lala : (n : Nat) -> (m : Nat ) ->
> sum (replicate n (fromFraction (1, Element (S m) MkPositive))) = fromFraction (n, Element (S m) MkPositive)
> lala Z m =
> let Sm' = Element (S m) MkPositive in
> let SZ' = Element 1 MkPositive in
> ( sum (replicate Z (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum Nil )
> ={ Refl }=
> ( fromFraction (0, SZ') )
> ={ fromFractionEqLemma (0, SZ') (0, Sm') Refl }=
> ( fromFraction (0, Sm') )
> QED
> lala (S n) m =
> let Sm' : PNat = Element (S m) MkPositive in
> let Sm : Nat = toNat Sm' in
> let Sn : Nat = S n in
> ( sum (replicate (S n) (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
> ={ Refl }=
> ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
> ={ cong {f = \ X => fromFraction (1, Sm') + X} (lala n m) }=
> ( fromFraction (1, Sm') + fromFraction (n, Sm') )
> ={ sym (fromFractionLinear (1, Sm') (n, Sm')) }=
> ( fromFraction ((1, Sm') + (n, Sm')) )
> ={ cong {f = fromFraction} Refl }=
> ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
> ={ cong {f = \ X => fromFraction (X, Sm' * Sm')} (sym (multDistributesOverPlusLeft 1 n Sm)) }=
> ( fromFraction ((1 + n) * Sm, Sm' * Sm') )
> ={ multElimRight (1 + n) Sm' Sm' }=
> ( fromFraction (1 + n, Sm') )
> ={ cong {f = \ X => fromFraction (X, Sm')} (plusOneSucc n) }=
> ( fromFraction (Sn, Sm') )
> QED
type checks in about 20 seconds. But commenting out
> %freeze fromFractionLinear
> %freeze fromFraction
increases the type checking time to hours! It will be interesting to see whether type checking based on whnf-form will make it possible to type in reasonable times and without having to introduce ad-hoc %freeze
directives.
I've been playing around with WHNF, and it's not actually clear to me now that it's always going to be a win in practice. Even here, it would end up having to reduce fromFraction to get at the relevant head, and it's clear from the %freeze that unification can make progress even avoiding that.
I'm reading around what other systems do - there must be a good strategy lurking somewhere.
Thanks Edwin! I am going to post a self-contained example that exhibits a similar behavior. Best, Nicola
As an update, I have found the cause of recent slow downs, which is to do with partial evaluation doing too much work. I'll aim to fix this later this week, but in the meantime you can probably get much better (compile time) performance with --no-partial-eval
@edwinb Maybe it's a good time to consider having multiple optimization levels?
@ahmadsalim we already do, in a sense, but that's nothing to do with the problem here. The partial evaluator does too much work and that is a bug (it's repeating work it's done before), not a failure in setting the right optimisation levels.
@edwinb Hmm ... I do not see improvements with the --no-partial-eval
option, my type checking times are:
- 20s with frozen
fromFractionLinear
,fromFraction
, standard flags - 20s with frozen
fromFractionLinear
,fromFraction
, standard flags +--no-partial-eval
- 31m with no freezing, standard flags
- 30m with no freezing standard flags +
--no-partial-eval
This is with Idris-dev-ff776da which I'm sticking to essentially because of #3405. Is it possible that --no-partial-eval
improves the type checking times with more recent Idris versions but not with ff776da?