5 ms·

> Fascination with type systems does not seem to be all that useful in practice. And yet type theory is an excellent way to express all kinds of invariants. Th

> Fascination with type systems does not seem to be all that useful in practice. And yet type theory is an excellent way to express all kinds of invariants. The more rich the type system the more you can express. If you get to dependent types you essentially have all of mathematics at your disposal. This is the basis of some of the most advance proof automation available. What is super cool is that proofs are programs. You can write your programs and use the same language to prove theorems about them. This is still fairly advanced stuff for most programming activities but the languages have been steadily getting better and the automation faster and I think the worlds will eventually collide in some area of industrial programming. We're already seeing it happen in security, privacy, and networking. I don't think type systems suffer from complexity. They merely reveal the inherent complexity. You can use languages that hide it from you but you pay a price: errors only become obvious at run time when the program fails. For small programs that's easy enough to tolerate but for large ones? Ones where certain properties cannot fail? Not so much in my experience. update: clarified wording of "proofs are programs"

spc476 5y ago
> You can write your programs and use the same language to prove theorems about them. Didn't Kurt Gödel and Alan Turing do some work on proving statements within a system?
- BalinKing 5y ago
  AFAIK languages like Idris, Agda, and Coq are not Turing-complete (specifically, they disallow general recursion) for just this reason.
  - raphlinus 5y ago
    If my understanding is correct, Agda and Coq disallow general recursion, so all programs terminate by construction, but Idris relaxes this, in a desire to be more pragmatic at the cost of not as clean mathematically (functions have to be modeled as partial in general, to account for the fact they might not terminate).
  - earleybird 5y ago
    General recursion, yes however often the fixed point operator is added (and its associated judgements) to have interesting programs/proofs. Hmm, that fixed point operator, rings a bell, can't quite put my finger on it . . . :-)
dmitriid 5y ago
> The more rich the type system the more you can express. If you get to Ah yes. And then you end up writing entire prgrams in types. So the next logical setep would be to start unit- and integration tests for these types, and then invent types for those types to more easily check them... > you essentially have all of mathematics at your disposal. Most of the stuff we do has nothing to do with mathematics.
- sidlls 5y ago
  One of the major selling points of a robust (not "strong", necessarily, but at least...not weak?) type system is that an entire class of unit tests are no longer necessary (e.g., those that validate/exercise handling of cases where data of an invalid type are passed as a parameter to the function). Integration tests are necessary independently of the implementation language--they don't test the correctness of units of code, but of communication between APIs.
  - dmitriid 5y ago
    > that an entire class of unit tests are no longer necessary That's not what I wrote about. I've seen people implement entire DSLs in types. So now you have to test that.
YorkshireSeason 5y ago
> The more rich the type system the more you can express Why is this interesting? You pay an extremely heavy price in terms of language complexity. In practise, you almost never have the invarants at all or correct when you begin programming, and your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one. Moreover proofs are non-compositional: you make a tiny change somewhere and you might have to change all proofs. In addition we don't have full dependent types for any advanced programming language features, we have them only for pure functions that terminate. > the same language to prove theorems about them That sounds like a disadvantage. Ultimately verification is about comparing two 'implementations' against each other (in a very general sense of implementations where logical specs and tests also count as implementations). And the more similar the two implementations, the more likely you are to make the same mistake in both. After all, your specification is just as likely to be buggy as your implementation code. > type systems suffer from complexity. This is clearly false for just about any reasonable notion of complexity. For a start pretty much as soon as you go beyond let-polymorphism in terms of typing system expressivity, you looks type-inference. Even type-checking can easily become undecidable when the ambient typing system is too expressive. There is no free lunch.
- agentultra 5y ago
  > Why is this interesting? You pay an extremely heavy price in terms of language complexity. As you say, there is no free lunch. Not having a useful type system introduces its own complexity. It depends on what abstractions you find most useful. The present limitations of dependently typed languages will not be limitations tomorrow. Evolution in the field of proof engineering is providing new frameworks for making proofs more compositional and being able to extract programs from the proofs. It's not amazing and super useful today but it's a lot better than it was even five years ago and I suspect will continue to improve. > After all, your specification is just as likely to be buggy as your implementation code If you can't think of the right theorems or specifications I doubt you will write a correct program. One is a lot easier to reason about than the other. > Even type-checking can easily become undecidable when the ambient typing system is too expressive. I'm not sure I follow. I understand how type inference can become undecidable but how does a sound type theory end up this way? The judgement and inference rules for CoC are rather small [0]. > There is no free lunch. I don't disagree. I still enjoy programming in C. And I might even choose it for a project. And if it so happened that I had certain requirements like the system had to be real-time and could not deadlock then... I might be making a trade off to write my proofs and specifications in another language than my implementation. We're not at a place yet where we can extract a full program from a specification and not in a place where we can write dependently-typed programs with deterministic run times either. I would like to have my cake and eat it too but that's where we are. [0] https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions
quickthrower2 5y ago
This advanced types stuff sounds really useful but it needs to be made very easy to use for the mainstream Java of C# programmer to use. A success story in this regard is the async keyword. Very quickly you can get used to it and it feels like any other imperative programming. In C# if I can add assertions and have C# compile time check the source that the assertion will not be violated. This would be great. I know they do this for null checking.
sigmaml 5y ago
Highly expressive type systems can lead people to as much design hell as does deep OOP. I have seen and experienced this in at least a couple of projects. The only difference is: instead of brittle hierarchies, we get ossified compositions (depending on how much nominal vs structural typing happens). We, of course, agree that we are quite some distance from having advanced type systems brought to day-to-day industrial programming.

spc476 5y ago

> You can write your programs and use the same language to prove theorems about them. Didn't Kurt Gödel and Alan Turing do some work on proving statements within a system?

BalinKing 5y ago
AFAIK languages like Idris, Agda, and Coq are not Turing-complete (specifically, they disallow general recursion) for just this reason.
- raphlinus 5y ago
  If my understanding is correct, Agda and Coq disallow general recursion, so all programs terminate by construction, but Idris relaxes this, in a desire to be more pragmatic at the cost of not as clean mathematically (functions have to be modeled as partial in general, to account for the fact they might not terminate).
- earleybird 5y ago
  General recursion, yes however often the fixed point operator is added (and its associated judgements) to have interesting programs/proofs. Hmm, that fixed point operator, rings a bell, can't quite put my finger on it . . . :-)

dmitriid 5y ago

> The more rich the type system the more you can express. If you get to Ah yes. And then you end up writing entire prgrams in types. So the next logical setep would be to start unit- and integration tests for these types, and then invent types for those types to more easily check them... > you essentially have all of mathematics at your disposal. Most of the stuff we do has nothing to do with mathematics.

sidlls 5y ago
One of the major selling points of a robust (not "strong", necessarily, but at least...not weak?) type system is that an entire class of unit tests are no longer necessary (e.g., those that validate/exercise handling of cases where data of an invalid type are passed as a parameter to the function). Integration tests are necessary independently of the implementation language--they don't test the correctness of units of code, but of communication between APIs.
- dmitriid 5y ago
  > that an entire class of unit tests are no longer necessary That's not what I wrote about. I've seen people implement entire DSLs in types. So now you have to test that.

YorkshireSeason 5y ago

> The more rich the type system the more you can express Why is this interesting? You pay an extremely heavy price in terms of language complexity. In practise, you almost never have the invarants at all or correct when you begin programming, and your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one. Moreover proofs are non-compositional: you make a tiny change somewhere and you might have to change all proofs. In addition we don't have full dependent types for any advanced programming language features, we have them only for pure functions that terminate. > the same language to prove theorems about them That sounds like a disadvantage. Ultimately verification is about comparing two 'implementations' against each other (in a very general sense of implementations where logical specs and tests also count as implementations). And the more similar the two implementations, the more likely you are to make the same mistake in both. After all, your specification is just as likely to be buggy as your implementation code. > type systems suffer from complexity. This is clearly false for just about any reasonable notion of complexity. For a start pretty much as soon as you go beyond let-polymorphism in terms of typing system expressivity, you looks type-inference. Even type-checking can easily become undecidable when the ambient typing system is too expressive. There is no free lunch.

agentultra 5y ago
> Why is this interesting? You pay an extremely heavy price in terms of language complexity. As you say, there is no free lunch. Not having a useful type system introduces its own complexity. It depends on what abstractions you find most useful. The present limitations of dependently typed languages will not be limitations tomorrow. Evolution in the field of proof engineering is providing new frameworks for making proofs more compositional and being able to extract programs from the proofs. It's not amazing and super useful today but it's a lot better than it was even five years ago and I suspect will continue to improve. > After all, your specification is just as likely to be buggy as your implementation code If you can't think of the right theorems or specifications I doubt you will write a correct program. One is a lot easier to reason about than the other. > Even type-checking can easily become undecidable when the ambient typing system is too expressive. I'm not sure I follow. I understand how type inference can become undecidable but how does a sound type theory end up this way? The judgement and inference rules for CoC are rather small [0]. > There is no free lunch. I don't disagree. I still enjoy programming in C. And I might even choose it for a project. And if it so happened that I had certain requirements like the system had to be real-time and could not deadlock then... I might be making a trade off to write my proofs and specifications in another language than my implementation. We're not at a place yet where we can extract a full program from a specification and not in a place where we can write dependently-typed programs with deterministic run times either. I would like to have my cake and eat it too but that's where we are. [0] https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions

quickthrower2 5y ago

This advanced types stuff sounds really useful but it needs to be made very easy to use for the mainstream Java of C# programmer to use. A success story in this regard is the async keyword. Very quickly you can get used to it and it feels like any other imperative programming. In C# if I can add assertions and have C# compile time check the source that the assertion will not be violated. This would be great. I know they do this for null checking.

sigmaml 5y ago

Highly expressive type systems can lead people to as much design hell as does deep OOP. I have seen and experienced this in at least a couple of projects. The only difference is: instead of brittle hierarchies, we get ossified compositions (depending on how much nominal vs structural typing happens). We, of course, agree that we are quite some distance from having advanced type systems brought to day-to-day industrial programming.