trouble-with-types

trouble-with-types

https://www.infoq.com/presentations/data-types-issues/

Author - Martin Odersky

tags :: R:tech

  • Static types are more common in academia?

  • Static

    • More efficient
    • Better ooling
    • Fewer tests needed
    • Better docs, maintenance etc
  • Dynamic

    • Simpler
    • No boilerplate
    • No type-imposed limits on expressiveness

Good software design?

  • Clear

  • Correct

  • Minimal

  • Deterministic

  • Patterns and Constraints

  • Language for good designs

    • Patterns -> abstractions
    • Constraints -> types?
  • Type systems are finicky, which is why there are so many different ones

  • Haskell is strong & static typed!

  • Static type: weak/strong vs coarse/detailed

    • C is weak and coarse

    • Go is strong, but coarse; simple types but strongly enforced

      • no generic types
      • Simple types cannot be extended by users; use abstractions that are given to you
      • normative; there is only to do things
    • R:haskell - type it to the max

      • rich & turing complete language to write types - these help model expressive systems that are as good as dynamically typed code
      • “nothing” type; allows tyoe correctness in WIP code
      • type combination forms
    • Typescript etc - cutting corners; detailed but weakly enforced

      • “post-modern languages”
      • appeals to users’ intuitions; covariant generics like “employees are persons, so employee->employer fn is also a person->employer fn”
      • embrace unsoundness; can make functions a bit more confusing
      • hacky?

Goal of types: Precision, Soundness, Simplicity

  • Most typed languages can only achieve 2 out of 3

Abstractions

  • Two forms:

    • Parameters (positional, functional)
    • Abtract members (modular, name based)
  • “orthogonal design” where you can mix and match the two

    • This is particular to Scala
    • results in a ton of combinations, which gives you a lot freedom arond structuring code; can be confusing
  • “non-orthogonal design” - has type and a module system

  • Use “projections” to reduce dimensionality in orthogonal design

    • project certain language features into others

DOT - Calculus for Dependent Object Types

  • Dotty - a scala-like language with DOT at its core