Introduction to Programming Languages/Type Checking

Static Type Checking In static typing, types are checked before program execution (at compile time). Every variable, function, and expression has a type determined beforehand Type errors are detected before running the program SML Example: fun sum (a:int, b:int) = a + b; val x = sum(1, 2); (* OK *) val y = sum(1, "abc"); (* COMPILE-TIME ERROR *)SML automatically infers types and prevents invalid operations. Java Example: int sum(int a, int b) { return a + b; } int x = sum(1, 2); // OK int y = sum(1, "abc"); // COMPILE-TIME ERRORThe compiler blocks incorrect type usage. Python Example: Python does not enforce static typing, but supports type hints:def sum(a: int, b: int) -> int: return a + b sum(1, 2) # OK sum(1, "abc") # RUNTIME ERROR (or caught by tools like mypy) Prolog Example: sum(A, B, R) :- R is A + B.Query: ?- sum(1, "abc", R).Error occurs at runtime, not before execution. Dynamic Typing Type checking happens during program execution. Programs run even if type issues exist Errors appear only when problematic code is executed Python Example: def sum(a, b): return a + b sum(1, 2) # OK sum(1, "abc") # RUNTIME ERROR Prolog Example: sum(A, B, R) :- R is A + B.Type correctness is enforced when the rule is executed. SML / Java Not dynamically typed by default But may perform runtime checks (e.g., casting) Static vs Dynamic Statically typed languages also use runtime checks: Especially with subtypes and object-oriented features.Object obj = "hello"; if (obj instanceof String) { String s = (String) obj; }Type is checked at runtime Dynamically typed languages also use static information: For optimization and partial inference Python Example: def sum(a: int, b: int) -> int: return a + bTools like mypy can perform static analysis Runtime Type Information Even dynamically typed languages must: store type information alongside values check operations at runtime Conceptually:value = 10 → [value + type=int] value = "abc" → [value + type=string] Explicit Runtime Type Tests Some languages allow explicit type checking: Java if (obj instanceof String) { // treat as String } Python if isinstance(x, int): print("it is an integer") Strong vs Weak Typing Strong Typing Prevents invalid operations on types Safer and more predictable Examples: SML Java Weak Typing Allows implicit or unsafe conversions More flexible but riskier Example (C-like behavior):int x = "abc"; // may compile in unsafe contexts