Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence
Proofs in Haskell?

Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific logic a particular programming language represents.

In particular, Haskell lacks dependent types. That means that it can't express statements with "forall x" or "exists x". So immediately there's no way to encode your axioms. 
The problem is that Haskell's types only let you refer to other types, not to specific values of those types. Your axiom says "forall x and y, Property holds for x and y": it's reasoning not about $Nat$ as a class, but about specific values of that class.

There are ways to fake it in Haskell, by encoding values with a type-level representation, but I'd strongly recommend against those for a beginner.

What does the Curry-Howard Correspondence Actually Mean?

What Curry-Howard is actually saying is not that we can write a program that implements a checker for proofs. What is says is that we can view a proof as a form of a program in a purely-functional language. Specifically, a proof is like a program that takes proofs of its assumptions as input, and produces proofs of its conclusions as outputs.

The key is that propositions are like types, and proofs are like programs. So in your example, it doesn't make sense to have an implementation of your axioms, since axioms are propositions that you take as true, without proof. An implementation would correspond to a proof of them.

The real magic of Curry-Howard comes when we introduce dependent types. The key is the dependent function type: instead of just having $A \to B$, we have $(x:A) \to B$, where $x$ can occur in $B$. 

There's a lot going on here. First, we've blurred the line between types and values. In the same way that the type constructor List takes an argument to become a type, like List Int, we now can have type constructors that take values as arguments.

The classic example of this is $Eq$ for representing proofs of equality. For any values $x,y$, $Eq\ x\ y$ is the type of proofs that $x = y$. So we have a type indexed on values.  

Secondly, we've now given names to our arguments in the type, not just in the implementation. So the order of arguments very much matters, because the types on the right can refer to the names on the left. They depend on the names, thus the name dependent types.
What this is really saying is that the return type of the function can change, depending on the value of the argument given.

Curry-Howard then says that, if we produce a well typed function of type $(x:A) -&gt; B$, this is the same as saying "for all $x$ that satisfy $A$, $B$ holds".

The dual of this is dependent pairs, which code "exists" proofs. Instead of having the tuple type $(A,B)$, we now have $(x:A, B)$, where $B$ can refer to $x$. This means that the type of the thing on the right can depend on the value of the thing on the left. This is a constructive form of an existential proof: the way you prove "there exists an x satisfying B" is by saying "here's the x, and here's the proof it satisfies B".

Where to learn more?

If you want to prove things in a formal setting, I'd recommend
Coq, Agda, Idris, or Isabelle, since they have the machinery
for dealing with dependent types and proving things.

Some good free resources:


Software Foundations
Certified Programming with Dependent Types
Lean You An Agda and Achieve Enlightenment


Some nice articles/papers/tutorials on the topic include:


Propositions as Types
The Power of Pi
Tutorial Implementation of Dependently Typed Lambda Calculus


The Idris book is popular, but not free: 
Type Driven Development in Idris