A lambda calculus for the HVM

[August-Alm]

Hi!

The HVM builds upon Lamping's abstract algorithm (the oracle-free part) and hence it cannot correctly reduce all lambda terms. The most succinct characterisation of which terms that are allowed is that "no clone may it's own clones". However, as far as I know there is no type theory that characterises this set of allowable terms, hence no type checker that can identify them; nor is there anything resembling a "borrow checker" that can do so. An early version of the Kind/Formality language used a lambda calculus based on Elementary Affine Logic (EAL) for this very reason, because EAL lambda terms belong to the class of terms that reduce correctly. However, the EAL conditions are much stronger than they need to be -- many more terms than those still reduce correctly. And EAL is, in my opinion at least, a bit weird semantically to program in.

I'd like to throw another ball into the air here. A computer scientist called Damiano Mazza has invented something he calls the Parsimonious Lambda Calculus. A simplified version of it, that I'd like to call the Very Parsimonious Lambda Calculus, is, in my mind, a much nicer calculus than EAL for practical programming, whilst still being reducible without an oracle. I don't think it captures all of the terms that reduce correctly, but more than EAL, and in a way that is easier for practical programming. Unlike EAL, it can also easily support recursion in the form of a Y-combinator.

The syntax extends the ordinary lambda calculus with a new form of abstraction lam! x. b and a modality !t. These combine in a new reduction rule, which, just like one would suspect, says that (lam! x. b !t) = b[t/x]. What makes the terms of this calculus reduce correctly without oracle is a kind of usage regiment:

Say that the "depth" of a variable x in a term t is the number of !:s inside of which it is nested.
In an ordinary lambda lam x.b, x occurs at most once in b and then only in depth zero.
In a lam! x.b, x can occur any number of times in depth zero, at most once in depth one, and not in higher depths.

So, for example, two = lam! s. lam z. (s (s z)) is a perfectly valid term. Recursion can be added in the form of a Y = (X !X) with
X = lam! x. lam! f. (f (x !x) f). (In the simple type system below, extended with polymorphism, (two !two) is not tapeable nor is X, but one can still add Y as a primitive of type forall a. !(a -> a) -> a. Note that recursion is restrained to be linear; one will have a "let rec f = bod" where bod can only contain one recursive call of f. Bit hard to write but opens up the possibility of automatically converting all recursions to tail-call / while loops.)

Semantically, one should think of !t as a constant stream of t:s. Or as a continuous emitter of t:s (compare with the ! in pi-calculus). One can pop/read as many t:s from it as one likes, without using the stream. Apart from that popping business everything is affine. (And applying ! means "pinning" a value as a constant stream.)

Moreover, these stratification rules can easily be incorporated in a type checker. Below is a small bidirectional implementation (in F#) of the "simply typed very parsimonious lambda calculus".

  type Typ = O | Hom of Typ * Typ | Box of Typ

  /// Terms of the simply typed very parsimonious lambda calculus.
  type Term =
    | Var of string
    | LamAff of string * (Term -> Term)
    | LamBox of string * (Term -> Term)
    | App of Term * Term
    | Box of Term
    | Ann of Term * Typ
  
  /// Weak head normal form reduction.
  let rec reduce t =
    match t with
    | App (f, a) ->
      match reduce f, a with
      | LamAff (_, b), a -> reduce (b a)
      | LamBox (_, b), Box a -> reduce (b a)
      | _ -> t
    | _ -> t
  
  type Usage = Lin of int | Exp of int | Used
  
  type Typing = { Name : string; mutable Usage : Usage; Typ : Typ }

  /// Bidirectional type inference.
  let rec infer ctx dep trm =
    match trm with
    | Var x ->
      match List.tryFind (fun ting -> ting.Name = x) ctx with
      | None -> failwith $"Untyped var {x}."
      | Some ting ->
        match ting.Usage with
        | Lin d when d = dep -> ting.Usage <- Used; ting.Typ
        | Lin _ -> failwith $"Linear var {x} breaks depth restriction."
        | Exp d when d = dep -> ting.Typ
        | Exp d when d = dep - 1 -> ting.Usage <- Used; ting.Typ
        | Exp _ -> failwith $"Exponential var {x} breaks depth restriction."
        | Used -> failwith $"Var {x} breaks affine usage rules."
    | LamAff _ | LamBox _ -> failwith "Can't infer types of raw lambdas."
    | App (f, a) ->
      match infer ctx dep f with
      | Hom (d, c) -> check ctx dep a d; c
      | _ -> failwith $"Inferred non-function application in {trm}."
    | Box t -> Typ.Box (infer ctx (dep + 1) t)
    | Ann (t, typ) -> check ctx dep t typ; typ
  
  /// Bidirectional type checking.
  and check ctx dep trm typ =
    match trm with
    | LamAff (x, b) ->
      match typ with
      | Hom (c, d) ->
        let xc = { Name = x; Usage = Lin dep; Typ = c }
        check (xc :: ctx) dep (b (Var x)) d
      | _ -> failwith $"Affine lambda can't have non-function type {typ}."
    | LamBox (x, b) ->
      match typ with
      | Hom (Typ.Box c, d) ->
        let xc = { Name = x; Usage = Exp dep; Typ = c }
        check (xc :: ctx) dep (b (Var x)) d
      | _ -> failwith $"Box-lambda can't have non-box-function type {typ}."
    | Box t ->
      match typ with
      | Typ.Box ty -> check ctx (dep + 1) t ty
      | _ -> failwith $"Type mismatch, box {trm} cannot have non-box type {typ}."
    | _ ->
      let inf = infer ctx dep trm
      if inf <> typ then
        failwith $"Type mismatch, inferred {inf} instead of {typ}."

[VictorTaelin]

That is amazing. I don't have much else to comment, but I'll be soon incorporating a HVM compatibility checker on Kind2. I have a different idea in mind, but if it doesn't work, that calculus looks like a much superior option than EAL.