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

Last update: Jan 1, 2023

Related tags

Overview

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

Motivating example: security types
More complex example: session and list types
How does Tyrade work?
Next steps

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 <Sec > }

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.

= >::Output; fn sec_tests() { // example unit tests assert_type_eq:: >(); assert_type_eq:: >(); } ">
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<i32, Close>, Dual<Send<i32, Close>> >(); }

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 <(Env, S) >); impl Chan > { // label() pushes a type S onto the environment fn label( self) -> Chan , S> { Chan(PhantomData) } } impl 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 <Close, Nil >, Label <Goto <S <Z >>>> = Chan(PhantomData); // label() pushes Goto onto the Env list let c: Chan < Cons <Goto <S <Z >>, Cons <Close, Nil >>, Goto <S <Z >> > = c. label(); // goto(1) replaces the session type with the type at index 1 let _: Chan <Cons <Close, Nil >, 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) => 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:

The compiler sets up the necessary traits and type definitions (ComputeTAdd and TAdd).

While compiling the operators to types, all operations are added as where constraints. For example, TAdd(N3, S(N2)) creates the constraint N3: ComputeTAdd >.

~~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:

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.

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].

Comments

Multi-level matching

I'm working on type level list. The list can be represented by an enum-like type.

pub enum List {
    Nil,
    Cons(Type, List)
}

To obtain the last element of list, we recursively checks if the list has single element or more, and is assumed not to be empty. I tried two ways of writing.

The first is apparently invalid for now since tyrade cannot match on type.

pub fn Last(L: List) -> Type {
    match L {
        Cons(Head1 @ Type, Nil) => { // Nil is a type here
            Head1
        }
        Cons(Head1 @ Type, Cons(Head2 @ Type, Tail @ List) @ List) => {
            Last(Cons(Head2 @ Type, Tail @ List))
        }

    }
}

I tried two level matching. However, it complains about Invalid match on Tail1 error.

pub fn Last(L: List) -> Type {
    match L {
        Cons(Head1 @ Type, Tail1 @ List) => {
            match Tail1 {
                Nil => Head1,
                Cons(Head2 @ Type, Tail2 @ List) => Last(Cons(Head2, Tail2))
            }
        }
    }
}

opened by jerry73204 4

Type equality?
You mention in the README that you couldn't get type equality to work. I was curious to know what kind of things you've tried. Just in case you hadn't seen it, there's a trick described here that seems relevant:

trait Id { type X; } impl<T> Id for T { type X = T; }

Then you can use where T: Id<X=U> that functions like where T == U. Using this and specialization, I'm under the impression that you could implement if T == U in your language.
opened by Nadrieril 13
Is it possible to build something like "consensus type" based on tyrade?

We know consensus(pbft, raft, paxos etc) is a big topic for distributed systems, which are hard to verify.

There's some tools like tla or coq, which can help verify simple systems, but neither verifies rigorously, or are too complex to do it rigorously.

Can tyrade help in this case?

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.

This is also a reply to the question.

opened by zhiqiangxu 2

Alternative construct of type operating traits

I noticed tyrade treats the first argument specially when translating function arguments.

impl<...> ComputeIdent<Arg2, Arg3, ...> for Arg1 {
    type Output = ...;
}

The design does not distinguish functions and methods. For example, users would add L name prefixes on list operating traits for distinction. It results in C-style naming.

impl<L: List, V> LAppend<V> for L {...}
impl<L: List, V> LPrepend<V> for L {...}

I have an alternative approach that enables us to write methods in impl {} block. We can instead move the first argument to the generic list. The additional benefic is that we can define constant-valued functions.

impl<...> Function<Arg1, Arg2, ...> for () {
    type Ouput = ...;
}

impl ConstFn for () {
    type Output = U3; // from typenum
}

impl<...> Calling<Arg1, Arg2, ...> for ()
where
    (): Function<Arg1, ...> // trait bound
 {
    type Output = <() as Function<Arg1, ...>>::Output;
}

While for methods, the self is regarded as operands.

impl List {
    fn Append(self, V: Type) -> List {
    }
}

// translates to

impl<S: LIst, V> Append<V> for S
{
    type Output = ...;
}

We can make it further. The Compute* traits are generalized into maps like that is done in my type-freak (code). It enables the function passing arguments. For example, List::map.

pub trait Map<Inputs> {
    type Output;
}

// type operating trait from user
trait Compute<Arg1, ...> {}
impl Compute<Arg1, ...> for () { type Output = ...; }

// derived
struct ComputeMap;
impl<...> Map<(Arg1, ...)> for ComputeMap {
    type Output = <() as Compute<Arg1, ...>>::Output;
}

// now we have "callbacks"
trait Calling<T, F: Map> {}
impl<T, F: Map> Calling<T, F> for () {
    type Output = <F as Map<T1, T2, T3, ...>>::Output;  // T1, T2, T3 arguments are derived from T
}

opened by jerry73204 2

Use typenum for type-level integers

Currently this crate uses peano arithmetic, but this is too inefficient in many cases (especially as numbers grow in size). It would be better to use typenum which offers all arithmetic operations in O(log(n)) time as the default. (I think we still need to keep the peano arithmetic because there are cases where it is more efficient, for example when counting things).

https://github.com/paholg/typenum

opened by RustyYato 1