Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/simple-optimal.ml

Last active September 1, 2025 19:48
Show Gist options
  • Save EduardoRFS/fab84dbe865cfdfe412f4fd27b55883b to your computer and use it in GitHub Desktop.
Save EduardoRFS/fab84dbe865cfdfe412f4fd27b55883b to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. EduardoRFS revised this gist Aug 31, 2025. 1 changed file with 4 additions and 4 deletions.
    8 changes: 4 additions & 4 deletions simple-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -7,11 +7,11 @@
    you force the head producing a potentially stuck value
    and then apply the new environment, progressing further.
    Lazy act like graph sharing for every reduction on the side.
    And everything on the head is shared by the environment.
    Lazy acts like graph sharing for reductions on the side.
    Everything on the head is shared by the environment.
    To some extent, the env captured by lazy, a form
    of environment sharing, which seems to be fundamental.
    The env captured by lazy makes a form of environment sharing,
    which seems to be a fundamental requirement for optimality.
    *)

    type var = int
  2. EduardoRFS created this gist Aug 31, 2025.
    59 changes: 59 additions & 0 deletions simple-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,59 @@
    (*
    Start with an environment based interpreter that does
    all the reductions, including under lambdas.
    Then make everything not on the head path lazy.
    When you go to evaluate everything on the side,
    you force the head producing a potentially stuck value
    and then apply the new environment, progressing further.
    Lazy act like graph sharing for every reduction on the side.
    And everything on the head is shared by the environment.
    To some extent, the env captured by lazy, a form
    of environment sharing, which seems to be fundamental.
    *)

    type var = int

    type term =
    | T_var of var
    | T_let of var * term lazy_t * term
    | T_lambda of var * term lazy_t
    | T_apply of term * term lazy_t

    and env = E_hole | E_let of env * var * term lazy_t

    let rec lookup env var =
    match env with
    | E_hole -> None
    | E_let (env, env_var, arg) -> (
    match Int.equal var env_var with
    | true -> Some arg
    | false -> lookup env var)

    let rec eval_head env term =
    match term with
    | T_var var -> (
    match lookup env var with Some arg -> Lazy.force arg | None -> T_var var)
    | T_let (var, arg, body) ->
    let arg = eval_lazy env arg in
    let env = E_let (env, var, arg) in
    eval_head env body
    | T_lambda (var, body) ->
    let body = eval_lazy env body in
    T_lambda (var, body)
    | T_apply (funct, arg) -> (
    let funct = eval_head env funct in
    let arg = eval_lazy env arg in
    match funct with
    | T_lambda (var, body) ->
    let env = E_let (E_hole, var, arg) in
    let body = Lazy.force body in
    eval_head env body
    | T_var _ | T_let _ | T_apply _ -> T_apply (funct, arg))

    and eval_lazy env term =
    lazy
    (let term = Lazy.force term in
    eval_head env term)