4 ms·

There’s a deep connection between Types and Logical Proofs (Curry Howard Correspondence). Haskell has a rich type system that allows you to “prove” (i.e. typech

There’s a deep connection between Types and Logical Proofs (Curry Howard Correspondence). Haskell has a rich type system that allows you to “prove” (i.e. typecheck) many properties of your program. This is valuable when getting right the first time is important such as smart contracts. I put prove in quotations because all type systems of Turing complete languages are unsound, but this doesn’t matter too much in practice. If you wanted to be really sure, you’d use a total language like Idris or Coq.

bodhiandpysics1 6y ago
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.
- xkapastel 6y ago
  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.
- chriswarbo 6y ago
  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).
  - agentultra 6y ago
    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).
    - chriswarbo 6y ago
      > 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...
- deleted 6y ago
  [deleted]
- BreakfastB0b 6y ago
  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.

bodhiandpysics1 6y ago

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.

xkapastel 6y ago
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.
chriswarbo 6y ago
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).
- agentultra 6y ago
  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).
  - chriswarbo 6y ago
    > 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...
deleted 6y ago
[deleted]
BreakfastB0b 6y ago
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.