You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This came up as part of a thing I'm currently working on. Due to Prelude.elem being implemented for all Foldables, it is significantly slower at compile-time compared to the "trivial" implementation by hand. The full call chain for Prelude.elem is:
elem = elemBy (==) = any = foldMap = __bind_foldMap
Which I understand is necessary because we are generalising over all Foldable instances, but it is a shame that it results in the worse performance detailed below.
module ListElem
import Data.So
import Data.List
%defaulttotalpublic export
elem':Eq a=> a ->List a ->Boolelem' _ [] =Falseelem' e (x :: xs) = (e == x) ||elem' e xs
public export
0Has42: So (elem' 42 [1..300])
Has42=Oh
With each module in its own file, measure the time it takes to type-check each file, for example via:
/usr/bin/time -- idris2 --check path/to/file.idr
Expected Behaviour
The two files should type-check in roughly the same time.
Observed Behaviour
The file using Prelude.elem type-checks in ~1.45 seconds, whereas the file using elem' type-checks in ~0.90 seconds. And this difference gets worse with more complex data types and longer lists (the above is a minimised example).
Thoughts
I don't know if there is much to be done about this, but I thought it was worth raising. Edwin mentioned something about __bind_foldMap being expanded or optimised at run-time, so maybe there is a similar hack we can employ at the type-level?
If nothing can be done, feel free to close this issue : )
The text was updated successfully, but these errors were encountered:
This came up as part of a thing I'm currently working on. Due to
Prelude.elem
being implemented for allFoldable
s, it is significantly slower at compile-time compared to the "trivial" implementation by hand. The full call chain forPrelude.elem
is:Which I understand is necessary because we are generalising over all
Foldable
instances, but it is a shame that it results in the worse performance detailed below.Steps to Reproduce
Consider the following two modules:
PreludeElem.idr
ListElem.idr
With each module in its own file, measure the time it takes to type-check each file, for example via:
Expected Behaviour
The two files should type-check in roughly the same time.
Observed Behaviour
The file using
Prelude.elem
type-checks in ~1.45 seconds, whereas the file usingelem'
type-checks in ~0.90 seconds. And this difference gets worse with more complex data types and longer lists (the above is a minimised example).Thoughts
I don't know if there is much to be done about this, but I thought it was worth raising. Edwin mentioned something about
__bind_foldMap
being expanded or optimised at run-time, so maybe there is a similar hack we can employ at the type-level?If nothing can be done, feel free to close this issue : )
The text was updated successfully, but these errors were encountered: