From 8ce0d1fcb60ca13512f98517083794bd4bcaa1d0 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 22 Oct 2023 19:39:02 -0500 Subject: [PATCH] progress --- bidir/bidir.ts | 57 +++++++++++++++ bidir/contexts.ts | 18 +++++ bidir/data.ts | 42 +++++++++++ extraexercises.agda | 5 ++ hwk1.typ | 175 ++++++++++++++++++++++++-------------------- 5 files changed, 216 insertions(+), 81 deletions(-) create mode 100644 bidir/bidir.ts create mode 100644 bidir/contexts.ts create mode 100644 bidir/data.ts create mode 100644 extraexercises.agda diff --git a/bidir/bidir.ts b/bidir/bidir.ts new file mode 100644 index 0000000..07a0319 --- /dev/null +++ b/bidir/bidir.ts @@ -0,0 +1,57 @@ +import { isTypeInContext } from "./contexts"; +import { ContextEntry, Term, Type } from "./data"; + +function check( + ctx: ContextEntry[], + term: Term, + type: Type +): [boolean, ContextEntry[]] { + switch (term.kind) { + case "var": + break; + case "unit": + return [type.kind === "unit", ctx]; + case "lambda": { + // Get A and B first + if (type.kind !== "arrow") return [false, ctx]; + const { input: A, output: B } = type; + } + case "app": + break; + case "annot": + break; + } +} + +function synthesize(ctx: ContextEntry[], term: Term): [Type, ContextEntry[]] { + switch (term.kind) { + case "var": { + const res = lookupTypeVariable(ctx, term.name); + if (!res) throw new Error("wtf?"); + return [res, ctx]; + } + case "unit": + return [{ kind: "unit" }, ctx]; + case "lambda": { + } + case "app": + break; + case "annot": { + // Require that the type exists + if (!isTypeInContext(term.type, ctx)) + throw new Error("type doesn't exist"); + + // Require that the term checks against the type + const [result, outputCtx] = check(ctx, term.term, term.type); + if (!result) throw new Error("invalid annotation: term doesn't check"); + + return [term.type, outputCtx]; + } + } +} + +function synthesizeApp( + ctx: ContextEntry[], + funcType: Type, + term: Term +): [Type, ContextEntry[]] {} diff --git a/bidir/contexts.ts b/bidir/contexts.ts new file mode 100644 index 0000000..aa57188 --- /dev/null +++ b/bidir/contexts.ts @@ -0,0 +1,18 @@ +// Helper functions for dealing with contexts + +import { ContextEntry, Type } from "./data"; +import { isEqual } from "lodash"; + +/** Γ |- A (is the given type in this context?) */ +export function isTypeInContext(type: Type, ctx: ContextEntry[]): boolean { + for (const entry of ctx) { + switch (entry.kind) { + case "termAnnot": + if (isEqual(entry.type, type)) return true; + break; + default: + continue; + } + } + return false; +} diff --git a/bidir/data.ts b/bidir/data.ts new file mode 100644 index 0000000..276a26d --- /dev/null +++ b/bidir/data.ts @@ -0,0 +1,42 @@ +/** + * Terms e ::= x | () | λx. e | e e | (e : A) + * Types A, B, C ::= 1 | α | ^α | ∀α. A | A → B + * Monotypes τ, σ ::= 1 | α | ^α | τ → σ + * Contexts Γ, ∆, Θ ::= · | Γ, α | Γ, x : A + * | Γ, ^α | Γ, ^α = τ | Γ, I^α + * Complete Contexts Ω ::= · | Ω, α | Ω, x : A + * | Ω, ^α = τ | Ω, I^ + */ + +export type Term = + | { kind: "var"; name: string } + | { kind: "unit" } + | { kind: "lambda"; name: string; body: Term } + | { kind: "app"; func: Term; arg: Term } + | { kind: "annot"; term: Term; type: Type }; + +export type Type = + | { kind: "unit" } + | { kind: "var"; name: string } + | { kind: "existential"; name: string } + | { kind: "poly"; name: string; type: Type } + | { kind: "arrow"; input: Type; output: Type }; + +export type Monotype = + | { kind: "unit" } + | { kind: "var"; name: string } + | { kind: "existential"; name: string } + | { kind: "arrow"; input: Monotype; output: Monotype }; + +export type ContextEntry = + | { kind: "typeVar"; name: string } + | { kind: "termAnnot"; name: string; type: Type } + | { kind: "existentialVar"; name: string } + | { kind: "existentialSolved"; name: string; type: Monotype } + | { kind: "marker"; name: string }; + +export type CompleteContextEntry = + | { kind: "typeVar"; name: string } + | { kind: "termAnnot"; name: string; type: Type } + | { kind: "existentialSolved"; name: string; type: Monotype } + | { kind: "marker"; name: string }; diff --git a/extraexercises.agda b/extraexercises.agda new file mode 100644 index 0000000..caa831e --- /dev/null +++ b/extraexercises.agda @@ -0,0 +1,5 @@ +module extraexercises where + +open import Data.Nat +open import Relation.Binary.PropositionalEquality as Eq +open Eq.≡-Reasoning diff --git a/hwk1.typ b/hwk1.typ index 4750b59..537c520 100644 --- a/hwk1.typ +++ b/hwk1.typ @@ -1,26 +1,36 @@ +#set document(title: "Homework 1", author: "Michael Zhang ") #set page("us-letter") #import "@preview/prooftrees:0.1.0": * += Homework 1 + +Michael Zhang \ + + #let c(body) = { set text(gray) body } -= Problem 1 +$#math.op("f")\(x)$ + +== Problem 1 + +$top : "Set"$ + +$"case"_top$ #c[Define `funsplit` in terms of `apply`.] -$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $ +$ "funsplit"(f, d) &equiv d((x) "apply"(f, x)) $ In the case of $f = lambda b$ the following evaluation occurs: -$ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \ -&equiv d(((x)x)(b)) \ +$ "funsplit"(lambda b, d) &equiv d((x) "apply"(lambda b, x)) \ +&equiv d((x) (b(x))) \ &equiv d(b) $ -NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$? - -= Problem 2 +== Problem 2 #c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove: @@ -91,112 +101,115 @@ $ #tree( ) $ $ #tree( - axi[$x = y in NN [x in NN, y in NN]$], - uni(right_label: "(3, 6)")[$"suc"(x) = "suc"(y) in NN [x in NN, y in NN]$], + axi[$x in NN$], + axi[$y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$], + bin(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN$], + uni(right_label: "(3)")[$"suc"("natrec"(x, 0, (u, v) "suc"(v))) = "suc"(x) in NN$], + uni(right_label: "natrec")[$"natrec"("suc"(x), 0, (u, v) "suc"(v))) = "suc"(x) in NN$], ) $ -$ #tree( +$ #pad(left: -4em, tree( axi(pad(bottom: .2em, [ $x in NN$ \ $"Eq"(NN, "natrec"(n, 0, (u, v) "suc"(v)), n) "set" [n in NN]$ \ $"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$ \ $"eq"_"suc" (x, y) in "Eq"(NN, "natrec"("suc"(x), 0, (u, v) "suc"(v)), "suc"(x)) [x in NN, y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)]$ \ ])), - uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$], -) $ + uni(right_label: "(7, 9, 10)")[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$], +)) $ #tree( axi[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$], - uni(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$], + uni(right_label: "(5, 11)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$], uni(right_label: [#sym.plus.circle])[$plus.circle(x, 0) = x in NN [x in NN]$], ) -#pagebreak() +// #pagebreak() -Then, we can use this: +// Then, we can use this: -#set math.equation(numbering: none) +// #set math.equation(numbering: none) -#tree( - axi[$0 in NN$], - uni(right_label: "(1)")[$0 = 0 in NN$], - uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$], -) +// #tree( +// axi[$0 in NN$], +// uni(right_label: "(1)")[$0 = 0 in NN$], +// uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$], +// ) -Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence: +// Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence: -#tree( - axi[$"suc"(x) in C(x) [x in NN]$], - axi[$x = y in NN$], - bin[$"suc"(x) = "suc"(y) in NN$], -) +// #tree( +// axi[$"suc"(x) in C(x) [x in NN]$], +// axi[$x = y in NN$], +// bin[$"suc"(x) = "suc"(y) in NN$], +// ) -Then, convert this to Eq: +// Then, convert this to Eq: -#tree( - axi[$"suc"(x) = "suc"(y) in NN$], - axi[$x = y in NN$], - bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$], -) +// #tree( +// axi[$"suc"(x) = "suc"(y) in NN$], +// axi[$x = y in NN$], +// bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$], +// ) -We can form a lambda term over eq objects using $lambda$-introduction: +// We can form a lambda term over eq objects using $lambda$-introduction: -#tree( - axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$], - uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$], -) +// #tree( +// axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$], +// uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$], +// ) -This gives us what we need to perform induction over nats: +// This gives us what we need to perform induction over nats: -#tree( - axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$], - uni[] -) +// #tree( +// axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$], +// uni[] +// ) -#tree( - axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$], - uni[], -) +// #tree( +// axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$], +// uni[], +// ) -#tree( - axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$], - uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$], - uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$], -) +// #tree( +// axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$], +// uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$], +// uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$], +// ) ---- -#pagebreak() +// --- +// #pagebreak() -#{ - let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$] +// #{ +// let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$] - tree( - axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$], - uni[$split1 equiv x in NN [x in NN]$], - ) +// tree( +// axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$], +// uni[$split1 equiv x in NN [x in NN]$], +// ) - tree( - // axi[$c in "Eq"(NN, split1, 0), x)$], - axi[$split1 equiv x in NN [x in NN]$], - uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$], - ) +// tree( +// // axi[$c in "Eq"(NN, split1, 0), x)$], +// axi[$split1 equiv x in NN [x in NN]$], +// uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$], +// ) - tree( - axi[$c in "Eq"(NN, plus.circle(x, 0), x)$], - uni[$plus.circle(x, 0) equiv x in NN [x in NN]$], - ) +// tree( +// axi[$c in "Eq"(NN, plus.circle(x, 0), x)$], +// uni[$plus.circle(x, 0) equiv x in NN [x in NN]$], +// ) - tree( - axi[$plus.circle(x, 0) equiv split1 [x in NN]$], - ) +// tree( +// axi[$plus.circle(x, 0) equiv split1 [x in NN]$], +// ) - tree( - axi[$split1 equiv x [x in NN]$], - ) +// tree( +// axi[$split1 equiv x [x in NN]$], +// ) - tree( - axi[$plus.circle(x, 0) equiv split1 [x in NN]$], - axi[$split1 equiv x [x in NN]$], - bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$], - ) -} \ No newline at end of file +// tree( +// axi[$plus.circle(x, 0) equiv split1 [x in NN]$], +// axi[$split1 equiv x [x in NN]$], +// bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$], +// ) +// } \ No newline at end of file