🚀 go-pugleaf

A while ago I posted a reaction on a discussion about
things that are difficult to do with functional programming
languages. I briefly mentioned Unique types.
I got some reactions on my post so I decided to write
a short follow up, to tell something about unique types
and to give some references where one can find more information.
I'll use Concurrent Clean syntax here, though it wil
be easy readible for anybody with no experience in Clean.
I use Clean because UNQ types are implemented in Clean
and because I'm working on an implementation of a portable IO system
using Concurrent Clean and UNQ types.

Consider the following very simple example:
We have an abstract type Clock that represents the system clock.
This abstract type can be used together with a function GetTime that
delivers the time of day:

ABSTYPE
:: Clock;

RULE == function 
:: GetTime Clock -> Time;

We can now write programs that access the system clock:
:: F Clock -> BOOL;
   F clock
   -> TRUE, IF Ontime clock; == ontime is some alarm function etc.
   -> FALSE

Now consider the function G:
:: G Clock -> ...;
   G clock -> .....GetTime clock ...... GetTime clock;

Somehere in its body G calls GetTime twice with the clock argument.
But since Clock represents the system timer and both the 'GetTime clock'
applications will not be executed at the same time they will not
deliver the same time. And therefore GetTime is not referentially transparent
i.e. not functional.
That's why we introduce a UNQ type predicate in our language that
enforces that the reference count of clock can be at most one.

ABSTYPE
:: UNQ Clock

RULE
:: GetTime Clock -> (Clock, Time);  

The next function will now be wrong:
:: G Clock -> ....
   G clock -> .... GetTime clock .... GetTime clock;

because the reference count of clock can be only one.
We should rewrite G as:
:: G Clock -> ....
   G clock -> ..... time1 ..... time2,
              (clock', time1): GetTime clock,
              (clock'', time2): GetTime clock';

We now have time1 and time2 with the correct values, yet it remains
referentially transparent and therefore functional.

The UNQ predicate is an extension of the type checker in Clean
and whenever a reference count of an object is >1 than
a compile time error is generated!

UNQ types van be usefull in many cased:
- doing unique file io
- other kinds of io
- in situ updating of lists or arrays
etc.

In the Concurrent Clean systems UNQ types are used at the moment
for files and IOStates, the latter is used for programming complex
windowing systems in functional languages.

More information about unique types can be found in:
* Concurrent Clean Language Manual - version 0.8.
  technical report no. 92-18 august 1992,
  Department of Informatics,
  Faculty of Mathematics and Informatica,
  University of Nijmegen, The Netherlands
  (available for anonymous ftp together with the concurrent clean package)

This manual also contains literature references.

The Concurrent Clean system is available for anonymous ftp
ftp to ftp.cs.kun.nl
in directory pub/Clean 

There are version of Clean 0.8 for Mac, Sun3 and Sun4
for the Mac version there is also a nice IO library
(which is described in the manual) that allows advanced gui
programming. This same library is currently being worked on
for Sun4/XWindows/OpenLook systems.


Leon Pillich
University of Nijmegen, Holland
email: leonp@cs.kun.nl
-------------------------------------------------------------
 Life is what's happening when you're making other plans ...
                                      John Lennon