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.
-
- my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine
I'm curious if you have any insight into what a realistic lower limit to Idris compile time speed looks like. Right now even moderately sized Idris programs can be quite slow to compile, slower than even other dependently-typed languages (see e.g. https://github.com/AndrasKovacs/smalltt). How much of this is intrinsic to Idris' language design and how much of it is due to lack of optimization in the implementation?
I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array.
The example given in the paper is a LinArray (https://github.com/idris-lang/Idris2/blob/main/libs/contrib/...). Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613)
The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type.
On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions.
ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).
Here is an example of a tiny toy compiler proven correct in Idris. It is a small example of the kind of cool things you can do in Dependently Typed languages: https://github.com/mbrodersen/idris-sandbox/blob/master/comp...