以 Value 为 Type。 回到我所熟悉的 bidirectional type checker。

由于 simple type 不需要 elaboration， 所以可以简单地写：

check(ctx: Ctx, exp: Exp, type: Value): void
infer(ctx: Ctx, exp: Exp): Value

union

如果想让 define-datatype 所引入的 union 之间，也可以形成子类型关系。 就需要能定制 data 的 hashtag。

(define-datatype exp-t
  (var-exp (name symbol-t))
  (int-exp (value int-t))
  (bool-exp (value bool-t))
  void-exp
  (if-exp (condition exp-t) (then exp-t) (else exp-t))
  (prim-exp (op symbol-t) (args (list-t exp-t)))
  (let-exp (name symbol-t) (rhs exp-t) (body exp-t))
  (begin-exp (sequence (list-t exp-t)))
  (the-exp (type type-t) (exp exp-t)))

改为：

(define-datatype exp-t
  (var-exp [#var (name symbol-t)])
  (int-exp [#int (value int-t)])
  (bool-exp [#bool (value bool-t)])
  (void-exp #void)
  (if-exp [#if (condition exp-t) (then exp-t) (else exp-t)])
  (prim-exp [#prim (op symbol-t) (args (list-t exp-t))])
  (let-exp [#let (name symbol-t) (rhs exp-t) (body exp-t)])
  (begin-exp [#begin (sequence (list-t exp-t))])
  (the-exp [#the (type type-t) (exp exp-t)]))

或：

(define-datatype exp-t
  (var-exp #var (name symbol-t))
  (int-exp #int (value int-t))
  (bool-exp #bool (value bool-t))
  (void-exp #void)
  (if-exp #if (condition exp-t) (then exp-t) (else exp-t))
  (prim-exp #prim (op symbol-t) (args (list-t exp-t)))
  (let-exp #let (name symbol-t) (rhs exp-t) (body exp-t))
  (begin-exp #begin (sequence (list-t exp-t)))
  (the-exp #the (type type-t) (exp exp-t)))

subtype 与 polymorphic 之间的关系

[2026-02-25]

• typeSubtype 不需要处理 type variable 和 unificaton 相关的问题， 因为只要在调用 typeSubtype 之前先做 unificaton， 然后处理 substApplyToType 之后的两个 type， typeSubtype 中原本会遇到 type variable 的地方就都已经被处理完了。

  unificaton 和 typeSubtype 在一个函数中做， 这件事可以作为后续的潜在优化方案。