Linear types (was Re: Unique types etc.)

Article View: comp.lang.functional

Article #646

Back to comp.lang.functional Previous Next

#646

From: Jeremy Gibbons
Date: Mon, 05 Oct 1992 01:10

15 lines
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)

Technical Details

Message-ID: <1992Oct5.011020.23442@cs.aukuni.ac.nz>

Path: arc1-ca.pugleaf.net!sparky!uunet!munnari.oz.au!comp.vuw.ac.nz!waikato.ac.nz!aukuni.ac.nz!cs18.cs.aukuni.ac.nz!jeremy

References: <BvG3I3.B2M@sci.kun.nl> <1992Oct2.083300.20958@kth.se>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!munnari.oz.au!comp.vuw.ac.nz!waikato.ac.nz!aukuni.ac.nz!cs18.cs.aukuni.ac.nz!jeremy
Newsgroups: comp.lang.functional
Subject: Linear types (was Re: Unique types etc.)
Message-ID: <1992Oct5.011020.23442@cs.aukuni.ac.nz>
From: jeremy@cs.aukuni.ac.nz (Jeremy Gibbons)
Date: Mon, 5 Oct 1992 01:10:20 GMT
References: <BvG3I3.B2M@sci.kun.nl> <1992Oct2.083300.20958@kth.se>
Organization: Computer Science Dept. University of Auckland
Keywords: Unique types, linear types, linear logic
Lines: 16

Reply to Parent Message