Crate typed_sf

Source
Expand description

Type-level implementation of SF. Proving that type-system turing-complete. Highly inspired by this article.

§Features

typed-sf supports “no_std” feature with limitations. Runtime representation of List’s and State’s unavailable (they are using Vec to represent themselves).

Full list of unsupported features:

Also where is “require_docs” feature which forbids undocumented pub items. If You want to contrubute, feel free to turn off this default feature.

§How it works

First, there’s some traits that i’m calling type-level enums (Bit, List). Have a look at it:

enum Bit {
    True,
    False
}

impl Bit {
    fn neg(self) -> Bit {
        match self {
            Bit::True => Bit::False,
            Bit::False => Bit::True
        }
    }
}

assert_eq!(Bit::True, Bit::False.neg());
assert_eq!(Bit::False, Bit::True.neg());
trait Bit {
    type Neg: Bit;
    fn real() -> bool;
}
struct True;
struct False;

impl Bit for True {
    type Neg = False;
    fn real() -> bool { true }
}

impl Bit for False {
    type Neg = True;
    fn real() -> bool { false }
}

assert_eq!(True::real(), <False as Bit>::Neg::real());
assert_eq!(False::real(), <True as Bit>::Neg::real());

Of course, what’s more bolierplate, but also instead of matching in runtime, compiler solves type-equasions in compile-time for us.

To type-encode functions i’m using something like this:

// A and B are arguments to 'function'.
trait Call<A, B> { type Return; }

struct Sum;
struct Diff;

impl<A, B> Call<A, B> for Sum
where
    A: Add<B>
{
    type Return = <A as Add<B>>::Output;
}

impl<A, B> Call<A, B> for Diff
where
    A: Sub<B>
{
    type Return = <A as Sub<B>>::Output;
}

type Apply<A, Fn, B> = <Fn as Call<A, B>>::Return;

What we can use later as:

struct X;
struct Y;
struct XaddY;
struct XsubY;

impl Add<Y> for X {
    type Output = XaddY;
}
impl Sub<Y> for X {
    type Output = XsubY;
}

/* Add `::val() -> Self` function to all types... */

assert_eq!(
    <Apply<X, Sum, Y>>::val(),
    XaddY::val()
);

assert_eq!(
    <Apply<X, Diff, Y>>::val(),
    XsubY::val()
);

That’s basically how Runner<Left, Value, Right> works. But commands such as Left take a generic argument, so it runs next command on modified state which does the same and so on…

§Examples

Basic usage

type SetTrue<Next = EOF> = Cycle<Flip, Flip<Next>>;
// [*<<[*]*>>>] // Move any-sized chunk of True's 2 cells left
type prog = Cycle<Flip<Left<Left<SetTrue<Right<Right<Right>>>>>>>;
type result = Run<
    prog,
    State<Nil, True, Cons<True, Nil>, False>
>;

assert_eq!(
    <result as StateTrait>::val(),
    (vec![true, true, false, false], false, Vec::new())
); //                 ^^^^^^^^^^^^
   // Some waste, honestly don't why it is here...

Structs§

Cons
Node of list, consists of value (Bit) and tail – List.
Cycle
Cycling ([ <Body> ] <Next> in SF) command. If current Bit is False – executes Next Command, otherwise – executes Body and itself again.
EOF
End-of-file command. Returns current state.
False
Type-level False value, Bit.
Flip
Flip current Bit (* <Next> in SF) command. Actually, just uses Bit::Neg type.
Left
Go left (< <Next> in SF) command. If left List is Nil, current bit will be from Default attribute from state.
Nil
End of List.
Right
Go right (> <Next> in SF) command. If right List is Nil, current bit will be from Default argument of state.
State
Zipper-list, representing current state of program. Consists of left-hand List, Value – Bit and right-hand List.
True
Type-level True value, Bit.

Traits§

Bit
Type-level enum of True and False.
Command
Type-level enum of commands. Supertrait of Runner
List
Type-level linked list, enum-like of Nil and Cons
Runner
Represents result of running some Command on State via generic arguments.
StateTrait
Single-type trait for State type, used to get Left, Value and Rigth types.

Type Aliases§

DefaultState
Default state, alias for State<Nil, Default, Nil, Default>.
Run
Alias for running Program on StateT
RuntimeState
Real value of any State.
SetFalse
Sets current bit to False.
SetTrue
Sets current bit to True.