Affine Lambda Calculus written purely in Typescript's type system

affine-lambda-calculus.ts

// the [Scope] of a [Expression] holds unbound variables
// in this implementation, scope works from the bottom-up:
// Var consumes declares a variable as consumed: (Var "a") :: { scope: { a: true } }
// Lambda supplies a variable, making it fresh
// Application joins the dependencies of its expressions: (Apply (Var "a") (Var "b")) :: { scope: { a: true, b: true } }
// and guarantees that its Lambda body cannot consume variables that its Argument has marked as consumed
//  (Apply (Var "a") (Var "a")) will declare { a: false } so that its body can't use { a: true }

// The motivation for evaluating this bottom-up is that, on the type level, Typescript 
// would require Context to be passed as a separate parameter for every single expression if evaluated top-down. 
// This would force users to manually calculate and input the scope for each expression, instead of it being inferred.

// there is also a previous attempt, which counts and incremetns each usage of a var (failed)
// https://www.typescriptlang.org/play?#code/FAOwhgtgpgzgDmAxlABAGQMIoN7GCglAeiJQBcALVAZUQHs5U6AzFMFAbQFEAPOAJ1gwAlnRABdFPQCuIMjBQU6AdxQQwIAJ7lh0Bew4A1MP0kUwCgEZQoIKWJjToAE3yESKYXcrCFuuAA2UNByYGSiIAA0KDD0jCjKdPwA1grM-HQQ5FQolnRkZJkAtNJwAFxuBB7G-PYgjnoozlCIASawbCgAbibCYJZBdQ1QzmUoABQ1KABEYNMAlChlY9gxcVArbGPT1NMoAL4HlcSkAIJwgcKIYREoAFZ0XgqUqM2MIM0giMIdLJ7yKCgfEEMBEDjG43OgW0kxMMzmi1htWmlgWi2WODWDA2mLA2120Us+L2h32xw8GhQUICVxuYjYARgdBiTgUSlU6i0OkaUCQFG6vX6g2UFiGThGADoJtSYVNZgsJnKEejNrFsZs8TNqLsDrqUOTSGhIJZnOxrnZHBcAtp2D1+H0BqhCtkoMJanlnJoAOQKNWMQnSMgugX2oWoCDSGBB6xilyAnhIMjWlBiZATHYLPCEE4oAAqOQg+WEPXC9OYSUBPQC0huIAA5tlfLl8oUICU4J5nuYyNF6S9yJp4kEulAAtFc4PYIh7XAgwaEnRpAFnChBABHaRu1AYMRkIFB50xhCgkZsfQxKAIfhhVBXyBQPe1cu1KAj-jaET1wZAgRCW7CVhXzAasbxXQo4CKZwVBAKV53zJtEiXFdnzTSMoH4Z5mU5GsAmTa4AkQJcbzYD5PBAOBA2DP1UGfQE+XjX9QQiaInj3MAVz+YRo1desyOYdDBGcCUs0IMhJxQWhsRQABeTEOA7LwYjIe163EMYoxUhsyWOMT4gALXQ5lZIAA2MnTxIAeRAVBZIASS+AAeAyMgAPnM+J7MQBzc3jPcPl9ZSvDrFyZJQYyABJsFzfZqDM7NdNQAARFp+G83zbGcALNJC2SfP3DKFAi7AvH42oAFUYuMlAAH4UDKpYUGcuh3JoJw0vy-ylM08cACZ0s6jSgpysLIui0aev2Mz5yNCATXYOsHwURAKGEZdfXWEiVwEOgumEZoFAABRMSApQwFbl31bMPBK9DbDTc0QHyBcUmbApilKGIvHu87nFOKRKWaTkVyZaAfF4xSr1sMgACFNpQSG5D+xCLvMEdyGZKs9uIygwhEggEpQXhGLBOxZJqByNE0EKAB90GNU0Ka0aJKZpqkrVpUsQEZzRma0NyWpQcnDH6zKuqG0LVgSsYvTtL1omSKBNDGQxomozYOGSMjBbUlArNQUk8YYpID3Ema5oc4WOtFwb62iaG6E9EWFCJkESZy45s0lydpbaWbTTl+HjogZXCQdpWUHtz1VfWMZqFKaEHMjzQOB9dYvXEaJDBCw4PEEQsRy7V5gg0FdDENn9jYHeJqQ5iIHIAJSdwngT-MRojQJuXdbkB3ezT2q5xL0wHZ65OYD325rGNBojvYOUHr6P1RQABZdCFrjiAHLQFPqPT6J653tPxGznNoH4BaFEBkuYENilmGYLxUAn01-oIpdI3IdCIHnc1clQeh6jKWkIgPcK4AKATfNoO0nYUwgDwg4CMcZUxQAFqcTA7UeB+VFhZCAXEHJdyYm3GY1FpghQAGSYjVnJBSFpAqqWqtsEkBxhq5lvqQM+F8UAUIaEtBwThZwRBvldUgj0gxoWBl9VAghmCJiSALVe58oAbwclgK2ChJL+hQBgPqaiJLrF7n3Agqx5JawVpoP4WBaZmIsT1HWyiOy6OsawLAtUMDyUkGMJqM8m5OK0X1VxPV3ENSatnNhTQUrBChgoSMYAFoplYAAaXnKIlA4jPpfCkVAGRIC5HxXEnHK0mgVFNw0VAaICSfGKwsTPQQXQm42wbLJNxCTj4yQ9oQX8dTdGyGaA-ayrhDEEFcVw6hWsWljD1kcQZDUcF4IwOU8hclNaKXGSgZK04HKdNCQLAA+vIegEAKJ7nwZ3FuhCohaNClwQ+2J07DWMTQlAviMA6zcXASQ2lszNFaO0IYQZgizk0BZSwdwWhkGoJoWadAAhjFkMIDcqAYCQryAEAA3McCu-ATbxC4IcsSwLQUgIlpwAF+KQVgohVCgI4gGEoGsm+A46LsyYuxagWyMBcWAoJWC7yLDO54qBeSoltUgGoDGDIxkUB0VhJ4CgIoIUeAAEJdkAAZQpoIwFvemYAHJeh4AHcmeqvQuRNTKuVCrzUoG0PKq1yq8nxB4DwTQ2hZIaq1X7HVRr27at1fq71HrdXekziYQNxqTWmvnLKm1UaQoAC9LVKt2aoV16CzYMy9XTANGa02etjQakNRrw0RuESgGNExrUhU0Iq+Y4wlWLF2TsxIyaqSpp9Rmmuo866Gv1S5f15svRBsFgW70Rb+YlrLeMCtpbq21urfOLwmMwLe1LTAtJZBlBXDKbkSi21drNA4hkiYBNVg8GJLqJsKSLAiDrOAR06MB6YlPVqEk8wk0qHVa2rNfq2aXE7WIC2Bae19vTYO7tYbw1mptZOhNM662ztfSWhdwE9oDzGLKpsa6KCCCdLoWAAYgy7r2qeZBR7xInvxDqQ4F6npXuEDesM97j2lrPfsBDolxI7M402j9mqc2+oDh2ukXMwO9p-TSP9wnAPGuA560DUnR1jvcKQeD8H50gEXahldTZgKCHYtoNJilqINs44299KbNWCc5gB1Khbg02Z7RGskQA

type Scope = { [p in string]: boolean }

// careful, 'Expression' cannot circularly reference itself :p
type Expression = Lambda<any, any> | Application<any, any> | Var<any>

type Var<V extends string> = { // var declares in the scope it consumes V
    type: 'var',
    key: V
    scope: { [k in V]: true },
}

type Lambda<V extends string, Body extends Expression> = {
    type: 'lambda',
    arg: V,
    body: Body,
    scope: _tscompute<Omit<Body['scope'], V>>
}

type InvalidateArgConsumptions<A extends Scope> =
    Scope & { [p in keyof A]?: false }

// applies (A)rgument to (L)ambda
type Application<A extends Expression, L extends Expression & { scope: InvalidateArgConsumptions<A['scope']> }> = {
    type: 'application',
    lambda: L,
    arg: A,
    // anything consumed in the arg cannot be consumed in the body
    // remove (consumed) args in A from L, then merge remaining scope
    scope: _tscompute<Omit<L['scope'], keyof A['scope']> & A['scope']>
}

// (optional) computes the type fully so it can be seen in type hints, for debugging purposes
// also, forces typescript to behave correctly and not be lazy!
type _tscompute<T> = T extends unknown ? { [K in keyof T]: T[K] } : never;

// x -> x!
type id = Lambda<'x', Var<'x'>>
// x -> y! (unbound y)
type _1 = Lambda<'x', Var<'y'>>

// x -> y -> z! (unbound z)
type __w = Lambda<'x', Lambda<'y', Var<'z'>>>
// x -> x -> y -> y!
type xxyy = Lambda<'x', Lambda<'x', Lambda<'y', Var<'y'>>>>

// x -> x -> z -> x!
type _w = Lambda<'x', Lambda<'x', Lambda<'z', Var<'x'>>>>

// x -> (y -> y!)(x!) 
type __wow = Lambda<'x', Application<Var<'x'>, Lambda<'y', Var<'y'>>>>


//            v error
// x -> (y -> x!)(x!)
// invalid type: x is used twice, but provided once (The types of 'scope.x' are incompatible between these types: 'true' is not assignable to type 'false')
type _wow = Lambda<'x', Application<Var<'x'>, Lambda<'y', Var<'x'>>>>

//                v error
// x -> (x -> x!)(x!)(x!)
// invalid type: x is used three times, but provided once (The types of 'scope.x' are incompatible between these types: 'true' is not assignable to type 'false')
type ___wow = Lambda<'x', Application<Var<'x'>, Application<Var<'x'>, Lambda<'x', Var<'x'>>>>>

//       v error
// x -> (x!)(x!)
// invalid type: x is used twice, but provided once (The types of 'scope.x' are incompatible between these types: 'true' is not assignable to type 'false')
type ____wow = Lambda<'x', Application<Var<'x'>, Var<'x'>>>

//  v error
// (x!)(x!)
// invalid type: x is already used in scope
type _____wow = Application<Var<'x'>, Var<'x'>>

type __ = Application<Var<'x'>, xxyy>


/*
 * reduce ctx expr = match expr
 *  lambda arg body => lambda             
 *  var k => var                   
 *  application argexpr lexpr {   
 *      lambda: Lambda = reduce ctx lexpr 
 *      arg: Lambda = reduce ctx argexpr 
 *      reduce (bind lambda.body lambda.key arg) ctx
 *  }
 * 
 * bind body key arg = match body
 *    var k => k == key ? arg : var k
 *    application argexpr lexpr = { application with arg = bind argexpr key arg, lambda = bind lexpr key arg }
 *    lambda k body => k == key ? lambda : { lambda with body = bind body key arg }
 */

type Normalize<P extends Expression> =
    P extends Lambda<infer K, infer B> ? P :
    P extends Var<infer Key> ? P :
    P extends Application<infer Arg, infer L> ?
    /**/ Normalize<L> extends Lambda<infer Key, infer Body> ?
    /**/ Normalize<Arg> extends infer U ? Normalize<Reduce<Body, Key, Cast<U, Expression>>> : never : never
    // /**/ Reduce<L, Ctx> extends Lambda<infer Key, infer Body> ?
    // /*    */ Reduce<Body, Ctx & { [p in Key]: Reduce<Arg, Ctx> }> : never : never
    // lots of meaningless `extends infer U ? U : never` and Cast<A,B> so typescript doesn't error "Type instantiation is excessively deep and possibly infinite"
    : never

type Cast<A, B> = A extends B ? A : never

type Reduce<E extends Expression, Key extends string, V extends Expression> =
    E extends Var<infer K> ? K extends Key ? V : E :
    E extends Application<infer Arg, infer Body> ? Update_cc<E, { lambda: Reduce<Body, Key, V>, arg: Reduce<Arg, Key, V> }> :
    E extends Lambda<infer K, infer Body> ? K extends Key ? E : Update_cc<E, { body: Reduce<Body, Key, V> }> : never

// update, compute, cast
type Update_cc<T, T2> = _tscompute<Omit<T, keyof T2> & { [p in keyof T2]: _tscompute<T2[p]> }>
// type Update_cc<T, T2, T3> = _tscompute<Cast<Omit<T, keyof T2> & { [p in keyof T2]: _tscompute<T2[p]> }, T3>>

// (bool -> ontrue -> onfalse -> ((bool)(ontrue))(onfalse))(x -> y -> x)(x -> x)(x -> x)
// (ontrue -> onfalse -> ((x -> y -> x)(ontrue))(onfalse))(x -> x)(x -> x)
// (onfalse -> ((x -> y -> x)(x -> x))(onfalse))(x -> x)
// ((x -> y -> x)(x -> x))(x -> x)
// (y -> x -> x)(x -> x)
// (x -> x)
type partial_1 = Normalize<Application<_true, ifelse>>
type partial_2 = Normalize<Application<idtrue, Application<_true, ifelse>>>
type result_true = Normalize<Application<idfalse, Application<idtrue, Application<_true, ifelse>>>>
type result_false = Normalize<Application<idfalse, Application<idtrue, Application<_false, ifelse>>>>
type x_y_z_x = Lambda<'x', Lambda<'y', Lambda<'z', Var<'x'>>>>

// (λf.(f (λx. x)) (λz. (z (λy. y)))
// ((z) => z((y) => y)
// ((f) => f((x) => x))((z) => z((y) => y))

// let fun = (f => f(x => x))
// let arg = (z => z(y => y)))
// fun(arg)

// (x -> y -> z -> x)(x -> y -> x)
// y -> z -> x -> y -> x
type partial1 = Normalize<Application<_true, x_y_z_x>>
// (y -> z -> x -> y -> x)(x -> x)
// (z -> x -> y -> x)
type partial2 = Normalize<Application<idtrue, Application<_true, x_y_z_x>>>
// (z -> x -> y -> x)(x -> x)
// (x -> y -> x)
type xyzx_result = Normalize<Application<idfalse, Application<idtrue, Application<_true, x_y_z_x>>>>

type idtrue = Lambda<'x', Var<'x'>> & { __id: "this when condition true" }
type idfalse = Lambda<'y', Var<'y'>> & { __id: "this when condition false" }

type _www = Normalize<Application<Var<'x'>, Var<'y'>>>

// x -> y -> x
type _true = Lambda<'x', Lambda<'y', Var<'x'>>>
// x -> y -> y
type _false = Lambda<'x', Lambda<'y', Var<'y'>>>
// bool -> ontrue -> onfalse -> (bool(ontrue))(onfalse)
type ifelse = Lambda<'bool', Lambda<'ontrue', Lambda<'onfalse', Application<Var<'onfalse'>, Application<Var<'ontrue'>, Var<'bool'>>>>>>