Our great sponsors
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
One catchy feature in the changelog is the "scheme-based evaluator", but oh dear the explanations are really not very clear. Eventually I found the relevant PR which is a bit clearer. My understanding is that this evaluator works by compiling the Idris terms into a Scheme value, then letting the Scheme backend eval this, and translating the normal form back into Idris, the reasoning being that Scheme's eval is probably faster than whatever Idris already has written by hand (it probably performs a form of just-in-time compilation to a more compiled representation).