The Haskell Elephant in the Room

Re:The Haskell Elephant in the Room by chriswarbo on Thursday July 30, 2020 @01:33PM (#24000839)

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).

[ Parent | on HN ]

Re:The Haskell Elephant in the Room by agentultra on Thursday July 30, 2020 @02:40PM (#24001538)

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).

[ Parent | on HN ]

Re:The Haskell Elephant in the Room by chriswarbo on Thursday July 30, 2020 @06:02PM (#24003339)

> 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

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) or run proofs in Coq's Mtac language ( 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+loo...

[ Parent | on HN ]