Hello there.
I'm observing a performance issue with current master when I import a module that uses instances. I have the following module, Sub1, which is imported from another module, Top.
open import Data.Nat using (ℕ ; NonZero ; _^_ ; _%_)
open import Data.Nat.Properties using (m^n≢0)
module Sub1 (bits : ℕ) where
instance
2^bits≢0 : NonZero (2 ^ bits)
2^bits≢0 = m^n≢0 2 bits
mod : ℕ → ℕ
mod n = n % 2 ^ bits
My Top module looks like this:
{-# OPTIONS --verbose tc:100 #-}
module Top where
open import Sub1 3
It looks like typechecking the import of Sub1 from Top takes time that's exponential in the bits argument to Sub1. So, typechecking becomes prohibitively expensive for larger values of bits, say, 32.
When I get rid of the instance as a workaround as in the following module, Sub2, and then have Top import that modified module instead of Sub1, then I don't see this issue.
open import Data.Nat using (ℕ ; NonZero ; _^_ ; _%_)
open import Data.Nat.Properties using (m^n≢0)
module Sub2 (bits : ℕ) where
mod : ℕ → ℕ
mod n = _%_ 2 (2 ^ bits) ⦃ m^n≢0 2 bits ⦄
Here's what see in the debug output for bits = 3 when I use the original module, Sub1:
Considering Top._.2^bits≢0 for projection likeness
Checking for projection likeness
2^bits≢0 : Data.Nat.Base.NonZero (2 Data.Nat.Base.^ 3)
no candidates found
adding typed instance 2^bits≢0 with type
Data.Nat.Base.NonZero (2 Data.Nat.Base.^ 3)
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
{ workOnTypes
}
added value 2^bits≢0 to discrimination tree with case
case 0 of
Data.Nat.Base.NonZero¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.suc¹ → case 0 of
Agda.Builtin.Nat.Nat.zero⁰ → done {2^bits≢0}
its type:
Data.Nat.Base.NonZero (2 Data.Nat.Base.^ 3)
its path:
[Data.Nat.Base.NonZero¹, Agda.Builtin.Nat.Nat.suc¹,
Agda.Builtin.Nat.Nat.suc¹, Agda.Builtin.Nat.Nat.suc¹,
Agda.Builtin.Nat.Nat.suc¹, Agda.Builtin.Nat.Nat.suc¹,
Agda.Builtin.Nat.Nat.suc¹, Agda.Builtin.Nat.Nat.suc¹,
Agda.Builtin.Nat.Nat.suc¹, Agda.Builtin.Nat.Nat.zero⁰]
Computing display forms for Top._.2^bits≢0
appDefE' v = Top._.2^bits≢0
I tried other values of bits and it generally seems like I get 2 ^ bits + 2-many { workOnTypes } log entries and the same number of case 0 of ... log entries. So, something related to instances seems linear in 2 ^ bits, or exponential in bits.
It's not a big deal to me, given that there's a workaround. But maybe it's something to look into. I found it quite confusing at first.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4