[question] if a value is evaluated in `ctx1`, is it safe to readback it in a different `ctx2`? about cicada-plct HOT 6 CLOSED

I think it's safe except for some name conflicts

Ctx plays two roles in this process.

The first one is for the name conflicts. I don't think this one will be too much of a problem.

And the other one is for some type refinements of TypeScript (such as assertClazzInCtx(ctx, restValue)). I guess they're just written for the TS compiler and won't fail in any situation.

from cicada-plct.

Example by @LittleJianCH

import { test } from "vitest"
import { Closure } from "../closure"
import * as Cores from "../core"
import { evaluate } from "../core"
import { CtxCons, CtxNull, ctxToEnv } from "../ctx"
import { EnvCons, EnvNull } from "../env"
import * as Values from "../value"
import { readback } from "../value"

test("Example", () => {
  const core = Cores.Fn("a", Cores.Cons(Cores.Var("a"), Cores.Var("a1")))
  const ctx1 = CtxCons("a1", Values.String(), CtxNull()) // a1: String
  const ctx2 = CtxCons("a", Values.String(), CtxNull()) // a: String
  const pSS = Values.Sigma(
    Values.String(),
    Closure(EnvCons("x", Values.String(), EnvNull()), "_", Cores.Var("x")),
  ) // Pair(String, String)
  const S2pSS = Values.Pi(
    Values.String(),
    Closure(EnvCons("x", pSS, EnvNull()), "a", Cores.Var("x")),
  ) // String -> Pair(String, String)s

  const value = evaluate(ctxToEnv(ctx1), core)
  console.log(value)
  const core_ = readback(ctx2, S2pSS, value)
  console.log(core_)
})

from cicada-plct.

But the following cicada code is OK:

let StringPair = Pair(String, String)
let StringToStringPair = (String) -> Pair(String, String)

function f(a: String, a1: String): Trivial {
  let x: StringToStringPair = (a) => cons(a, a1)
  return sole
}

from cicada-plct.

Why we need freshName in readback again?

from cicada-plct.

首先 ctx 记录了在递归处理 Exp 时，当前的 scope。

随着我们深入表达式内部，scope 会逐渐扩展，
因为有一些表达式，诸如 Pi、Sigma 和 Lambda，
会引入 name 到 type （或 value）的 binding。

readback 必须引入新的、没有在当前 scope 中出现过 name，
这个 name 将用来制作新的带有 binding 的表达式，
这个 binding 表达式的内部表达式，
是递归的 readback 而得到的 partial evaluation 的结果，
即，用这个 name 构造一个 variable，
然后把 closure apply 到这个 variable 上得到 value，
再递归 readback。

因为已经在 scope 中出现过的 name，
对 closure 内部的表达式来说是 free variable，
我们构造新的 binding 的时候，
不能将原本 free 的 variable 变成 bound variable，
所以 readback 的过程中，要找一个「没有在当前 scope 中出现过 name」。

from cicada-plct.

实际上在 infer 和 check 中使用 readback，也并没有改变破坏 scope。

因为在 infer 和 check 中所得到的 value，
要么是在当前的 scope 中 evaluate 得到的，
要么是在更外层的 scope 中 evaluate 得到的。

from cicada-plct.