Hacker News Reader

Comment by TeMPOraL | Hacker News Reader

I have a question that's been on the back of my mind for a while: why just types? Aren't there other things we should be able to tell the compiler so it enforces correctness better? Or a different way to tell those things? What I've seen so far are:

- Type systems of varying complexity, where you sometimes have to abuse the language in complicated ways to express constraints you want;

- Pushing complex checks to runtime, even though they should be - in principle - computable ahead of time. Or, the compiler should be able to tell you ahead of time what you need to do to ensure an assertion never fails.

- External tools like proof checkers.

I guess having types as names of constraints is useful. Then, what I'm looking for is a better "satisfies" from Common Lisp - one that would be guaranteed to run mostly arbitrary code at compile time.

View on HN

That's a great question!

It turns out that sets are a very general concept. Anything you can say about a program can be expressed in terms of sets of states that program goes through as it runs. So there is nothing you can say about a program that cannot be expressed, at least in principle, in terms of sets.

The problem is that sets are themselves Turing-complete. If you can add a member to a set, and remove a member from a set, and test if a set is empty, that is a Turing-complete set of primitives. So if you allow yourself to have a type system that is so powerful as to be Turing-complete you haven't gained anything because now the problem of debugging problems in your type system is equivalent to that of debugging problems in your programming language.

So in order to be useful, a type system has to be constrained in some way that prevents it from being Turing-complete. Choosing those constraints is the art of designing type systems. No matter what you do, it will necessarily be the case that if your type system is going to be useful at all there will be certain things it cannot express. The trick is to insure that those things are things you don't actually care about very much or, alternatively, that your language allows you to "break out" of the constraints of the type system when they become too burdensome and tell the compiler to just do what you tell it despite the fact that it can't prove there won't be errors.

> sets of states that program goes through

I wonder if this is true of a program written in a purely functional language.

This is a really good question!

Basically a lot of properties that you probably can think of that could be checked for but aren't expressible in Java types system can still be expressed using types in another system. Therefore if you want something more powerful than the types your using, use more powerful types! It turns out that we do not really need more to reach the limits of what we can check for automatically.

Lifetimes in rust fits this, they are sort of types.

> Aren't there other things we should be able to tell the compiler so it enforces correctness better?

Well, programming language people tend to call any kind of property you can statically check a 'type'.

There's static asserts.

Yes. I meant the theory people would still look at that through the lens of type systems.

See eg https://en.wikipedia.org/wiki/Dependent_type

If you're interested, there is Calculus of constructions that can express anything.

Reply on news.ycombinator.com