Idris 0.9.15 released – partial evaluation and uniqueness types
idris-lang.org
idris-lang.org
Uniqueness types[1], which are inspired by ownership types and borrowed pointers in the Rust language, and should eventually be able to provide compile-time guarantees that critical program fragments will never allocate. If this was achieved, Idris would potentially be usable for tasks that previously necessitated using either C, C++ or Rust.
Partial evaluation[2], which can also be used to improve performance by specialising type classes and higher order functions. Another use is creating speedy interpreters/EDSLs, with the one in [3] being competitive in speed with Java in spite of only being an interpreter.
Uniqueness types can also be used for safe in-place updates of a datastructure. The following map function, for instance, where UList is a UniqueType, will be compiled to code that updates the list in-place, avoiding allocating a new list:
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
2. https://github.com/idris-lang/Idris-dev/wiki/Static-Argument...
If so, doesn't that make Uniqueness Types very awkward to use?
(.) : {a, b, c : Type\star} -> (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)
Not being able to use UniqueTypes in place of regular Types could indeed cause some inconvenience, however I think to some degree it's unavoidable. Rust for instance doesn't let you pass a reference-counted or garbage-collected pointer to a function expecting a unique/borrowed pointer.
Note that \star should be an asterix character, but I'm not sure how to escape it properly here.
On the other hand, I see them as something you use when you want more precise control over memory management, control of in-place update and so on.
As ever, there's a trade off between efficiency and abstraction, which is where the partial evaluator comes in. This is still experimental and we're working on it, but I'm wondering if we can use partial evaluation to turn nicely abstract high level code into something efficient based on uniqueness types at run time.
I guess my main worry with this scheme would be fragmentation, having 3rd party libraries not bothering using Type* where it makes sense and making it very difficult to write code using uniqueness types. I guess I'll have to learn me some Idris and see for myself, the language looks very interesting.
"They are inspired by linear types, Uniqueness Types in the Clean programming language, and ownership types and borrowed pointers in the Rust programming language."
See http://clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.h...
ATS combines ML-style types, linear types, dependent types and theorem-proving. Plus it compiles down to C, has pointers including (safe!) pointer arithmetic, has trivial C interop, and doesn't have GC (alloc/free safety is provided by the linear types, like with Rust lifetimes). It's a really interesting beast and I hope I have more time in the future to dive into it. Idris wins in the syntax department tho.
Rust's move/ownership semantics are based on linear types, where as its lifetimes are based on regions. ATS has linear types, but not regions.