You've just encountered the Curry-Howard Isomorphism. When programming, all a type will typically mean "this is what kind of thing this thing is". Any type system can be trivially converted to an equivalent system of logic, so it stands to reason that once you get a sufficiently interesting type system, you also get a sufficiently interesting logical system. To do logic programming, we encode a proposition in the type of our program, and if we can write a value of that type which the compiler accepts, we have proven that proposition.

We can actually pick apart Haskell's type system and find some problems that make it problematic as a system of logic. We'll start with the basics:

Code: Select all

`-- (a, b) == (A and B), which can also be written (A × B)`

data (,) a b = (a, b) -- we can make a true (a, b) by providing proofs (values) of type a, b

-- Either a b == (A or B), which can also be written (A + B)

data Either a b = Left a | Right b -- we can make a true (Either a b) by providing a proof of type a, OR a proof of type b

-- (a -> b) == (A implies B), which can also be written as (A → B)

-- given a proof (value) of type a, we get a proof (value) of type b

To finish our correspondence with propositions, we need

universal quantification. From the type perspective, "∀" is a way of bringing type variables into scope. Haskell has type variables, but hides the quantification for us. We will turn off that hiding later on, and see that GHC uses the "forall" keyword for this purpose.

Implication is where things start to go wrong for us, in Haskell. Let's take a look at some obvious implications. You'll want to be using a specific invocation of ghci for this:

Code: Select all

`$ ghci -fprint-explicit-foralls`

λ> :t id -- ∀a. a → a

id :: forall a. a -> a

λ> :t const False -- ∀b. b → Bool

const False :: forall b. b -> Bool

λ> import Data.Function

λ> :t fix -- this one is interesting... ∀a. (a → a) → a

fix :: forall a. (a -> a) -> a

The type of fix is somewhat worrying. We (or rather, the standard library) have proved that if a thing implies itself, that thing is true. Do we have any of those implications lying around? Why yes!

Code: Select all

`λ> :t fix id -- oh god, what`

fix id :: forall a. a

Everything is true! This is usually okay, because even if our logical system is unsound, it stops a lot of "obviously false" proofs. For most programming, the type system only needs to make the distinction between "no obvious bugs" and "obviously no bugs".

For an example of a logically sound language, see

Agda, but there's a catch. By rejecting all false proofs, Agda loses the ability to prove some true propositions. Oddly, this also means Agda isn't Turing-complete. As it happens, Gödel's incompleteness theorem in logic corresponds to the halting problem in general programming.

Agda includes many interesting features that help the programmer work around those limitations and convince it of a proof's soundness. Just be prepared for a fairly rough time learning, as it's not yet made it from "learning through research papers" to "learning with tutorials".

<quintopia> You're not crazy. you're the goddamn headprogrammingspock!

<Weeks> You're the goddamn headprogrammingspock!

<Cheese> I love you