Idris 0.9.15 released – partial evaluation and uniqueness types

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by logicchains on Monday October 27, 2014 @01:58AM (#8514097)

Some highlights:

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

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

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by igouy on Monday October 27, 2014 @02:21PM (#8517169)

>>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."

See http://clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.h...

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by simias on Monday October 27, 2014 @06:30AM (#8514709)

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?

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by edwinb on Monday October 27, 2014 @06:51AM (#8514760)

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.

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by simias on Monday October 27, 2014 @09:11AM (#8515222)

Thank you for both your answers.

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.

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by logicchains on Monday October 27, 2014 @06:51AM (#8514757)

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.

[ Parent | on HN ]