Comment by chadaustin | Hacker News Reader

Comment by chadaustin | Hacker News Reader

Parent Full thread

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-0...

I tried to do my part here: http://chadaustin.me/2015/07/sum-types/ and http://chadaustin.me/2015/09/haskell-is-not-a-purely-functio...

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

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.

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).

Type Systems, Contract Systems, and IFC are three terms that I think are hard to distinguish using lay language.

Perhaps what you're pointing out is that there are many dynamic and static ways to verify assertions about programs? Certainly.

When programmers talk about "type systems" I think they tend to mean a static, sound, computable approach to verifying assertions about programs.

JIF is a _type system_, albeit not a unification-based one like ML. Moreover, the situations the GP is discussing seem like things that don't need the powerful type system of JIF. Something like ML could handle those situations with ease.

I think contract often takes one of two meanings among non-researchers. Either people are referring to assertions that are dynamically checked or they're referring to very expressive assertions (regardless of when they're checked).

These are all different ways of proving statements about programs.

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.

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

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.

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.

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.

Reply on news.ycombinator.com