6 ms·

Wow, apropos! I was just thinking about this in the shower. For most of my life, I equated types with sets of values, but after learning Haskell and working w

Wow, apropos! I was just thinking about this in the shower. For most of my life, I equated types with sets of values, but after learning Haskell and working with higher-kinded types, type classes, and existential types, I realized I don't know anymore what a type _is_. I know that type systems provide proof that certain classes of operations are impossible (like comparing a number to a string, or dereferencing an invalid reference). It's pretty mindbending to use existentials or GADTs and pull two values of a record and not know anything about those values except that, for example, they can be compared for equality. data HasTwoEq = forall a. Eq a => HasTwoEq a a equalOrNot :: HasTwoEq -> Bool equalOrNot (HasTwoEq x y) = x == y The example is contrived, but it illustrates the point that the types of x and y are not known, _except_ that they can be compared. That's not the kind of thing you can express with, say, Java or Go interfaces, but it makes perfect sense once you start to break down the mental walls you've built in your head over the years. I'm thrilled to see a growing body of accessible* PL and type theory literature, because these things are important to helping us develop software at increasingly large scales, and it's clear that very few people -- including myself! -- know enough about this topic. * e.g. https://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/ https://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-0... I tried to do my part here: http://chadaustin.me/2015/07/sum-types/ http://chadaustin.me/2015/07/sum-types/ and http://chadaustin.me/2015/09/haskell-is-not-a-purely-functional-language/ http://chadaustin.me/2015/09/haskell-is-not-a-purely-functio...

woah 11y ago
Do these things actually help us develop software at increasingly large scales?
- chadaustin 11y ago
  Absolutely. As a codebase grows and a larger and larger number of users depend on it, you want to be able to statically verify things like "I never compare an experiment ID to a customer ID" or "timeouts are always precisely specified with their units" or "I never issue a MySQL query from a retriable Redis transaction" or "this unit test is 100% deterministic" or "all code handles the case that this optional field is missing", just to pick a few specific examples that I've run into.
  - vezzy-fnord 11y ago
    Those sound like jobs amenable to design by contract and information flow control, not necessarily type systems and type theory, per se (though there is some overlap).
    - implicit 11y ago
      How is "information flow control" different from a type system? I've always considered the primary purpose of type systems to be restricting how data can flow through a program.
      - vezzy-fnord 11y ago
        IFC is orthogonal to type systems, having also been modeled in terms of axiomatic semantics (Hoare logic) independent of a type system. It can also be practically implemented through runtime monitoring, partial evaluation and various hybrid approaches. Type systems are certainly one way of providing foundations for IFC, but few languages have it as a first-class construct. Notable exceptions are SPARK (based on Ada) and Jif (based on Java). See also "A Perspective on Information-Flow Control": http://www.cse.chalmers.se/~andrei/mod11.pdf http://www.cse.chalmers.se/~andrei/mod11.pdf
        elcritch 11y ago
        Interesting, I'll definitely have to check this out. Any input on whether this has been applied and/or could be applied to actor paradigms of computation? It seems like modeling data flow via messages would be pretty natural semantics for something like this. But first I need to dig into what Hoare logic is and how it applies.
    - bassislife 11y ago
      Well, the purpose of types is to enable design by contract among other things. Therefore, I am also a bit dubious about IFC. It seems to me that Data Flow Analysis is more suitable. We are essentially hinting at the same thing I guess, but I expect some type system tie-ins. Otherwise it might become too abstract.
- lmm 11y ago
  Yes! In fact I'd go so far as to say they're what make it possible. Without them you end up needing to split a large codebase into microservices, with all the disadvantages that entails, because that's the only way to get good isolation in a language without a good type system.

woah 11y ago

Do these things actually help us develop software at increasingly large scales?

chadaustin 11y ago
Absolutely. As a codebase grows and a larger and larger number of users depend on it, you want to be able to statically verify things like "I never compare an experiment ID to a customer ID" or "timeouts are always precisely specified with their units" or "I never issue a MySQL query from a retriable Redis transaction" or "this unit test is 100% deterministic" or "all code handles the case that this optional field is missing", just to pick a few specific examples that I've run into.
- vezzy-fnord 11y ago
  Those sound like jobs amenable to design by contract and information flow control, not necessarily type systems and type theory, per se (though there is some overlap).
  - implicit 11y ago
    How is "information flow control" different from a type system? I've always considered the primary purpose of type systems to be restricting how data can flow through a program.
    - vezzy-fnord 11y ago
      IFC is orthogonal to type systems, having also been modeled in terms of axiomatic semantics (Hoare logic) independent of a type system. It can also be practically implemented through runtime monitoring, partial evaluation and various hybrid approaches. Type systems are certainly one way of providing foundations for IFC, but few languages have it as a first-class construct. Notable exceptions are SPARK (based on Ada) and Jif (based on Java). See also "A Perspective on Information-Flow Control": http://www.cse.chalmers.se/~andrei/mod11.pdf http://www.cse.chalmers.se/~andrei/mod11.pdf
      - elcritch 11y ago
        Interesting, I'll definitely have to check this out. Any input on whether this has been applied and/or could be applied to actor paradigms of computation? It seems like modeling data flow via messages would be pretty natural semantics for something like this. But first I need to dig into what Hoare logic is and how it applies.
  - bassislife 11y ago
    Well, the purpose of types is to enable design by contract among other things. Therefore, I am also a bit dubious about IFC. It seems to me that Data Flow Analysis is more suitable. We are essentially hinting at the same thing I guess, but I expect some type system tie-ins. Otherwise it might become too abstract.
lmm 11y ago
Yes! In fact I'd go so far as to say they're what make it possible. Without them you end up needing to split a large codebase into microservices, with all the disadvantages that entails, because that's the only way to get good isolation in a language without a good type system.