> 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://stackov

> 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-completeness-of-systems 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 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 It can be. If we're being lazy, we can just wrap things in a 'Delay'/'Partial' type (described a little in the above "nat-like types" link, and also at https://news.ycombinator.com/item?id=17472926 https://news.ycombinator.com/item?id=17472926) or run proofs in Coq's Mtac language ( https://plv.mpi-sws.org/mtac https://plv.mpi-sws.org/mtac ) > And in practice I still think of Haskell's type system as sound. Me too. This tends to be called "fast and loose reasoning" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loo...