That's not true... all turing complete type systems are unsound (where the type metalanguage itself is a turing complete language), but you can have a sound type system of a turing complete language, and in fact haskel itself has such a type system.
All types in Turing complete languages are inhabited by non terminating terms (looping forever, throwing exceptions), which means all propositions are provable.
For instance in Typescript,
const absurd = <A>(): A => absurd()
const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) }
const uninhabited: string & number = absurd()
Intuitively you can think of it like, “Yeah sure, I can build you a term of any possible type, as soon as I get back to you.”, but then the function just ghosts you by looping forever. But it hasn’t lied. However, so long as you’re aware of these gotcha’s they don’t come up much in practice which is why viewing types as proofs is still useful. Just don’t stake your career on one.
Haskell's type system is unsound. Here's an example, where we can prove that 1 + 1 = 1:
{-# LANGUAGE GADTs, TypeFamilies #-}
-- Peano arithmetic: these types represent '0' and '1+n'
data Zero
data Succ n
-- We can define 1 as '1+0', 2 as '1+1', and so on
type One = Succ Zero
type Two = Succ One
-- A closed type family is a function at the type level.
-- This function implements addition of the above Peano numbers.
type family Add x y where
Add Zero y = y
Add (Succ x) y = Succ (Add x y)
-- 'Equal a b' is a proof that types 'a' and 'b' are the same.
-- It works by forcing the type variable 'x' in 'Refl' to unify with both.
data Equal a b where
Refl :: Equal x x
-- The type checker will accept this proof that 1 + 1 = 2, giving:
-- >[1 of 1] Compiling Main
-- Ok, one module loaded.
truePositive :: Equal (Add One One) Two
truePositive = Refl
-- The type checker will reject this proof that 1 + 1 = 1, giving:
-- >[1 of 1] Compiling Main
-- x.hs:24:16: error:
-- • Couldn't match type ‘Zero’ with ‘Succ Zero’
-- Expected type: Equal (Add One One) One
-- Actual type: Equal One One
-- • In the expression: Refl
-- In an equation for ‘trueNegative’: trueNegative = Refl
-- |
-- 24 | trueNegative = Refl
-- |
--trueNegative :: Equal (Add One One) One
--trueNegative = Refl
-- However, the type checker will accept this (unsound) proof
-- that 1 + 1 = 1, giving:
-- >[1 of 1] Compiling Main ( x.hs, interpreted )
-- Ok, one module loaded.
falsePositive :: Equal (Add One One) One
falsePositive = falsePositive
The unsound proof works because our type 'Equal a b' doesn't only contain proofs that a = b (AKA 'Refl'); it also contains infinite loops, like 'falsePositive = falsePositive' (AKA "bottom"). We can use this to undermine any guarantee we try to enforce using Haskell's type system. In fact, we can make a generic version, which can be used to satisfy any type constraint:
loop :: forall a. a
loop = loop
In theory, any time we actually try to use 'loop' our program will freeze; so we might think we're safe from any bad consequences; e.g. if we have 'launchTheMissiles :: PresidentialApproval -> IO ()' we can trick it with 'launchTheMissiles loop', but we're safe since that program contains an infinite loop, right?
Wrong! Haskell is lazy, so it won't bother evaluating arguments which aren't needed. Even if we try forcing the value, we can't be sure that the compiler won't optimise it away! In practice this means that we can't rely on the mere existence of well-typed values as proof of their types; we can be sure that our data dependencies exist (i.e. those values which are forced as part of our computation, which can't be optimised away), but we still won't know that beforehand (i.e. the program may crash or freeze at any point before a particular expression, due to the presence of "bottom" somewhere).
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
I think it's the possibility of nontermination that leads to unsoundness. You can construct a well-typed program that never produces a result, which means the fact that a program has a particular type does not mean you've proved a particular proposition.
