Need help with tyrade?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

willcrichton
161 Stars 7 Forks 24 Commits 4 Opened issues

Description

A pure functional language for type-level programming in Rust

Services available

!
?

Need anything else?

Contributors list

# 168,700
Rust
Shell
CSS
stanfor...
18 commits
# 10,924
python3
pandas
SQL
inspect...
1 commit
# 15,458
tutoria...
tutoria...
Rust
1 commit
# 231,754
testcon...
jupyter
repl
Visual ...
1 commit

Tyrade: a pure functional language for type-level programming in Rust

ci

Tyrade is a proof-of-concept language showing how Rust traits enable a general purpose type-level programming model. Its goal is to show that type-level programming is possible for useful tasks (not writing Turing machines), and programs can be written in a reasonable way. Here's what the language looks like:

tyrade! {
  enum TNum {
    Z,
    S(TNum)
  }

fn TAdd() { match N1 { Z => N2, S(N3) => TAdd(N3, S(N2)) } } }

fn num_tests() { // 1 + 1 == 2 assert_type_eq::>, TAdd, S>>(); }

At its core, Tyrade supports recursive enum types (kinds, technically) and pure recursive functions. For the main ideas behind Tyrade, continue below or consider reading my blog post on type-level programming.

Motivating example: security types

Others have shown that Rust traits are Turing-complete and can be used for e.g. Fizz-Buzz. However, the direct expression of type-level programming in traits is quite obtuse, i.e. the relationship between the conceptual program and the actual traits are obscured.

As a simple example, consider two types

HighSec
and
LowSec
representing the security of an item:
struct HighSec;
struct LowSec;

struct Item { t: T, _sec: PhantomData }

A simple type-level program is to compute the maximum of two security levels. That is, if

S1 = S2 = Low
, then return
Low
, else return
High
. To encode this program in Rust traits, we turn the
MaxLevel
function into a trait, with an
impl
for each condition.
trait ComputeMaxLevel {
  type Output;
}

// These impls define the core computation impl ComputeMaxLevel for LowSec { type Output = LowSec; } impl ComputeMaxLevel for LowSec { type Output = HighSec; } impl ComputeMaxLevel for HighSec { type Output = HighSec; } impl ComputeMaxLevel for HighSec { type Output = HighSec; }

// The type alias gives us a more convenient way to "call" the type operator type MaxLevel = >::Output;

fn sec_tests() { // example unit tests assert_type_eq::>(); assert_type_eq::>(); }

The goal of Tyrade is to perform this translation automatically from a functional programming model. Using Tyrade, this program is written as:

tyrade!{
  enum Security {
    Low,
    High
  }

fn MaxLevel() { match S1 { Low => match S2 { Low => Low, High => High } High => High } }

// In the high-level language, we can more easily see a chance for simplification. fn MaxLevel2() { match S1 { Low => S2, High => High } }

}

This way, both the data-type definition and the type-level program are expressed using familiar constructs like

enum
and
match
.

More complex example: session and list types

Tyrade can be used to define a framework for communication protocols, e.g. session types. For example, the session types and their duals can be defined as follows:

tyrade! {
  enum SessionType {
    Close,
    Recv(Type, SessionType),
    Send(Type, SessionType),
    Choose(SessionType, SessionType),
    Offer(SessionType, SessionType),
    Label(SessionType),
    Goto(TNum)
  }

fn Dual() { match S { Close => S, Recv(T, S2) => Send(T, Dual(S2)), Send(T, S2) => Recv(T, Dual(S2)), Choose(S2, S3) => Offer(Dual(S2), Dual(S3)), Offer(S2, S3) => Choose(Dual(S2), Dual(S3)), Label(S2) => Label(Dual(S2)), Goto(N) => S } } }

fn session_type_test() { assert_type_eq::< Recv, Dual> >(); }

Tyrade provides a standard library of type-level building blocks like booleans, numbers, and lists. For example, we can use lists to implement the compile-time saving and indexing of jump points in session types.

struct Chan(PhantomData);

impl<env: tlist s: sessiontype> Chan> { // label() pushes a type S onto the environment fn label(self) -> Chan, S> { Chan(PhantomData) } }

impl<env: tlist n: tnum> Chan> where Env: ComputeTListNth + ComputeTListSkip { // goto gets the Nth type from the environment, removing every type // before then fn goto(self) -> Chan, TListNth> { Chan(PhantomData) } }

fn session_type_test() { let c: Chan< Cons, Label>>> = Chan(PhantomData);

// label() pushes Goto onto the Env list let c: Chan< Cons>, Cons>, Goto>> = c.label();

// goto(1) replaces the session type with the type at index 1 let _: Chan, Close> = c.goto(); }

How does Tyrade work?

Consider the translation of

TAdd
. Here's the Tyrade definition:
fn TAdd() {
  match N1 {
    Z => N2,
    S(N3 @ TNum) => TAdd(N3, S(N2))
  }
}

And here's the generated Rust code:

pub trait ComputeTAdd {
    type Output;
}

pub type TAdd = >::Output;

impl ComputeTAdd for Z { type Output = N2; }

impl ComputeTAdd for S where N3: ComputeTAdd> { type Output = TAdd>; }

At a high level, Tyrade does the following for you: 1. The compiler sets up the necessary traits and type definitions (

ComputeTAdd
and
TAdd
). 2. While compiling the operators to types, all operations are added as
where
constraints. For example,
TAdd(N3, S(N2))
creates the constraint
N3: ComputeTAdd>
. 3. The compiler generates a different
impl
for each match branch. In the case of multiple matches, e.g. as in
MaxLevel
, the compiler generates an impl for the cartesian product of all match branches.

See trans.rs for the details.

Next steps

Tyrade is experimental, meaning I'm still discovering the boundaries of what's possible. There are two main areas of inquiry:

  1. What type-language mechanisms does Rust's trait system permit? For example, I was not able to implement

    ==
    since type equality in Rust doesn't quite work as we need it. Higher-kinded types would be useful as well to enable proper polymorphic type functions.
  2. What application areas can benefit from a type-level programming language? Session types are the most complex example I've seen so far, but I'd be really interested to find other use cases for Tyrade.

Please let me know if you'd be interested in using or contributing to Tyrade! Email me at [email protected]

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.