typecheck-algorithm-notes.txt 900 B

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354
  1. E ::= n
  2. | x
  3. | f(E…)
  4. | let x = E in E
  5. P ::= int | intptr[l]
  6. C ::= P(x) | C & C | ⊤
  7. Σ ::= l…; x… ⊢ C
  8. Γ ::= ε | Γ,f(Σ)→Σ | Γ,y | Γ,x:=α
  9. W ::= ε | E:W | apply[f]:W | let[x,E]:W | drop[x]:W
  10. S ::= ε | α:S
  11. Defn [ <Γ;C;S;W> → <Γ;C;S;W> ]
  12. x:=y in Γ
  13. ------------
  14. <Γ; C; S; x:W> → <Γ; C; y:S; W>
  15. x free in Γ
  16. ------------
  17. <Γ; C; S; n:W> → <Γ,x; C & int(x); x:S; W>
  18. ------------
  19. <Γ; C; S; f(E…):W> → <Γ; C; S; E…:apply[f]:W>
  20. ------------
  21. <Γ; C; S; (let x = E1 in E2):W> → <Γ; C; S; E1:bind[x]:E2:drop[x]:W>
  22. y free in Γ
  23. Γ ⊢ f(x…) → l…; y : C' ⇒ C"
  24. ⊢ C' ⊆ C
  25. ----------------------------------------
  26. <Γ; C; x…:S; apply[f]:W> → <Γ,l…,y; (C & C"); y:S; W>
  27. ----------------------------------------
  28. <Γ; C; y:S; bind[x]:W> → <Γ,x:=y; C; S; W>
  29. f<N>(vec: Vec<A, N+1>)
  30. let x: Vec<A, M+1>
  31. f(x)
  32. N + 1
  33. M + 2
  34. M = 1 + N