Software Geek

March 24, 2008

Uniqueness Typing Simplified

Filed under: Software

Also see: A VS.NET Macro to Generate Machine Keys.

Uniqueness Typing Simplified , by Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson.

We present a uniqueness type system that is simpler than both Clean’s uniqueness system and a system we proposed previously. The new type system is straightforward to implement and add to existing compilers, and can easily be extended with advanced features such as higher rank types and impredicativity. We describe our implementation in Morrow, an experimental functional language with both these features. Finally, we prove soundness of the core type system with respect to the call-by-need lambda calculus.

Uniqueness typing is related to linear typing, and their differences have been discussed here before. Linear types have many applications. This paper describes the difference between linear and unique types:

In linear logic, variables of a non-linear type can be coerced to a linear type (dereliction). Harrington phrases it well: in linear logic, “linear” means “will not be duplicated” whereas in uniqueness typing, “unique” means “has not been duplicated”.

In contrast to other papers on substructural typing, such as Fluet’s thesis Monadic and Substructural Type Systems for Region-Based Memory Management , this paper classifies uniqueness attributes by a kind system. This possibility was mentioned in Fluet’s thesis as well, Section 4.2, footnote 8, though the technique used here seems somewhat different.

Uniqueness typing is generally used to tame side-effects in purely functional languag

Also see: Programmers At Work

Also see: Blogging and Newspapers, a Lesson in How Not to Brand and Market

Also see: TransparentProxy

Also see: YouTube Tries to Get Legal

Also see: CERT C Secure Coding Standard

Also see: DevWeek 2008 Cross Platform Silverlight Demos

es. Uniqueness types have also been contrasted with monads on LTU , which are also used to tame effects, among other things. One point not discussed in that thread, is how straightforward it is to compile each approach into efficient code. It seems clear that uniqueness types have a straightforward, efficient compilation, but it’s not clear to me how efficient monads can be, and how much work is required to make them efficient. This may make uniqueness or substructural types more suitable for just-in-time compilers than monads.
http://lambda-the-ultimate.org/node/2708

Comments »

The URI to TrackBack this entry is: http://annil12.blogsome.com/2008/03/24/uniqueness-typing-simplified-2/trackback/

No comments yet.

RSS feed for comments on this post.

Leave a comment

Line and paragraph breaks automatic, e-mail address never displayed, HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>



Anti-spam measure: please retype the above text into the box provided.

Get free blog up and running in minutes with Blogsome
Theme designed by Jay of onefinejay.com