diff --git a/extraexercises.agda b/extraexercises.agda index caa831e..f885f9d 100644 --- a/extraexercises.agda +++ b/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 +-- {! !} \ No newline at end of file diff --git a/src/bidir.res b/src/bidir.res deleted file mode 100644 index 51bef48..0000000 --- a/src/bidir.res +++ /dev/null @@ -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 => { - switch (tyA, tyB) { - | (_, _) => failwith("TODO") - } -} - -and typecheck = (ctx: context, term: term, typ: typ): result => { - 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)) - } -} diff --git a/src/data.res b/src/data.res deleted file mode 100644 index d64a93a..0000000 --- a/src/data.res +++ /dev/null @@ -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 - -/** Context lookup */ -let rec lookupTypeVariable = (ctx: list, name: string): result => { - switch ctx { - | list{} => Error(`could not find name ${name}`) - | list{TermAnnot(n, t), ..._} if n == name => Ok(t) - | list{_, ...rest} => lookupTypeVariable(rest, name) - } -} diff --git a/src/index.res b/src/index.res deleted file mode 100644 index f0554e0..0000000 --- a/src/index.res +++ /dev/null @@ -1,3 +0,0 @@ -open Js - -Console.log("hellosu")