{{ message }}

Instantly share code, notes, and snippets.

# brendanzab/weird-lang.md

Last active Aug 24, 2020
A weird dependent graph language thing?
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,
}
``````