Davy's Notes

4-1-2025

2 min read

Typing

  • Type System: Rules that dictate a type to a construct
  • Type: A categorization, a classification or set (ultimately an ontological problem)
  • Examples for PL: int, float, bool, function
  • Construct: A meaningful thing

Type systems give meaning to constructs (ultimately bits) They tell us two things:

  • What type is _
  • What can we do with type _

Type systems can be sound, complete, or decidable, but never all 3

  • Complete and decidable
  • Sound and decidable Sound: All bad programs (ill-defined, unexplainable behavior) will be rejected Complete: All good programs will be accepted Decidable: Able to check all programs

Think about precision and recall in data science!!!! Same concept!!!

The most sound compiler rejects every single program The most complete compiler accepts every single program

To what extent can the type system enforce? Thing can be well-typed (accepted by the type system) but still be ill-defined

  • example: C
char buff[4];
buff[x];
 
// if x >= 4, error

C’s type system only says x has to be an int

Type safe languages enforce, type-unsafe do not Type safe: well-typed well-defined

Type Checking

Type systems are rules Applying the rules: type checking Can do this at compile time: static type checking Can do this at run time: dynamic type checking (Java polymorphism)

A type checker needs a rule of what type an expression is

Like Opsem but instead of ,

Graph View