Improving Correctness with Types

Iain Hull

http://gotocon.com/berlin-2015/presentation/Improving%20Correctness%20with%20Types

Slides: http://de.slideshare.net/IainHull/improving-correctness-with-type-goto-con-berlin

Video: https://www.youtube.com/watch?v=uxofKKIAY3Q

iain.hull@workday.com workday.github.com

 

  • Defensive Programming: not so nice for finding errors
  • Fail Fast:
    • Find bugs quickly
    • Requires lots of tests
    • what happens when tests miss?
    • errormessages not 
  • Design by contract
    • invariants, pre- and post-conditions
    • nobody seems to be interested
    • toolsupport bad
  • Function: Abbildung von domain -> Range
    • total function: complete domain, complete range
    • shrink domain and range to get total functions
      • never use nulls (Hoare: billion dollar mistake)
      • (almost) All data is immutable
        • great for correctness
      • do not throw exceptions
        • use error types instead
      • Use Wrapper types (to shrink domain and range)
        • example:
          • AnyVal => keyword: Value Type
          • private constructor
          • from method in companion object
          • use ===  => type checked equals!
          • define operators on Types
          • => move validation to correct place
          • => define semantic properties
        • non-empty list
          • org.scalactic
            • Every (non-empty list)
          • method call with vargars with first parameter fixed
          • maybeNonEmpty
      • Algebraic data types
        • sealed traits
        • tag type
          • import tag.@@
          • trait Foo
          • function takes value tagged as @@ Foo
        • functional dependencies between types
          • use traits
        • expose shape of your data
        • use shape to control possible states
      • Path-Dependent types
        • tied to the instance
        • good for encryption, multi-tendancy
      • Amanda Launcher
        • Tests vs Types
      • "The purpose of abstraction is not to be vague, but to create new semantic level in which one can be absolutely precise" Dijkstra