From 794eb5949aef517aa067ec990e874e5806e77db2 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 19 Nov 2024 11:41:38 +0100 Subject: [PATCH] [lec5] type-checking.md update --- notes/divide-annotated.c | 11 ++++++++ notes/divide-untyped.c | 10 +++++++ notes/divide.c | 11 ++++++++ notes/prime-stms.c | 58 ++++++++++++++++++++++++++++++++++++++++ notes/type-checking.md | 36 ++++++++++++++++++++----- 5 files changed, 120 insertions(+), 6 deletions(-) create mode 100644 notes/divide-annotated.c create mode 100644 notes/divide-untyped.c create mode 100644 notes/divide.c create mode 100644 notes/prime-stms.c diff --git a/notes/divide-annotated.c b/notes/divide-annotated.c new file mode 100644 index 0000000..7ffbce3 --- /dev/null +++ b/notes/divide-annotated.c @@ -0,0 +1,11 @@ +int idivii (int x, int y) { return (x int./ y); } +double ddivii (int x, int y) { return (double)(x int./ y); } +double ddivid (double x, int y) { return (x double./ (double)y); } +double ddivdd (double x, double y) { return (x double./ y); } + +int main() { + printDouble((double)idivii(5,3)); // 1.0 + printDouble(ddivii(5,3)); // 1.0 + printDouble(ddivdi((double)5,3)); // 1.6666666666666667 + printDouble(ddivdd((double)5,(double)3)); // 1.6666666666666667 +} diff --git a/notes/divide-untyped.c b/notes/divide-untyped.c new file mode 100644 index 0000000..e8d7f5c --- /dev/null +++ b/notes/divide-untyped.c @@ -0,0 +1,10 @@ +div(x,y) { return (x / y); } + +main() { + printDouble(div(5,3)); +} + +// What does this print? +// 1 1 +// X 1.6666666666666667 +// 2 2 diff --git a/notes/divide.c b/notes/divide.c new file mode 100644 index 0000000..e2d88f3 --- /dev/null +++ b/notes/divide.c @@ -0,0 +1,11 @@ +int idivii (int x, int y) { return (x / y); } +double ddivii (int x, int y) { return (x / y); } +double ddivid (double x, int y) { return (x / y); } +double ddivdd (double x, double y) { return (x / y); } + +int main() { + printDouble(idivii(5,3)); // + printDouble(ddivii(5,3)); // + printDouble(ddivdi(5,3)); // + printDouble(ddivdd(5,3)); // +} diff --git a/notes/prime-stms.c b/notes/prime-stms.c new file mode 100644 index 0000000..ba14f06 --- /dev/null +++ b/notes/prime-stms.c @@ -0,0 +1,58 @@ +// TYPE(VARS): expression of type TYPE over variables VARS +bool divides (int q, int p) { + return BOOL(p,q); +} + +// +bool prime (int p) { + if (BOOL(p)) return BOOL(p); + else { + int q = INT(p,q); + while (BOOL(p,q)) + if (BOOL(p,q)) return BOOL(p,q); + else ANY(p,q); + } + return BOOL(p); +} + +int main () { + if (BOOL()) ANY(); else ANY(); +} + +/* +BOOL(p,q): (p / q) * q == p + + + +BOOL(p): p == 1 || divides(2,p) +BOOL(p): true + +INT(p,q): 3 +BOOL(p,q): q * q <= p +BOOL(p,q): divides(q,p) +BOOL(p,q): false +ANY(p,q): q = q + 2 +BOOL(p): false + + +BOOL(): prime(641) +ANY(): printInt(641) +ANY(): printInt(0) +*/ + + + +/* +BOOL(): prime(641) +BOOL(p): p == 1 || divides(2,p) + true + false +BOOL(p,q): (p / q) * q == p + q * q <= p + divides(q,p) + false +INT(p,q): 3 +ANY(): printInt(641) + printInt(0) +ANY(p,q): q = q + 2 +*/ diff --git a/notes/type-checking.md b/notes/type-checking.md index 461a8e6..e1ab301 100644 --- a/notes/type-checking.md +++ b/notes/type-checking.md @@ -18,8 +18,9 @@ Introduction ```c typedef int (*fun_t)(); // Pointer to function without arguments returning int + int f() {...} int main () { - fun_t good = &main; // Function pointer to main function + fun_t good = &f; // Function pointer to function f int i = (*good)(); fun_t bad = 12345678; // Function pointer to random address int j = (*bad)(); @@ -40,14 +41,37 @@ Introduction - Programming language perspective: * Facilitate overloading (like `/` for different division algorithms) + * (Non ad-hoc) polymorphism: + - Parametric polymorphism (Haskell `forall`, Java generics) + - Subtyping + +- Correctness perspective: + * Types partially describe behavior (properties, invariants) + * Dependent types: Rich property language + * Machine-checked documentation / communication of program behavior + +### Type-checking, informally + +- Goal: type-check programs like [prime.c](prime.c) +- Perspective: expressions in their own layer: [prime-stms.c](prime-stms.c) ### Where types make a difference +Code: [divide-untyped.c](divide-untyped.c) ```c ... divide(... x, ... y) { return x / y; } printDouble (divide (5, 3)); ``` +Quiz: In an untyped language, what is printed? [menti.com code 413881](https://www.menti.com/alw5a4m2kgzb) + +- 1: 1.0 +- X: 1.6666666666666667 +- 2: 2.0 + +Some possible typings: [divide.c](divide.c) + +Elaborations: [divide-annotated.c](divide-annotated.c) Judgements and rules -------------------- @@ -212,7 +236,7 @@ In practice, it often does. E.g. with coercions to `string`: int ≤ string 1 → "1" int ≤ double ≤ string 1 → 1.0 → "1.0" -Quiz: What is the value of this expression? (menti.com code 83910313) +Quiz: What is the value of this expression? [menti.com code 413881](https://www.menti.com/alw5a4m2kgzb) 1 + 2 + "hello" + 1 + 2 @@ -248,7 +272,7 @@ Example implementation: (e₂', t₂) ← infer (e₂) t ← max t₁ t₂ e₁'' ← coerce (e₁', t₁, t) - e2'' ← coerce (e₂', t₂, t) + e₂'' ← coerce (e₂', t₂, t) return (ETArith t e₁'' ADiv e₂'', t) @@ -279,7 +303,7 @@ Example implementation: (e₂', t₂) ← infer (e₂) t ← max t₁ t₂ e₁'' ← coerce (e₁', t₁, t) - e2'' ← coerce (e₂', t₂, t) + e₂'' ← coerce (e₂', t₂, t) if t /= TInt && t /= TDouble then fail "illegal arithmetic comparison" else return (ETCmp t e₁'' CEq e₂'', TBool) @@ -289,7 +313,7 @@ Example implementation: (e₂', t₂) ← infer (e₂) t ← max t₁ t₂ e₁'' ← coerce (e₁', t₁, t) - e2'' ← coerce (e₂', t₂, t) + e₂'' ← coerce (e₂', t₂, t) return (ETCmp t e₁'' CEq e₂'', TBool) Statements @@ -478,7 +502,7 @@ Branches need to be in new scope. Γ ⊢ᵗ⁰ if (e) s₁ else s₂ ⇒ Γ Γ ⊢ᵗ⁰ e : bool Γ. ⊢ᵗ⁰ s ⇒ Γ' - ----------------------------- + ------------------------------ Γ ⊢ᵗ⁰ while (e) s ⇒ Γ Example: