Is this what people mean when they say, Haskell's type system is sound?
We know Haskell's type system includes bottom as an inhabitant of every type which enables us to shrug and hand-wave away proofs of termination. As long as one understands that consequence doesn't it pass Milner's definition?
I'm happy writing proofs in Lean or Agda but having to avoid or prove termination would be a pain in the rear end for most large programs. And in practice I still think of Haskell's type system as sound. I always thought of "unsound" as programs with terms that are logically inconsistent with respect to the theorems proposed by the types, eg: early version of TypeScript or Java. Put another way, that you could write a proposition in they type system that wasn't satisfied by the program (proof).
> Is this what people mean when they say, Haskell's type system is sound?
It depends on the context, but it's certainly in common use (e.g. see https://stackoverflow.com/questions/21437015/soundness-and-c... although I switched 'positive' and 'negative' in my example: e.g. I treat 'true positive' as 'correct program was accepted', that link treats 'true positive' as 'error message was justified')
> As long as one understands that consequence doesn't it pass Milner's definition?
Milner's definition is usually summarised as "well-typed programs have well-defined behaviour". Haskell does fit this description, although certain optimisations may be unsound (e.g. library-supplied rewrite rules).
To me, the key deficiency is that Haskell can't ignore 'absurd' branches. For example, let's say we have a function like this:
foo :: a -> b -> LessThan a b -> Foo
foo Zero (Succ y) _ = bar y
foo (Succ x) (Succ (Succ y)) _ = baz x y
If 'a' and 'b' represent numbers (with singleton values), and 'LessThan a b' describes proofs that a < b (see e.g. http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html for how to encode such proofs), then these two branches form a complete definition of 'foo': the combinations 'foo _ Zero _' and 'foo (Succ x) (Succ Zero) _' can't occur, if we trust the 'LessThan a b' proof. In Agda, Coq, etc. we can either leave out those absurd branches (if the compiler can spot their absurdity), or in more complicated cases we can satisfy the type checker by proving they lead to a contradiction.
In Haskell we can't do this: the type of one argument can't rule-out values of another. Hence we must define those branches (or else leave the implicit "unmatched pattern" error, which is a "bottom"), and we need them to return values of type 'Foo' (which may be impossible to construct, unless we return "bottom"). This satisfies Milner's definition, but also goes too far: we're specifying well-defined behaviour for programs which aren't well-typed! In practice, this leads to redundant branches like 'Nothing -> error "Shouldn't happen"', which (a) introduce potential crashes and (b) are so close to being statically avoided!
> having to avoid or prove termination would be a pain in the rear end for most large programs
We know Haskell's type system includes bottom as an inhabitant of every type which enables us to shrug and hand-wave away proofs of termination. As long as one understands that consequence doesn't it pass Milner's definition?
I'm happy writing proofs in Lean or Agda but having to avoid or prove termination would be a pain in the rear end for most large programs. And in practice I still think of Haskell's type system as sound. I always thought of "unsound" as programs with terms that are logically inconsistent with respect to the theorems proposed by the types, eg: early version of TypeScript or Java. Put another way, that you could write a proposition in they type system that wasn't satisfied by the program (proof).