Mega-explainer: types, affine types, session types

[cognivore]

Why?

• I need to give a talk on these subjects
• To do that, I need to structure my knowledge and put it into simple yet technical post
• I need to survey business applicability of these things

How?

• [x] Motivate type systems in general
• [x] Show how Java ecosystem took stuff from good languages and good language designers
  • [x] Generics
  • [x] HKT (no support)
  • [x] Show how Scala brings a lot more concepts into Java for Functor, Monad to be easily implementable
• [x] Story of the fairies there eas a mummy nd she gave ay many cinamon roppyyls and bby was ga
• [ ] How Rust got its ownership / borrowing semantics
• [ ] Examples of affine types / linear types https://en.wikipedia.org/wiki/Substructural_type_system#Programming_languages
• [ ] Linear types allow for a particular type of implementation of session types

Old checklist:

• ~Motivate sound type systems~
• ~Explain typed lambda calculus~
• ~Explain linear logic~
• ~Explain turning linear logic into typed lambda calculus~
• ~Explore affine types in Rust ownership~
• ~Motivate session types~
• ~Explain how linear types are used in the motivation for session types~
• ~Explain pi-calculus~
• ~Explain typing pi-calculus~
• ~Talk about my one of my favorite papers~

[cognivore]

Based on the feedback from the colleagues and my pondering, I think I should focus on engineering of typing and extending protocols.

[cognivore]

I've worked on a lot of options, including writing my own tiny type system simulators, but I figured that for business-inclined crowd, the most helpful and understandable thing would be to make argument for the fact that us foreseeing more bleeding edge type system inclusions into existing ecosystems by following HKT and generics relationship with Java.

[cognivore]

http://www.jot.fm/issues/issue_2007_09/article3.pdf heroic efforts to formalise Java's semantics

[cognivore]

Something to add to the investment into PLT part:

• Suggest companies to build "bridges" between their stacks and research languages that are doing stuff they need to increase assurance, including devops engineering.