david's pl notes

2024-08-20 • Prelim review - STLC and friends

Sep 02, 20245 min read

Definitions

  • Substitution in term:
  • Beta = eval, alpha = rename arg
  • Call-by-name, i.e., lazy: no reductions inside abstractions.
  • Call-by-value, i.e., strict: outermost application reduced, application only occurs if right-hand side is value (var or lambda, not another application).
  • Y combinator: fix = λf. (λx. f (x x)) (λx. f (x x))
  • de Brujin indices: becomes .
  • Non-value normal forms are stuck. Run-time error.
    • A well-typed term is normalizing iff it’s guaranteed to halt in finite steps.

See 2024-06-17 • lambda calc.

Simply-typed lambda calculus

  • Type safety = progress (well-typed term not stuck) + preservation (after eval, still well-typed)
    • Well-typed term can make eval progress, well-typedness is preserved in eval
  • Curry-Howard: types are propositions, programs are proofs.
t = x | λx:T. t | t1 t2
v = λx:T. t
T = T -> T | (* base types *)
C = null | C, x:T (* context *)

Eval: evaluate either side of application, then do substitution

Typing: variable type, lambda introduction and elimination

Big step eval 

\begin{prooftree} \AXC{$t_{1} \Downarrow true$} \AXC{$t_{2} \Downarrow v_{2}$} \BIC{$\verb|if t1 then t2 else t3| \Downarrow v_{3}$} \end{prooftree}
Link to original

See 2024-06-17 • lambda calc.

Extensions

Simple ones

  • Derived forms & elaboration: iff , iff .
  • Type ascription (x as T): evaluation removes ascription, introduction rule gives expr type T.
  • Let binding: evals as substitution. Can be defined as sugar on typing derivation (transform into application of function), since we need extra info about type of let-bound var
  • Tuples: records w/ projection. Eval rules for projection and if subpart of record evals. Typing for introduction and delimination.
  • Variants: tag <l = t> as T and pattern match. Intro and elim (pattern match)
  • Recursion:
    • Diverges!

References

  • Introduction with ref val, elimination with dereferencing !val
  • Internally, we have a new location value , used for type-checking and eval.
  • Evaluation is with respect to a store
    • Substitution for stores:

  • Typing with respect to and .

- Do this for performance (don't need to typecheck reference every time) and to enable cyclic refs.

Exceptions

  • Multiple ways of modeling:
    • Panic: ,
    • try-catch: standard
    • exceptions with values: instead of .

See 2024-06-26 • type system extensions.

Java-type beat

Subtyping

  • Subsumption:
  • Records: width (records with more fields), depth (subtype between same field), permutation (order doesn’t matter)
  • Functions: contravariant (reversed) on first arg, covariant on second
    • must be usable at least wherever is.
  • Ascription: upcast to supertype, downcast to subtype (assume during typechecking, evaluation only works if the type matches the downcast)
  • References: invariant (both contra- and covariant on argument). Need covariance on read, contravariance on write.
  • Coercion: maybe even if they have different reprs, values. We can define a function that transforms typing derivations into terms with runtime coercions.
    • Make sure we have coherence: different coercion paths yield same behavior
  • Intersection, union types

See 2024-06-26 • type system extensions.

Imperative objects in STLC

  • What the fuck is OOP
    • Multiple representations: An abstract data type (ADT) has an interface. Different classes can implement that interface, even if they have different internals.
    • Encapsulation: hide object’s internals, only expose public operations.
    • Open recursion via self and inheritance.
  • We store instance variables with a representation type: a record with instance variables. Each instance variable maps to a reference containing that var’s state.
  • A class is represented as a function that takes the instance variables, returning a record of functions that act on those vars.
    • A class instance is that class function applied to a representation type.
    • We can call superclass methods by let-binding to a superclass instance in the subclass
  • Constructors create a new repr type and class and return the package.
  • We can get self by adding an argument self to our class functions.
    • self must have type Unit -> Class, to avoid diverging.
    • We create an initially empty reference cAux : Ref (Unit -> Class) to the current class instance, binding cAux := (whateverClass vars cAux) in the constructor for the class.

See 2024-07-03 • denotational semantics and fancy types.

Graph View

Backlinks