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 _|_.
IsNatis a predicate: making a proposition from a term.
nis a variable.
Sis a function, making a term from a variable.
Zis 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(?)