A weird dependent graph language thing?

weird-lang.md

Notation	Meaning
l ? T	abstract node in T
l : T	concrete node in T
l = t	node equal to t
default = t	reduce to this node if all nodes are concrete
{ ... }	graph term
t1.{ l = t2 }	updates node l in t1 to be t2
t.l	gets the value of node l in t
t.{ l1 -> l2 }	renames l1 to l2 in t
t1 <> t2	merges/composes t1 and t2
{ l1 l2 ? T, ... }	sugar for { l1 ? T, l2 ? T, ... }
{ l1 l2 : T, ... }	sugar for { l1 : T, l2 : T, ... }
{ l ? T1, ... } -> T2	sugar for { l ? T1, ..., default : T2 }
{ l, ... } => t	sugar for { l, ..., default = Type }
{ l : T = t }	sugar for { l : T, l = t }

{
    id : { A ? Type, a ? A, a' : A },
    id = { A, a, a' = a },

    always : { A B ? Type, a ? A, b ? B, a' : A },
    always = id <> { B, b },

    compose : {
        A B C ? Type,
        a->b ? { a ? A, b : B },
        b->c ? { b ? B, c : C },
        a->c : { a ? A, c : C },
    },
    compose = {
        A, B, C, a->b, b->c,
        b = a->b.{ a = a }.b,
        a->c = { c, b->c.{ b = b }.c },
    },

    subst : {
        A B C ? Type, 
        ab->c ? { a ? A, b ? B, c : C },
        a->b ? { a ? A, b : B },
        a->c : { a ? A, c : C },
    },
    subst = {
        A, B, C, ab->c, a->b,
        a->c = { a, c = ab->c.{ a = a, b = a->b.{ a = a }.b }.c },
    },


    Unit : Type,
    Unit = {},

    unit : Unit,
    unit = {},


    Bool : Type,
    Bool = 'true | 'false,

    true : Bool,
    true = 'true,

    false : Bool,
    false = 'false,


    Point2 : Type,
    Point2 = {
        x : F32,
        y : F32,
    },


    Option : { Data ? Type } -> Type,
    Option = { Data } => {
        tag : 'some | 'none,
        data : tag.{
            'some => Data,
            'none => {},
        },
    },

    some : { Data ? Type, data ? Data } -> Option.{ Data = Data },
    some = { Data, data } => { tag = 'some, data = data },

    none : { Data ? Type } -> Option.{ Data = Data },
    none = { Data } => { tag = 'none, data = {} },

    map : { 
        A B ? Type,
        f ? { a ? A } -> B, 
        option ? Option.{ Data = A },
    } -> Option.{ Data = B },
    map = { A, B, f, option } =>
        option.tag.{
            'some => some.{ 
                Data = B, 
                data = f.{ a = option.data },
            },
            'none => {},
        },

    and-then : { 
        A B ? Type,
        f ? { a ? A } -> Option.{ Data = B }, 
        option ? Option.{ Data = A },
    } -> Option.{ Data = B },
    and-then = { A, B, f, option } =>
        option.tag.{
            'some => f.{ a = option.data },
            'none => {},
        },


    Singleton : { Data ? Type, data ? Data } -> Type,
    Singleton = { Data, data } => {
        data : Data,
        data = data,
    },


    Nat : Type,
    Nat = {
        tag : 'zero | 'succ,
        data : tag.{
            'zero => {},
            'succ => Nat,
        },
    },
}

Let expressions:

{
    test : Int,
    test = {
        x : Int = 1,
        y : Int = 2,
    } => x * y,
}

this reduces to:

{
    test : Int,
    test = 3,
}