Luna Flow
简体中文

stlc API

stlc 包是基于共享命名语法的简单类型 lambda 演算：类型、带类型常量的签名、类型上下文、双向类型推断与检查、有步数上限的操作式范式化，以及到 β-范式、η-长形式的带类型求值范式化（NbE）。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
  "Luna-Flow/type_theory/stlc",
}

项是 @syntax.Term[Atom]：Bind(x, b) 是 λx. b\lambda x.\,b（不带类型标注），Apply 是应用，Variable 是变量，Value 持有一个 Atom。类型规则和 NbE 算法见 stlc 设计。

语法

Atom

Atom 是该演算中的常量。

pub(all) enum Atom {
  UnitLit
  Const(@core.Name)
} derive(Eq, @debug.Debug)
pub fn Atom::equal(Self, Self) -> Bool

UnitLit 是单位值 ()()；Const(c) 是一个类型在 Signature 中声明的常量。

Term

Term 是 STLC 项的类型。

pub type Term = @syntax.Term[Atom]

它是一个别名，因此 syntax、substitution 和 rewrite 的全部内容都适用于 STLC 项。

Ty

Ty 是简单类型。

pub(all) enum Ty {
  Base(@core.Name)
  Unit
  Arrow(Ty, Ty)
} derive(Eq, @debug.Debug)
pub fn Ty::equal(Self, Self) -> Bool

Base(b) 是未解释的基本类型，Unit 是单位类型，Arrow(a, b) 是函数类型 a→ba \to b。类型按结构进行比较。

签名与上下文

Signature

Signature 为常量指定类型。

pub struct Signature {
  entries : Array[(@core.Name, Ty)]
} derive(Eq, @debug.Debug)
pub fn Signature::empty() -> Self
#alias(extend, deprecated)
pub fn Signature::extend_with(Self, @core.Name, Ty) -> Self
pub fn Signature::lookup(Self, @core.Name) -> Ty?
pub fn Signature::to_array(Self) -> Array[(@core.Name, Ty)]
pub fn Signature::equal(Self, Self) -> Bool

extend_with(c, ty) 返回添加了 c : ty 的新签名；同名的较晚条目会遮蔽较早的条目，lookup 返回最新的那个。to_array 按插入顺序返回条目的副本。

TypeContext

TypeContext 为自由变量指定类型。

pub struct TypeContext {
  entries : Array[(@core.Name, Ty)]
} derive(Eq, @debug.Debug)
pub fn TypeContext::empty() -> Self
#alias(extend, deprecated)
pub fn TypeContext::extend_with(Self, @core.Name, Ty) -> Self
pub fn TypeContext::lookup(Self, @core.Name) -> Ty?
pub fn TypeContext::to_array(Self) -> Array[(@core.Name, Ty)]
pub fn TypeContext::equal(Self, Self) -> Bool

同样的遮蔽规则也适用：类型检查器在进入 lambda 时扩展上下文，因此一个名字由最近的绑定子决定。

test "signatures and contexts" {
  let c = @core.Name::new("c")
  let x = @core.Name::new("x")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let sig = @stlc.Signature::empty().extend_with(c, @stlc.Ty::Arrow(a, a))
  let ctx = @stlc.TypeContext::empty().extend_with(x, a).extend_with(x, @stlc.Ty::Unit)
  assert_eq(sig.lookup(c), Some(@stlc.Ty::Arrow(a, a)))
  assert_eq(ctx.lookup(x), Some(@stlc.Ty::Unit))
  assert_eq(ctx.to_array().length(), 2)
}

错误

TypeError

TypeError 报告项被拒绝的原因。

pub(all) enum TypeError {
  UnboundVariable(@core.Name)
  UnknownConstant(@core.Name)
  CannotInferLambda
  ExpectedFunction(Ty)
  TypeMismatch(expected~ : Ty, actual~ : Ty)
  EmptyApplication
  ScopeError(@debruijn.ScopeError)
  NormalizationError(message~ : String)
} derive(Eq, @debug.Debug)
pub fn TypeError::equal(Self, Self) -> Bool
情形含义
UnboundVariable(x)x 不在上下文中。
UnknownConstant(c)c 不在签名中。
CannotInferLambdalambda 出现在必须推断其类型的位置。
ExpectedFunction(ty)对非函数类型 ty 的项进行了应用。
TypeMismatch(expected, actual)推断出的类型与期望的类型不同。
EmptyApplicationApply(head, []) 没有参数。
ScopeError(e)为 De Bruijn 作用域错误保留；当前的函数不会产生。
NormalizationError(message)带类型 NbE 的内部不变式失败；对已检查的输入不应出现。

类型检查

infer

infer 合成项的类型。

pub fn infer(Signature, TypeContext, @syntax.Term[Atom]) -> Result[Ty, TypeError]

单位字面量的类型是 Unit，常量和变量具有其声明的类型；对于应用 f a_1 … a_n，在将每个参数对照相应的定义域检查之后，其类型为 f 的结果类型。单独的 lambda 无法推断（CannotInferLambda）。直接应用于参数的 lambda 的推断方式是：先推断第一个参数的类型，再在该假设下推断体的类型。

check

check 将项对照类型进行检验。

pub fn check(Signature, TypeContext, @syntax.Term[Atom], Ty) -> Result[Unit, TypeError]

lambda 对照箭头类型进行检查时，会以定义域作为参数的类型，将体对照陪域进行检查。其他所有项都先推断类型，再用 == 比较；若不同则给出 TypeMismatch。

test "infer and check" {
  let x = @core.Name::new("x")
  let f = @core.Name::new("f")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let id : @stlc.Term = Bind(x, Variable(x))
  let sig = @stlc.Signature::empty()
  let ctx = @stlc.TypeContext::empty()
  assert_eq(@stlc.check(sig, ctx, id, @stlc.Ty::Arrow(a, a)), Ok(()))
  assert_eq(@stlc.infer(sig, ctx, id), Err(@stlc.TypeError::CannotInferLambda))
  let ctx_f = ctx.extend_with(f, @stlc.Ty::Arrow(a, a))
  let bad : @stlc.Term = Apply(Variable(f), [Value(@stlc.Atom::UnitLit)])
  assert_eq(
    @stlc.infer(sig, ctx_f, bad),
    Err(@stlc.TypeError::TypeMismatch(expected=a, actual=@stlc.Ty::Unit)),
  )
}

范式化

normalize_checked

normalize_checked 将项对照类型进行检查，然后用无类型的 β-η 归约器对其范式化。

pub fn normalize_checked(Signature, TypeContext, @syntax.Term[Atom], Ty, Int) -> Result[@rewrite.NormalizationResult[Atom], TypeError]

遇到类型错误时，它返回 Err 而不进行归约。否则返回 Ok(@lambda.normalize(term, max_steps))：带步数上限的正规序 β-η 归约。其范式是 β-范式且 η-短的。

normalize_eta_long

normalize_eta_long 将项对照类型进行检查，并返回其 β-范式、η-长形式，该形式通过带类型的求值范式化计算得到。

pub fn normalize_eta_long(Signature, TypeContext, @syntax.Term[Atom], Ty) -> Result[@syntax.Term[Atom], TypeError]

在结果中，每个箭头类型的子项都是 lambda，每个应用的头部都是变量或常量。上下文中的变量和签名中的常量保持原样，并按其类型进行 η-展开。不需要步数上限：良类型的项总能范式化。新的绑定子名称为 x、x_1、…，其选取会避开项和上下文中的所有名字。

test "beta-normal eta-long form" {
  let f = @core.Name::new("f")
  let x = @core.Name::new("x")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let ctx = @stlc.TypeContext::empty().extend_with(f, @stlc.Ty::Arrow(a, a))
  let sig = @stlc.Signature::empty()
  // f is eta-expanded to λx. f x
  let expected : @stlc.Term = Bind(x, Apply(Variable(f), [Variable(x)]))
  match @stlc.normalize_eta_long(sig, ctx, Variable(f), @stlc.Ty::Arrow(a, a)) {
    Ok(normal) => assert_true(@syntax.alpha_equal(normal, expected))
    Err(_) => fail("well typed")
  }
  // the operational normalizer contracts the redex but does not expand
  let redex : @stlc.Term = Apply(Bind(x, Variable(x)), [Variable(f)])
  assert_eq(
    @stlc.normalize_checked(sig, ctx, redex, @stlc.Ty::Arrow(a, a), 10),
    Ok(NormalForm(term=Variable(f), steps=1)),
  )
}

已弃用

已弃用替代项
Signature::extendSignature::extend_with
TypeContext::extendTypeContext::extend_with

本包中各类型上隐藏的方法形式 not_equal 和 to_repr 已弃用；请使用 != 和 Repr(x)。