News for hackers. Stuff that matters.
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.

There are no comments on this comment yet.