Simply Typed Lambda Calculus Martin Löf Type Theory Homotopy Type Theory Links Category Theory Haskell Algebraic Data Type Type Inference Type Erasure