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

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.

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.

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
} 

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