Skip to main content

​
Linear Types

Dryft uses a linear type system to achieve memory safety without garbage collection. Every value must be used exactly once, eliminating memory leaks and use-after-free errors.

​
Why Linear Types?

Linear types enable:
  • Memory safety without garbage collection
  • Lightweight runtime suitable for embedded systems and performance-critical applications
  • Explicit resource management where resource lifecycles are visible in code
  • No use-after-free bugs - the compiler prevents them
  • No memory leaks - resources must be explicitly consumed or freed

​
The Linear Type Philosophy

While linear types can seem restrictive in traditional languages, they work naturally with stack-based languages. In Dryft:
  • Working data lives on the shared stack
  • The difference between consuming and non-consuming operations is pronounced
  • It’s harder to “forget” to free a resource
  • Not using a value automatically returns it in a way

​
Value Consumption

In Dryft, most operations consume their inputs from the stack: 
5 3 +  # Both 5 and 3 are consumed by +
Once consumed, a value cannot be used again: 
# ERROR: Can't use same value twice
5 var: x
$x $x +  # Second $x is invalid - x already consumed!

​
Non-Consuming Operations

Some operations don’t consume values - they copy them:

​
The copy Operation

Use copy (or ^) to duplicate a value: 
5 copy  # Stack: [5, 5]
Now you can use the value twice: 
5 copy + # Duplicates 5, then adds: 5 + 5 = 10

​
Practical Example

fun: double
    copy + ;  # Duplicate the value, then add it to itself

fun: square
    copy * ;  # Duplicate the value, then multiply by itself

​
Variables and Linear Types

Variables in Dryft interact with the linear type system:

​
Reading Variables

Reading a variable with $ moves the value from the variable: 
10 var: x
$x printi  # x is consumed, cannot be read again
# $x printi  # ERROR: x already consumed

​
Using Variables Multiple Times

To use a variable multiple times, reassign it: 
10 var: x
$x copy x!  # Read x, copy it, write one copy back
$x printi   # Now we can read x again
Or use the value and write a new one: 
10 var: x
cycle: $x 0 =? then: break ;
    $x printi
    $x 1 - x!  # Use old x, compute new value, store it
:cycle

​
Linear Types in Practice

​
Factorial Example

fun: factorial var: n
    1 var: result
    cycle: $n 0 =? then: break ;
        $result $n * result!  # Consume result and n
        $n 1 - n!             # Consume n, compute n-1, store back
    :cycle
    $result  # Return final result (consuming it)
:fun
Notice how:
  • Each read of $n consumes it
  • We immediately write a new value back with n!
  • Variables maintain the linear invariant

​
Swap Operation

# swap doesn't consume - it rearranges
1 0 swap  # Stack: [0, 1]
printi space printi  # Prints "1 0"

​
Drop Operation

Explicitly discard a value with drop (or v): 
42 drop  # Value consumed without being used
This is important for linear types - you must explicitly state when you’re done with a value.

​
Resource Management

Linear types shine in resource management: 
# Future file handling example
file_open var: handle
$handle file_read var: data
$handle file_close  # Must close - handle must be consumed
$data process
The compiler ensures:
  • handle is not used after being closed
  • handle cannot be forgotten - it must be consumed (closed)
  • data is used exactly once

​
Copy vs Move Semantics

Move (Default)

Most operations move/consume values
  • +, -, *, /, mod
  • Comparisons: =?, >?, <?
  • Logical ops: both?, either?
  • Variable write: x!

Copy (Explicit)

Use copy to duplicate
  • copy or ^
  • Variable read with copy: $x copy
  • Non-consuming pattern

​
Benefits of Linear Types in Stack Languages

​
Explicit Data Flow

The stack makes value lifetimes visible: 
5          # [5] - value created
copy       # [5, 5] - value copied
3          # [5, 5, 3] - new value
+          # [5, 8] - top two consumed
swap       # [8, 5] - rearranged
+          # [13] - consumed

​
Natural Resource Handling

In concatenative style, resources flow through transformations: 
data clean validate transform store
Each step consumes the resource and produces a new state.

​
Prevention of Common Errors

# PREVENTED: Use after free
resource free resource use  # ERROR: resource consumed by free

# PREVENTED: Memory leak  
resource # ERROR: resource not consumed before end of scope

# PREVENTED: Double free
resource free free  # ERROR: resource already consumed

​
Comparison with Other Languages

​
Rust

Rust uses affine types (at most once) with borrowing. Dryft uses linear types (exactly once) without borrowing, which is simpler but requires explicit copying.

​
Austral

Dryft was inspired by Austral’s linear types. The stack-based nature makes linear types feel more natural than in traditional languages.

​
Working with Linear Types

​
Common Patterns

Using a value multiple times: 
5 copy copy  # [5, 5, 5] - three copies
* +          # 5*5 + 5 = 30
Temporary variables: 
10 var: temp  # Store temporarily
# ... do other work ...
$temp use     # Retrieve and use
Conditional consumption: 
value var: v
when: condition then:
    $v use_one_way ;
    $v use_other_way ;
Each branch must consume v exactly once.

​
Type System Integration

Linear types work with Dryft’s static type system: 
(Int -> Int Int)
fun: duplicate
    copy ;  # Takes one Int, returns two
The type system tracks:
  • What types are on the stack
  • How many times each value is used (linear property)

​
Limitations and Trade-offs

Linear types require more explicit code:
  • Must explicitly copy for multiple uses
  • Must explicitly drop unused values
  • Can feel restrictive initially
However, this explicitness provides:
  • Complete control over resources
  • Guaranteed memory safety
  • Zero-cost abstractions
  • No runtime overhead

​
Summary

  • Every value must be used exactly once
  • Operations consume their inputs by default
  • Use copy to duplicate values for multiple uses
  • Use drop to explicitly discard values
  • Variables follow linear rules: reads consume, writes replace
  • Linear types prevent leaks and use-after-free
  • Stack-based languages make linear types natural and intuitive
Linear types in Dryft achieve memory safety without garbage collection, making the language suitable for systems programming, embedded development, and performance-critical applications.

Build docs developers (and LLMs) love

Get started for freeTalk to us