Comment by cle | Hacker News Reader

Comment by cle | Hacker News Reader

Parent Full thread

I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are. They’re about ergonomically reducing the space of valid programs.

There are a lot of interesting tradeoffs to be made there. Over strict specification (whether parsing or type checking), specifically checking for invariants that aren’t actually useful, can make code and systems brittle and hard to change, just like under specifying them. The specifications can also be different depending on what you’re doing with the data.

Also as the expressiveness of types increases, the space of possible ways to constrain your program space goes up, along with the complexity of the transformations of that space, making it difficult to understand what the valid program space actually is, hard to understand when you’ve accidentally excluded perfectly valid programs, etc.

So yes, fundamentally there are always types and underlying structure to useful data, but saying that it has “a” type is dramatically over-simplifying things.

>I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct

This is not true. Consider the map function of a typical functional language with parametric polymorphism:

map : (a -> b) -> [a] -> [b]

That signature is complete, it covers everything there is to know about the function. And, except for trivial implementations, there is no way to implement it wrongly.

In some cases, one can even rule out trivial implementations and infer the correct implementations from the type signature alone.

In any case, there is no "semantically wrong" input to such a function. It is just a function and totally agnostic regarding your use case.

Of course that type doesn't encode everything there is to know about that function, even assuming purity.

Here are some functions that match that type signature:

    map1 foo x:xs = [foo x]

    mapR foo x:xs = append (mapR foo xs) foo x

    mapI foo x:xs = foo x : mapI foo x:xs

Of course, we can create many more functions that arrange the values in other creative ways, that add more or fewer values etc. If the function isn't pure, we can also imagine many more dimensions of functions that do arbitrarily different things from what you would expect.

If you want complete signatures without dependent types, you need functions which take only single values of different unknown types, like apply: (a -> b) -> a -> b. If you have more than one parameter of the same unknown type, you'll have some ambiguity already.

Non-dependent types can only be used to encode extremely simple properties of a program. They are certainly useful, but they are not in any way the be-all, end-all of static verification.

> Of course that type doesn't encode everything there is to know about that function, even assuming purity.

Right—we need to require foo id = id.

That only works because Haskell can't really express it. That is, if you could write Haskell code that checked that equality, that equality wouldn't be enough, because you could write a function `mapStrange foo [x]` that is equal to `map` if `foo = id` and is something else otherwise.

But since you can't compare 2 functions for equality, and you can't compare two arbitrary values for equality, then yes - your informal requirement is enough togethet with the type to force the function to be `map`.

Sorry for the confusion, I think we are using different definitions of "semantics" here, I'm not talking about formal semantics. I'm considering these to be semantically different, even though their structural types are the same:

    fn min(x: int, y: int) -> int
    fn max(x: int, y: int) -> int

The meaning of a computation changes depending on which one we use.

I probably should have used a different word than "semantics" since that has a technical definition in the PL field...

> I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are.

Can you give an example?

  transferAmount(from: Account, to: Account, amount: Money)

How can a type system know that you are passing the accounts in the correct order?

You might start by trying to make more strict types such as SourceAccount and DestinationAccount.

  transferAmount(from: SourceAccount, to: DestinationAccount, amount: Money)

But we know that any account is likely to be both of these at different times. We only persist Accounts and have to convert at runtime. Now you face the challenge of converting a regular Account to a FromAccount.

  src := fromAccount.toSourceAccount()
  dest := toAccount.toDestinationAccount()
  transferAmount(src, dest, amt)

How can the type system know that you are converting the correct Account? The type system cannot determine what is semantically correct. It's a recursive problem.

What you are saying is all correct, but I think we disagree about the terminology. You said "the type system can never know what is semantically correct" but I think the right way of saying it is "the type system can sometimes not know what is semantically correct".

Because in practice, code like "src := fromAccount.toSourceAccount()" is very rare and happens at system boundaries or logic boundaries once - after that, all semantical errors can be caught by the typesystem, and this accounts for the vast majority of the code.

So yes, the typesystem can and will prevent semantical errors. But it can not protect you from making them in all cases, that's impossible.

A programmer will still need to write correct code, but in your first example the error happens at the boundary between two modules. In the second example, the error is fully contained within one module.

One of those two is easier to spot, either by the original programmer, or by a code reviewer, or by someone trying to track down a fault.

If all the type system does is make semantic errors easier to spot and fix, it's still offering a lot of value.

Reply on news.ycombinator.com