/*
    The most important theorem of Typed Lambda Calculus is the following,

  THEOREM: if a term A has type T and A beta-reduces to B, then B also have T.

  The theorem can be referred to the type soundness theorem.  Evaluation
  (beta-reduction) should not change the type of terms.  This means that
  we can do type checking before, during or after beta-reduction.  Checking
  types after reduction is a bit late.  Checking it before can be called
  "static typing": that is type check all terms before any reduction takes
  place.  We can also type checking during reduction, in which case it should
  be called "dynamic typing."  Static typing is usually done at compile time.
  It is both the safest option, because it detects errors before they can 
  cause any damage, as well as the fastest option because it carries no
  runtime overhead. 

  Languages like Python are dynamically typed.  You can declare:

  def f(x):
    if x>0: return 1
    else return "abc"
 
  print(f(0) / 4) # error here, but not a statically (compile-time) 

  The error in the expression f(0)/4 is not detected until the program
  runs.  

  There are many languages that behave similarly to Python in this regard,
  the oldest one being List and Scheme.  The most direct, modern descendant 
  of Scheme is Clojure, which is also dynamically typed.  But Scheme also
  influenced the development of Perl, Ruby, Python, Javascript, R and 
  a host of simlar languages.  They're easy to learn and use, but are slow
  and the lack of static type safety is a major disadvantage.  One important
  trend in the direction of programming languages is to add more static
  typing features to these languages.  Typescript imposes type inference
  and type checking on Javascript.  Crystal does the same for Ruby.  Python
  is also adding more support for static type checking.  There is also a 
  modlue (mypy) that can statically type check programs and REJECT the f
  function above before it's called.

  Other languages support different degrees of static typing, but sometimes
  it's not perfect ...
*/

// is C statically typed?

#include<stdint.h>
#include<stdio.h>

int f(int x) {
  if (x>0) return 1;
  else return (int)(int64_t)"abc";
}

int main() {
  printf("f(\"abc\") - 1 is %ld\n", f(0));
}
// worst case scenario - not even a runtime error message, get 
// unpredictable behavior, junk.

/*
    What are the advantages of static typing?

    1. safety
    2. no runtime overhead

    C's type system allows arbitrary casting from integers to pointers,
    thus compromising 1 (but not 2.)  But 1. is certainly more important.
*/