Curry Howard correspondence to Predicate Logic?

Question

So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell tutorials linked from wikipedia, esp Tim Newsham's. There's also a useful discussion when Newsham posted the tutorial.

(But I'm going to ignore Newsham's and Piponi's data wrappers, and talk about the underlying types.) We have Hilbert's axiom scheme (expressed as S, K combinators); we have propositions as types; implication as function-arrow; and Modus Ponens as function application:

axK :: p -> q -> p
axK  = const
axS :: (p -> q -> r) -> (p -> q) -> p -> r
axS     f                g          x  = f x (g x)

modPons = ($);   infixl 0 `modPons`          -- infix Left, cp ($) is Right

Then I can derive the identity law:

ident     = axS `modPons` axK `modPons` axK  -- (S K K)
-- ident :: p -> p                           -- inferred

Having these types as bare typevars merely corresponding to propositions seems rather unimaginative. Can I use more of the type system to actually construct the propositions? I'm thinking:

data      IsNat n  = IsNat !n                -- [Note **]

data      Z        = Z
axNatZ ::            IsNat Z
axNatZ             = IsNat Z

data      S n      = S !n
axNatS :: IsNat n -> IsNat (S n)
axNatS   (IsNat n) = IsNat (S n) 

twoIsNat = axNatS `modPons` (axNatS `modPons` axNatZ)
-- ===> IsNat (S (S Z))

[Note **] I'm using strict constructors, as per the discussion thread, to avoid introducing _|_.

Where:

• IsNat is a predicate: making a proposition from a term.
• n is a variable.
• S is a function, making a term from a variable.
• Z is a constant (niladic function).

So I seem to have embedded (First-Order) Predicate Logic(?)

I appreciate my types are not very hygienic; I could easily mix up a typevar-as-proposition with a typevar-as-term. Perhaps I should use the Kind system to segregate them. OTOH my axioms would have to be spectacularly wrong to get to any conclusion.

I haven't expressed:

• universal quantifier: it's implicit for the free vars;
• existential quant: in effect constants could act as skolemised existentials;
• equality of terms: I've used repeated typevars in implications;
• relations: this seems to work, or is it fuddlement? ...

    data          PlusNat n m l  = PlusNat !n !m !l

    axPlusNatZ :: IsNat m       -> PlusNat Z m m
    axPlusNatZ   (IsNat m)       = PlusNat Z m m

    axPlusNatS :: PlusNat n m l -> PlusNat (S n) m (S l)
    axPlusNatS   (PlusNat n m l) = PlusNat (S n) m (S l)

    plus123 = axPlusNatS `modPons`
              (axPlusNatZ `modPons`
               (axNatS `modPons` (axNatS `modPons` axNatZ)) ) 
    -- ===> PlusNat (S Z) (S (S Z)) (S (S (S Z)))

Writing the axioms is easy, courtesy of Wadler's Theorems for Free!. Writing the proofs is hard work. (I shall drop the modPons and just use function application.)

Is this actually achieving a logic. Or is it crazy stuff? Should I stop before I do any more harm to my brain?

You're supposed to need Dependent Types to express FOPL in Curry-Howard. But I don't seem to be doing that(?)

Answer 1

To explain why I'm uncomfortable with Newsham's and (especially) Piponi's data wrappers ... (This is going to be more question than answer, but perhaps it'll work towards explaining what's wrong with my IsNat even though it seems very similar to Newsham.)

Piponi page 17 on has:

data Proposition = Proposition :-> Proposition
                  | Symbol String
                  | False deriving Eq

data Proof = MP Proof Proof
     | Axiom String Proposition deriving Eq

I see no types here. Spelling a data constructor :-> does not make it function arrow; and spelling a data constructor MP (for Modus Ponens) does not make it function application. There's a 'smart constructor' operator (@@) for MP, but that doesn't apply no function: it merely does pattern matching on the :-> constructor.

Newsham has (I'll start with the Implication section/Modus Ponens):

data Prop p = Prop p

data p :=> q = Imp (Prop p -> Prop q)

impInj :: (Prop p -> Prop q) -> Prop (p :=> q)
impInj p2q = Prop (Imp p2q)

impElim :: Prop p -> Prop (p :=> q) -> Prop q
impElim p (Prop (Imp p2q)) = p2q p

This looks more like it: we have types, function arrows, function application in impElim. The type constructor Imp with its injection and elimination rules mirror the proof tree structures in the Lectures on Curry-Howard isomorphism. But I'm nervous: why does Imp need a type constructor and data constructor? Again, spelling as :=> doesn't make that a function arrow. Why all this wrapping and unwrapping Prop constructors? Why not plain Prop (p -> q)?

So when I look at the 'Conjunction' section (which actually comes first):

data p :/\ q = And (Prop p) (Prop q)

andInj :: Prop p -> Prop q -> Prop (p :/\ q)
andInj p q = Prop (And p q)

andElimL :: Prop (p :/\ q) -> Prop p
andElimL (Prop (And p q)) = p

andElimR :: Prop (p :/\ q) -> Prop q
andElimR (Prop (And p q)) = q

Those Elim functions don't use function application. They merely pattern match on the constructors. There's no implicational structure for conjunction: we rely entirely that the 'programmer' has used only the andInj rule to build a type (p :/\ q).

So when Newsham gets to the commutativity of conjunction:

commuteAnd :: Prop (p :/\ q) -> Prop (q :/\ p)
commuteAnd pq = andInj (andElimR pq) (andElimL pq)

And claims

Notice that our Haskell proof did not contain any reference to the internal structure of the (:/\) data type. Having defined and proven our rules "andInj", "andElimR" and "andElimL" we shouldn't ever have to peek into the implementation of the (:/\) data type again.

I plain disagree:

• The signature for commuteAnd does rely on the internal structure of the :/\ type constructor.
• Although the function definition looks like merely function application, in fact the andElims do "peek" into the structure.

I'd expect we could prove the commutativity of conjunction from its definition, without needing an axiom to say so(?)

OK if I'm being so purist, what do I expect? This for conjunction is based on the Church encoding for pair:

type Conj p q r = Prop ((p -> q -> r) -> r)     -- not right, see later

andInj :: Prop p -> Prop q -> Conj p q r
andInj (Prop p) (Prop q) = Prop (\elim -> elim p q)

andElimL :: Conj p q p -> Prop p
andElimL (Prop conj) = Prop (conj axK)    -- axK is `const`

Now I can write commuteAnd using 'proper' function application:

--  commuteAnd :: (Conj p q r) -> (Conj q p r)
commuteAnd pq = andInj (andElimR pq) (andElimL pq)

That function definition is the same as Newsham's. But I've commented out the signature because GHC's inferred type is not general enough. It wants Prop ((p -> p -> p) -> p) -> ((p -> p -> p) -> p). Which is only a fancy variation on the Identity law.

Edit: (After @DerekElkins first comment here.) Scrap all this:

I've ended up in deep (and murky) water. I think my type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:

type Conj p q = Prop (forall r.((p -> q -> r) -> r))

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky".) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to use.

I do need a higher-rank type, but not Impredicative. And not on the type for Conj but for commuteAnd

commuteAnd :: (forall r. Conj p q r) -> (Conj q p r')
-- (same function for `commuteAnd` as above)

OK. I can happily swap arguments ad infinitum.

[End of Edit]

So my question: if it's legit what Newsham is doing with nesting constructors and pattern matching everywhere, then what's not legit about my IsNat and pattern matching?