7
$\begingroup$

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(?)

$\endgroup$
  • 1
    $\begingroup$ The issue with your approach is IsNat is not making a proposition from a term, it's making a proposition from a proposition. $\endgroup$ – Derek Elkins Jul 13 '17 at 18:46
  • $\begingroup$ Thanks @DerekElkins, I guess you mean the argument to IsNat is just a type, so must be a proposition. OK, equally IsNat n is just a type so must be a proposition. I must be 'on my honour' not to let n escape into proposition-land/appear as argument to a logical connective (which is why I talked about type hygiene). Would you be happier if I used Church encoding for Nats? I think I'm just extending λ-calc with constructors at the type level, same as Haskell at the term level(?) $\endgroup$ – AntC Jul 14 '17 at 1:14
  • $\begingroup$ P.S. perhaps n is a proposition: it's saying 'I am inhabited'. Which is no more than any typevar is saying under CH. IsNat n is saying/witnessing: furthermore, the inhabitant of n is of a particular 'Kind', aka 'sort' in logic. Then I'm going beyond Simply-typed λ-calc(?) $\endgroup$ – AntC Jul 14 '17 at 2:28
  • 1
    $\begingroup$ I don't think that learning about the Curry-Howard Isomorphism by playing around with arcane programming languages is the right approach. It isn't going to lead to any true understanding of the principle. $\endgroup$ – Miles Rout Jul 18 '17 at 1:18
  • 1
    $\begingroup$ If you don't understand the texts, then you should learn what you need to understand the texts. Haskell is not one of those things. $\endgroup$ – Miles Rout Jul 18 '17 at 22:16
3
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ As Piponi states, the Proposition and Proof types aren't examples of the Curry-Howard correspondence in action. Those just form a simple LCF-style proof system. The Curry-Howard correspondence is witnessed by the compile function (though most of the work is done by (^) and show) which turns those Propositions and Proofs into Haskell code. As for Newsham's code, the wrappers make no difference (:=>) is essentially (->). He only adds them (as he explicitly states) so he can swap in a different, non-trivial implementation later on. $\endgroup$ – Derek Elkins Jul 17 '17 at 5:20
  • $\begingroup$ Thanks. wrt Neasham, I wanted to stick with Intuitionistic Logic, not Classical; so ignored the continuations/monad stuff. Are you saying his def'ns don't work for Intuitionistic? Yes (:=>) is implemented as (->). But a model/simulation of a logic, needs a validation of the interpreter(?). Why can't I express direct in Haskell (->)? $\endgroup$ – AntC Jul 17 '17 at 9:55
  • $\begingroup$ Similar remarks wrt Piponi: he introduces (^) to deal with Classical. OK I'll try his show to generate Haskell code and see how that differs. (I'll also try to figure out how he's introducing Integer.) I'm trying to use a minimum of Haskell machinery, for fear I'll introduce _|_ somewhere and undermine "programs are proofs". $\endgroup$ – AntC Jul 17 '17 at 10:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.