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
>>Uniqueness types[1], which are inspired by ownership types and borrowed pointers in the Rust language<<
"They are inspired by linear types, Uniqueness Types in the Clean programming language, and ownership types and borrowed pointers in the Rust programming language."
If I understand correctly Uniqueness Types cannot be used in place of regular Types? That is, if one function takes regular Types you can't have it work on an Uniqueness Type?
If so, doesn't that make Uniqueness Types very awkward to use?
It's hard to write something that's generic over a uniqueness type and a normal type, which is indeed a bit of a pain. It's not completely impossible: we have a kind 'Type*' which covers both unique and normal types, which can be used to make some polymorphic functions which preserve uniqueness, but that's all at the minute.
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.
That's correct. You can however have a function take a Type\star, meaning it accepts both Types and UniqueTypes. If such a function is passed a Type, that Type can only be used in the ways that UniqueTypes can be used ("any value of type Type* must also satisfy the requirement that it appears at most once on the right hand side"). The linked page provides an example of function composition defined using Type*:
(.) : {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.
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.
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
1. https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type...2. https://github.com/idris-lang/Idris-dev/wiki/Static-Argument...
3. http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf