Skip to content

LOG.md

Latest commit

 

History

History
185 lines (127 loc) · 6.06 KB

LOG.md

File metadata and controls

185 lines (127 loc) · 6.06 KB

Week 1

  • Setting up dune project and environment

  • Untyped lambda calculus and beta reduction in lib/untyped_lambda_calculus

    • Added sexp based parsing with quickcheck round trip tests

  • Untyped nameless lambda calculus in lib/untyped_nameless

    • DeBruijn Indicies with remove_names and restore_names
    • Quickcheck roundtrip tests for removing and restoring variable names
    • Evaluation with shift/subst

  • Start of simply typed lambda calculus in simply_typed_lambda_calculus

    • bool and -> types only

  • Refactoring codebase

  • Bonsai based typing judgement visualizer, rendered with MathJax

Week 2

  • Extensions to Simple Types (Chapter 8/11/12) in lib/simply_typed_extended

    • seq, let, as
    • tuples, records, and variants with projection functions
    • Syntactic sugar (dropping some parens in let/fun, implicit < variant > = < variant : #u >
    • (Exhaustive) pattern matching with (case _ of _)
    • Nat, zero, succ, pred, iszero
    • fix point with letrec

  • Simple beta reduction eval (no closures)

    • Examples and test cases

  • Some debugging on LaTeX generation

Week 3

  • Parser Combinator Library, porting from Abstract Machine project

    • Convert to use Core's Monad.Make and Applicative.Make
    • Add Alternative and Functor syntax
    • Use stream of (char * pos) Sequence.t instead of char list

  • Implement parser combinator for ty and t (lots of retries)

    • Big test function takes ~60 seconds to parse (guessing issue is with too many strips)

    • Refactor to remove some backtracking (~30 seconds)

    • Implementation of Lexer to tokens

      • Convert Parser to be a functor Chomp.Make(Lexer)
      • Parses arbitrary tokens instead of string
      • Cuts down big test function to ~20 seconds

    • Refactor parser to use commit on first token (~12 seconds)

    • Refactor parser to postfix forms that have valid expressions as a prefix (~1 second)

  • Simple REPL interface (not a true repl, just expression evaluator)

Week 4

  • Completely move sexp based tests to chomp based test

  • shift/subst based evaluation of simply_typed_extended

    • Closures naturally supported now, added tests
    • Refactor to use eval1 to follow small step semantics more directly

  • Merging typechecker and evaluation tests

  • ref, !, and := type checking and parsing, adding tests

  • Refactoring using Store (state monad implementation of mu) for ref-related evaluation

  • Fix issue in REPL where Ctrl-D causes error due to In_channel.input_line_exn

Week 5

  • Move Lexer to chomp since it will be shared for most impls, but keep generic Parser functor

  • Start work on subtyping

    • Add parsers for top type and modified variants (no longer needs to be ascribed to type), patching tests
    • Implement subtyping <: and patch in terms that don't require join/meet, replacing most equal_tys
    • join for if and match, adding tests
    • Minimal bot type implemented
    • Add error form with bot type, adding tests
    • Set bool <: nat (implicitly, #f => 0 and #t => 1)

  • Generic REPL implementation supporting subtyping

  • Makefile

Week 6

  • eval for subtyping, adding error/exception forms

  • featherweight_java (implementation was almost directly from the helper functions and rules in TAPL)

    • Parser for FJ, does not check if constructor has exact required order or contents
    • Tests for term and class_decl parsing
    • Typecheck term
    • Typecheck methods and class declarations
    • Evaluation of term given class_decls (uses subtyping!)
    • Complete tests for typecheck/eval
    • REPL support

Week 7

  • Recursive Types!

    • This was not an implementation chapter, it was a bit of a struggle
    • Github repository with implementations did not include subtyping either :(

  • Parser for recursive types (mostly copied)

  • Typechecking for recursive types

    • Patched bug in simply_typed_extended and subtyping where variant contents were not evaluated
    • Add tests for recursive types (map!)
    • Fix bug where coinduction step used wrong equal_ty (should use derived version)

  • Subtyping support

    • Update tests accordingly
    • Used Unique_id to generate fresh variables to join into new recursive types
    • Add tests for subtyping in recursive types

  • Add Error form

  • Add REPL support

Week 8

  • ML-style Polymorphism!

    • Minimal parser and types
    • constraints, unify, and subst based polymorphism
    • Functions added with implicit newly generated type variable
    • rename_tyvars pass to rename variables like 'v12 to 'a
    • let form added, generalizeing over type schemes for performance
    • REPL support (no eval, would be same as previous languages)
    • ref cells with value restriction
    • letrec, fix, and seq forms
    • Tests for all new cases

Week 9

  • System F

    • Parser for universal and existential types / related terms
    • Typechecking for universal and existential types
    • Tests for universal types

Week 10

  • Add global eval function
  • Fix Bonsai dependency, add nix flake

Week 11

  • Add context stack information to chomp
  • Implement f-sub

Week 12

  • Implement f-omega

Week 13

  • Implement f-omega-sub

TODO

  • REPL interface for type inference and evaluation

  • List / Arrays / Exceptions

  • Push Bonsai code

  • meet (as in join/meet)

  • Coercion semantics for runtime evaluation in subtyping?

  • Chapter 18/19 tests with objects

  • Web interface to quickly run examples

  • Mass commenting and documentation backlog

  • FJ: Better error messages in typechecker / evaluator

  • FJ: Less tolerant parser for constructors

  • FJ: Check for dependency cycles in subtyping

  • FJ: Extension exercises (assign fieldref-style, raise/try, interfaces, super, primitives)

  • REC: More examples and tests

  • GM: Add more cases in general

  • GM: Tuples (need TupleProj type?)

  • GM: Row Polymorphism with records

  • GM: Better checks for free vars, aside from syntactic restriction