#import "@preview/prooftrees:0.1.0": *
#let synth = text(red, sym.arrow.double.r)
#let tyck = text(blue, sym.arrow.double.l)

= Ideas

- Compared to Hindley-Milner type systems, this bidirectional system still serves a lot of similar purposes:
  - Rather than collecting and unifying variables, we have input and output contexts
  - Rather than having special unification rules for polymorphic variables, we use existential variables in the context and solve them using subtyping

= Expressions

- $ id &: forall a. a arrow.r a \
  id &= lambda x . x $

  The typing rules should be:

  - Apply $arrow.r"I"synth$

    #tree(
      axi[$Gamma, hat(alpha), hat(beta), x : hat(alpha) tack.r e tyck hat(beta) tack.l Delta, x : hat(alpha), Theta $],
      uni[$Gamma tack.r lambda x.e synth hat(alpha) arrow.r hat(beta) tack.l Delta$]
    )

    Get $Gamma, hat(alpha), hat(beta), x : hat(alpha) tack.r x tyck hat(beta) tack.l Delta , x : hat(alpha), Theta$

= Open Questions

- Why is subtyping critical to this type system? What would happen without it?
- $Gamma_0 [hat(beta) = hat(alpha)]$ is listed as a type of instantiation but isn't one of the types of contexts defined. How are they allowed to do this?