30 lines
1.2 KiB
Plaintext
30 lines
1.2 KiB
Plaintext
#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? |