12
$\begingroup$

Linear types are quite a powerful feature of type systems that ensure that "linear values" are used exactly once.

For example,

fn foo(): let handle = acquire_linear_value() // ... close(handle)

The compiler would force passing handle to some function like close before the function ends; otherwise, handle would not have been used!

This seems fine until other features, which may non-deterministically alter the usual control flow, are introduced in the language. An example of such a feature would be exceptions. E.g.,

fn foo(): let handle = acquire_linear_value() // ... bar() // may throw // ... close(handle)

Assuming that bar is a function that may diverge the usual control flow, handle would no longer be guaranteed to be used exactly once.

Can both features coexist in the same language? If so, how?

$\endgroup$
1

2 Answers 2

Reset to default
6
$\begingroup$

defer blocks

Swift has a defer keyword that guarantees a block to run when the scope exits — whether that’s via return, an error, or just reaching the closing brace:

func useFile() throws { let handle = open() defer { close(handle) } try bar() // If bar throws, Swift will catch the error, run the defer block, and then rethrow. if checkCondition() { return // early exit also triggers defer } baz() // reached end of scope normally, defer runs here }

If there are multiple defer blocks in the same scope, they run in reverse order of declaration.

In the same vein, languages like C# and JavaScript have try/finally:

var handle = open(); try { bar(); } finally { close(handle); }
$\endgroup$
3
$\begingroup$

A partial solution

A language like Rust would be able to partially accomplis this. Rust does not have exceptions, which are the primary way that the control flow would be diverted; instead, it has Result-returning functions, which the typechecker can easily see might lead to the linear type never being used. Rust does, however, have panics; in that case we will just have to assume that whatever the linear type represents will be taken care of by the OS (like if it's a file handle the OS will close it). This is not a perfect solution, however.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.