some progress on extra exercises

extraexercises.agda

@@ -3,3 +3,42 @@ module extraexercises where
 open import Data.Nat
 open import Relation.Binary.PropositionalEquality as Eq
 open Eq.≡-Reasoning
+
+J : {A : Set}
+  → (C : (x y : A) → x ≡ y → Set)
+  → (c : (x : A) → C x x refl)
+  → (x y : A) → (p : x ≡ y) → C x y p
+J C c x x refl = c x
+
+inv : {A : Set} {a b : A}
+  → (d : a ≡ b)
+  → sym (sym d) ≡ d
+inv {A} {a} {b} d = 
+    J (λ x y p → sym (sym p) ≡ p  ) (λ x → refl) a b d
+
+-- Problem 2
+
+assoc : {A : Set} {a b c d : A}
+  → (e : a ≡ b)
+  → (f : b ≡ c)
+  → (g : c ≡ d)
+  → trans (trans e f) g ≡ trans e (trans f g)
+assoc {a} {b} {c} {d} e f g =
+  let whatever = J {!   !} {!   !} {!   !} {!   !} {!   !} in
+  {!   !}
+
+-- Problem 6
+
+-- id : {A : Set} → (a : A) → a ≡ a
+-- id a = refl
+
+-- interchange : {A : Set}
+--   → (a : A)
+--   → (d : id a ≡ id a)
+--   → (e : id a ≡ id a)
+--   → trans d e ≡ trans e d
+-- interchange a d e =
+--   let transde = trans d e in
+--   let transed = trans e d in
+--   let tmpl = J (λ x y p → {!   !}) (λ x → {!   !}) (id a) (id a) transde in
+--   {!   !}

src/bidir.res

@@ -1,88 +0,0 @@
-open Belt
-open Data
-
-let _genSymCtr = ref(0)
-let genSym = (~prefix="var", ()): string => {
-  let num = _genSymCtr.contents
-  _genSymCtr := num + 1
-  `${prefix}${num->Int.toString}`
-}
-
-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, TUnit) => Ok(ctx)
-
-  // ∀I rule
-  | (e, TPolytype(x, tyA)) => failwith("TODO ∀I-rule")
-
-  // →I rule
-  | (Lam(x, e), TArrow(tyA, tyB)) =>
-    let augmentedCtx = ctx->List.add(TermAnnot(x, tyA))
-    typecheck(augmentedCtx, e, tyB)->Result.map(_ => ctx)
-
-  // Sub rule
-  | (_, _) =>
-    let tyA = synthesize(ctx, term)
-    let tyA' = applyContext(ctx, tyA)
-  }
-}
-
-and synthesize = (ctx: context, term: term): result<(typ, context), string> => {
-  switch term {
-  // Var rule
-  | Var(name) => lookupTypeVariable(ctx, name)->Result.map(ty => (ty, ctx))
-
-  // 1I⇒ rule
-  | Unit => Ok(TUnit, 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", ())
-    let augmentedCtx = list{TermAnnot(x, TVar(exA)), TypeVar(exB), TypeVar(exA), ...ctx}
-    typecheck(augmentedCtx, e, TVar(exB))->Result.map(_ => (
-      TArrow(TExistential(exA), TExistential(exB)),
-      ctx,
-    ))
-
-  // →E rule
-  | App(e1, e2) => synthesize(ctx, e1)->Result.flatMap(((tyA, ctx)) => appSynthesize(ctx, tyA, e2))
-  }
-}
-
-and appSynthesize = (ctx: context, funTy: typ, term: term): result<(typ, context), string> => {
-  switch (funTy, term) {
-  // →App rule
-  | (TArrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))
-
-  // ∀App rule
-  | (TPolytype(a, tyA), e) => failwith("TODO")
-
-  // âApp rule
-  | (TExistential(_), _) => failwith("TODO")
-
-  | (TUnit | TVar(_), _) => Error("trying to appSynthesize with a non-function type")
-  }
-}
-
-// Figure 8. Applying a context, as a substitution, to a type
-and applyContext = (ctx: context, typ: typ): typ => {
-  switch typ {
-  | TUnit => TUnit
-  | TVar(x) => TVar(x)
-  | TExistential(_) => failwith("TODO")
-  | TPolytype(_) => failwith("TODO")
-  | TArrow(a, b) => TArrow(applyContext(ctx, a), applyContext(ctx, b))
-  }
-}

src/data.res

@@ -1,44 +0,0 @@
-type rec term =
-  | Unit // ()
-  | Var(string) // x
-  | Lam(string, term) // λx.e
-  | App(term, term) // e e
-  | Annot(term, typ) // (e : A)
-
-and typ =
-  | TUnit // 1
-  | TVar(string) // α
-  | TExistential(string) // â
-  | TPolytype(string, typ) // ∀α.A
-  | TArrow(typ, typ) // A -> B
-
-and monotyp =
-  // Unit monotype
-  | MUnit // 1
-  | MVar(string) // α
-  | MExistential(string) // â
-  | MArrow(monotyp, monotyp) // τ -> σ
-
-type rec contextEntry =
-  | TypeVar(string) // Γ,α
-  | TermAnnot(string, typ) // Γ,x:A
-  | ExistentialVar(string) // Γ,â
-  | ExistentialSolved(string, monotyp) // Γ,â=τ
-  | Marker(string) // Γ,🢒â
-
-type rec completeContextEntry =
-  | CCTypeVar(string) // Ω,α
-  | CCTermAnnot(string, typ) // Ω,x:A
-  | CCExistentialSolved(string, monotyp) // Ω,â=τ
-  | CCMarker(string) // Ω,🢒â
-
-type context = list<contextEntry>
-
-/** Context lookup */
-let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): result<typ, string> => {
-  switch ctx {
-  | list{} => Error(`could not find name ${name}`)
-  | list{TermAnnot(n, t), ..._} if n == name => Ok(t)
-  | list{_, ...rest} => lookupTypeVariable(rest, name)
-  }
-}

src/index.res

@@ -1,3 +0,0 @@
-open Js
-
-Console.log("hellosu")