pijul nest
guest › [sign in] [explore]

update

[?]
Nov 1, 2023, 8:22 PM
PMMOC2YIW57R7PHLDQ7GURO4ST5LKODR3WHGMAZTTW5X2Y6LFOBQC

Dependencies

Change contents

  • file addition: src (d--r------)
    [3.2]
  • file addition: index.res (----------)
    [0.1]
    open Js
    Console.log("hellosu")
  • file addition: data.res (----------)
    [0.1]
    // Disable warning about the same constructor for different types
    @@warning("-30")
    type rec term =
    | Unit // ()
    | Var(string) // x
    | Lam(string, term) // λx.e
    | App(term, term) // e e
    | Annot(term, typ) // (e : A)
    and typ =
    | Unit // 1
    | Var(string) // α
    | Existential(string) // â
    | Polytype(string, typ) // ∀α.A
    | Arrow(typ, typ) // A -> B
    and monotyp =
    // Unit monotype
    | Unit // 1
    | Var(string) // α
    | Existential(string) // â
    | Arrow(monotyp, monotyp) // τ -> σ
    type rec contextEntry =
    | TypeVar(string) // Γ,α
    | TermAnnot(string, typ) // Γ,x:A
    | ExistentialVar(string) // Γ,â
    | ExistentialSolved(string, monotyp) // Γ,â=τ
    | Marker(string) // Γ,🢒â
    type rec completeContextEntry =
    | TypeVar(string) // Ω,α
    | TermAnnot(string, typ) // Ω,x:A
    | ExistentialSolved(string, monotyp) // Ω,â=τ
    | Marker(string) // Ω,🢒â
    type context = list<contextEntry>
    @@warning("+30")
    /** Context lookup */
    let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): typ => {
    switch ctx {
    | list{} => failwith("L")
    | list{TermAnnot(n, t), ..._} if n == name => t
    | list{_, ...rest} => lookupTypeVariable(rest, name)
    }
    }
  • file addition: bidir.res (----------)
    [0.1]
    open Belt
    open Data
    let _genSymCtr = ref(0)
    let genSym = (~prefix="var", ()): string => {
    let num = _genSymCtr.contents
    _genSymCtr := num + 1
    `${prefix}${Int.toString(num)}`
    }
    let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result<context, string> => {
    switch (tyA, tyB) {
    | (_, _) => failwith("TODO")
    }
    }
    and typecheck = (ctx: context, term: term, typ: typ): result<context, string> => {
    switch (term, typ) {
    // 1I rule
    | (Unit, Unit) => Ok(ctx)
    // ∀I rule
    | (e, Polytype(x, tyA)) => failwith("TODO")
    // →I rule
    | (Lam(x, e), Arrow(tyA, tyB)) =>
    let augmentedCtx = ctx->List.add(TermAnnot(x, tyA))
    typecheck(augmentedCtx, e, tyB)->Result.map(_ => ctx)
    // Sub rule
    // TODO: Subtyping rule???
    | (Var(_) | Lam(_, _) | App(_, _) | Annot(_, _), _) => failwith("TODO")
    | _ => Error("could not resolve")
    }
    }
    and synthesize = (ctx: context, term: term): result<(typ, context), string> => {
    switch term {
    // Var rule
    | Var(name) => Ok(lookupTypeVariable(ctx, name), ctx)
    // 1I⇒ rule
    | Unit => Ok(Unit, ctx)
    // Anno rule
    | Annot(e, tyA) => typecheck(ctx, e, tyA)->Result.map(ctx => (tyA, ctx))
    // →I⇒ rule
    | Lam(x, e) =>
    // TODO: Check x and e
    let exA = genSym(~prefix="ex", ())
    let exB = genSym(~prefix="ex", ())
    Ok(Arrow(Existential(exA), Existential(exB)), ctx)
    // →E rule
    | App(e1, e2) => failwith("TODO")
    }
    }
    and appSynthesize = (ctx: context, funTy: typ, term: term): result<(typ, context), string> => {
    switch (funTy, term) {
    // →App rule
    | (Arrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))
    // ∀App rule
    | (Polytype(a, tyA), e) => failwith("TODO")
    // âApp rule
    | (Existential(_), _) => failwith("TODO")
    | (Unit | Var(_), _) => Error("trying to appSynthesize with a non-function type")
    }
    }
    // Figure 8. Applying a context, as a substitution, to a type
    let rec applyContext = (ctx: context, typ: typ): typ => {
    switch typ {
    | Unit => Unit
    | Var(x) => Var(x)
    | Existential(_) => failwith("TODO")
    | Polytype(_) => failwith("TODO")
    | Arrow(a, b) => Arrow(applyContext(ctx, a), applyContext(ctx, b))
    }
    }
  • file addition: package.json (----------)
    [3.2]
    {
    "scripts": {
    "res:build": "rescript",
    "res:dev": "rescript build -w"
    },
    "devDependencies": {
    "rescript": "^10.1.4"
    }
    }
  • file addition: bun.lockb (---r------)
    [3.2]
  • file addition: bsconfig.json (----------)
    [3.2]
    {
    "name": "your-project-name",
    "sources": [
    {
    "dir": "src",
    "subdirs": true
    }
    ],
    "package-specs": [
    {
    "module": "es6",
    "in-source": true
    }
    ],
    "suffix": ".bs.js",
    "bs-dependencies": []
    }
  • replacement in .gitignore at line 4
    [2.6134]→[2.6134:6140](∅→∅)
    _build
    [2.6134]
    _build
    *.bs.js
    node_modules
    lib/bs