Thread View: comp.lang.functional
6 messages
6 total messages
Started by Leon Pillich
Thu, 01 Oct 1992 13:44
Unique types etc.
Author: Leon Pillich
Date: Thu, 01 Oct 1992 13:44
Date: Thu, 01 Oct 1992 13:44
102 lines
4013 bytes
4013 bytes
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
Re: Unique types etc.
Author: Karl-Filip Faxen
Date: Fri, 02 Oct 1992 08:33
Date: Fri, 02 Oct 1992 08:33
19 lines
1271 bytes
1271 bytes
Hello!
Unique types seem related, if not identical, to what Phil Wadler
calls "linear types". His (and others) work is (as far as I know)
based on Girard's linear logic, in which assumptions must be used
exactly once. Thus the type checker guarantees that variables with
linear types are used exactly once. The major application so far
seems to have been the array update problem (guaranteeing that
arrays are used in such a way that array update can safely be
implemented without copying).
So, are unique types the same as linear types?
Curious cheers,
Karl-Filip
------------------------------------------------------------
Make the frequent case fast, and the fast case frequent!
Re: Unique types etc.
Author: Fergus James HENDERSON
Date: Fri, 02 Oct 1992 18:41
Date: Fri, 02 Oct 1992 18:41
36 lines
2225 bytes
2225 bytes
kff@dentex.tds.kth.se (Karl-Filip Faxen) writes: >Hello! > >Unique types seem related, if not identical, to what Phil Wadler >calls "linear types". His (and others) work is (as far as I know) >based on Girard's linear logic, in which assumptions must be used >exactly once. Thus the type checker guarantees that variables with >linear types are used exactly once. The major application so far >seems to have been the array update problem (guaranteeing that >arrays are used in such a way that array update can safely be >implemented without copying). > >So, are unique types the same as linear types? Yes, I believe so. (Who am I to answer this question? I had never heard of either of them until they came up here! But from my limited understanding, yes :-) On the other hand if I were implementing arrays with destructive update, I would not use exactly what has described as linear types or unique types. When we are talking about I/O states, it is not possible to refer to the same state more than once - once you have invoked some I/O operation, the state has changed and it may be physically impossible to return to the old state. Thus you must issue an error message if a program tries to use the same I/O state twice. However with arrays, you *can* refer to them twice - it's just not as efficient that way. Instead of issuing an error message when an array is used twice, you should automatically copy the array, perhaps issuing a warning at most. -- Fergus Henderson fjh@munta.cs.mu.OZ.AU This .signature virus is a self-referential statement that is true - but you will only be able to consistently believe it if you copy it to your own .signature file!
Re: Unique types etc.
Author: Leon Pillich
Date: Sat, 03 Oct 1992 17:24
Date: Sat, 03 Oct 1992 17:24
32 lines
1785 bytes
1785 bytes
In <1992Oct2.170149.24827@plex-1.ann-arbor.mi.us> dhw@plex-1.ann-arbor.mi.us (David West) writes:
>In article <BvG3I3.B2M@sci.kun.nl> leonp@cs.kun.nl (Leon Pillich) writes:
>>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.
>Don't you need to somehow make clock'' available for the next invocation
>of GetTime anywhere, even within G? Or have I misunderstood how this is
>supposed to work?
Sure, but only whenever you will need it again.
But indeed normally you would write such programs like
- first initialize a unq type i.e. Open a UNQ file, clock etc
- a cascade of functions each having the unq type as input
and the again as output
- when thers no need anymore of the type just discard it
Thats all to it....
Leon Pillich
University of Nijmegen, Holland
email: leonp@cs.kun.nl
-------------------------------------------------------------
Life is what's happening when you're making other plans ...
John Lennon
Linear types (was Re: Unique types etc.)
Author: Jeremy Gibbons
Date: Mon, 05 Oct 1992 01:10
Date: Mon, 05 Oct 1992 01:10
15 lines
1309 bytes
1309 bytes
In <1992Oct2.083300.20958@kth.se> kff@dentex.tds.kth.se (Karl-Filip Faxen) writes: >Unique types seem related, if not identical, to what Phil Wadler >calls "linear types". His (and others) work is (as far as I know) >based on Girard's linear logic, in which assumptions must be used >exactly once. Thus the type checker guarantees that variables with >linear types are used exactly once. Which brings up the question... if linear logic insists that assumptions be used exactly once, does a language with linear types insist that linear variables be used exactly, as opposed to at most, once? What breaks if you just insist that variables with "linear" types be used at most once---"single threading"? (Is it some sort of strictness that breaks?) Jeremy (a linear novice)
Re: Unique types etc.
Author: "D. Hugh Redelmeier"
Date: Tue, 06 Oct 1992 04:57
Date: Tue, 06 Oct 1992 04:57
17 lines
1151 bytes
1151 bytes
leonp@cs.kun.nl (Leon Pillich) writes:
| 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.
Interesting. These seem to be related to "dialogues" which I
discussed in a chapter of my PhD Dissertation:
D. Hugh Redelmeier, "Towards Practical Functional Programming",
Department of Computer Science, University of Toronto, 1984.
Hugh Redelmeier
hugh@mimosa.com or {utcsri, yunexus, utzoo, scocan}!redvax!hugh
When all else fails: hugh@csri.toronto.edu
+1 416 482-8253
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads