Major breakthrough in path semantics: First working prototype of dependently paths!!!!

example.rs

/*
Diary, Sven Nilsen, 15.09.2016:

Reading mathematical papers does help.
Woke up with an idea that arguments could be represented as tuples.
This idea turned into functional currying.
Started coding from scratch today (in Rust of course!) and came this far.
I think I'm starting to understand how dependently types work!

Path semantics is a new field that might make dependently types more powerful and practical.
It fits natural language in an intuitive way, and might be easier to use for productivity,
since you can add more paths later without changing the types.

The notation is used informally to reason about complex problems and derive algorithms in the Piston project.
It was also the major driving force of designing and bootstrapping the meta language in Piston-Meta.
*/

let p = prog!(
    // These 3 lines are not needed for this simple example,
    // but will be used in type checker for a fully working language.
    (is_even -> f64 -> bool)
    (is_even -> : 0 -> : true) // More powerful language will use modulus.
    (is_even -> : 1 -> : false)

    (add -> f64 -> f64 -> f64)
    // Paths is a generalization type relations, constructed using functions.
    (add -> is_even : X -> is_even : Y -> is_even : (X = Y))
);
let a = progln!(add -> is_even : true -> is_even : true);
// Evaluation is a lot more complex than normal programming languages.
// For example, "local variables" are stored as proofs of dependently paths!
// This architecture might make it easier to do other kinds of constraints in the future...
eval(&a, p).println();

// Output:
is_even : true

// Yay! We "proved" that when you add two even numbers, you get an even number!