Skip to content
CinchTHE CINCH
PROGRAMMING LANGUAGE
LANGUAGE DESIGN / IN DEVELOPMENTTYPES · EFFECTS · OWNERSHIP

Power,
with proof.

Dependent types.
Explicit effects. Resource control.

Cinch is a strict functional language for programs with contracts about their data, resources, and runtime behavior.

Get Cinch ↗Start the tutorial →
01 / DEPENDENT TYPES
first.cinchTYPE ILLUSTRATION
first :: forall a n region.
Ref region (Vec (n + 1) a)
→ Ref region a
Nonempty input3 = 2 + 1

The length fits n + 1. The first element can be borrowed.

INPUT: LENGTH-INDEXEDRESULT: BORROWED
03
TUTORIAL 01Read the example
Change the input. Inspect the contract.
STRICT FUNCTIONAL LANGUAGEINSIDE THE LANGUAGE ↓
01 / LANGUAGE DESIGNCINCH / DESIGN NOTES

Functional code.
Explicit contracts.

A function’s type can describe the length of its result, the effects it performs, and the resources it borrows.

Cinch uses algebraic data types, pattern matching, and higher-order functions. Dependent types and ownership extend that foundation so you can specify properties of your code and check the evidence for them.

Core language specification ↗
STRICT EVALUATIONDEPENDENT TYPESEXPLICIT EFFECTSRESOURCE CONTROL
02 / DEPENDENT TYPES IN USETHE CONTRACT IN CODE

A first element
requires
a nonempty vector.

The input has length n + 1. An empty vector has length 0, so it cannot be passed to this function.

Pattern matching leaves one constructor to handle. The returned reference borrows from the input and cannot outlive it.

Read the example in context ↗
first.cinchDESIGN EXAMPLE
-- Borrow the first element of a nonempty vector.
first :: forall a n region.
  Ref region (Vec (n + 1) a)
  -> Ref region a

first xs = case xs of
  Cons x rest -> x
↳

Why there is no Nil branch
Nil has length 0. This input requires n + 1.

TUTORIAL 01 / VALUES AND DEPENDENT TYPES
FIG. 01 / DEPENDENT TYPESINPUT → BORROWED RESULT
A three-element vector and a reference to its first elementThree cells form one vector. The first cell is highlighted. The remaining two cells form the tail. A result reference points back to the first cell, borrowing its value rather than copying it.n + 1 = 3xyz123n = 2
  1. InputRef region
    (Vec (n + 1) a)
  2. Remaining tail

    n elements

  3. Borrowed resultRef region a
Figure 01. A nonempty vector. The illustrated input has length 3, so n = 2. The result refers to the first element and cannot outlive the input.
03 / LANGUAGE FEATURESTYPES / RESOURCES / EVOLUTION

What the language
keeps track of.

Dependent types

A vector carries its length in its type. A connection carries its schema. Functions can require evidence about the values they accept and preserve those relationships in their results.

Values and dependent types↗

Ownership and effects

Resource ownership determines who can use a value and when it must be released. Effect signatures describe what a computation can do, including I/O, suspension, and divergence.

Ownership and effects tutorial↗

Checked hot upgrades

Replacing a running module requires a compatibility check and a plan for its state. An upgrade package describes the migration, ownership transfer, and obligations to existing clients.

Compatible hot upgrades tutorial↗
04 / DOCUMENTATIONCONTENTS

Read the
language design.

The tutorials introduce the notation.
The specifications define the contracts.

Tutorials

14 chapters, from values and types to concurrency and compatible upgrades.

Specifications

The semantics, contracts, and rules that make up the language.

Design notes

Open questions, implementation plans, and the reasoning behind the design.

05 / TOOLS AND LIBRARIESDEVELOPER RESOURCES

Downloads
and packages.

TOOLCHAIN

Get Cinch

Choose a platform, inspect release information, or get the source.

LIBRARY INDEX / PREVIEW

Browse packages

Explore libraries, read module references, and follow linked types into the API.

TUTORIAL 01 / VALUES AND DEPENDENT TYPES

Read the
first tutorial.

STRICT FUNCTIONS → VALUES IN TYPES → RUNTIME WITNESSES