Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence I have to ask for forgiveness in advance if the whole question doesn't
make a lot of sense, but unfortunately, I have no better intuition as
of right now and this seems like the best starting point I could come
up with.

I'm reading Tarski's book "Introduction to Logic: and to the
Methodology of Deductive Sciences", I'm on Part VII Chapter 43
"Primitive terms of the theory under construction; axioms concerning
fundamental relations among numbers". It begins by laying out an
elementary mathematical theory of arithmetic of real numbers.

The primitive terms are:


real number (denoted as variables like x, y)
is less than (&lt;)
is greater than (&gt;)
sum (+)
N meaning "the set of all numbers". Thus, an expression "x is a
number" would be written as x ∈ N
is not less than (≮)
is not greater than (≯)


Among the axioms of the theory under consideration, two groups may be
distinguished. The axioms of the first group express fundamental
properties of the relations less than and greater than, whereas those
of the second are primarily concerned with addition. For the time
being, we shall consider the first group only; it consists, altogether,
of five statements:


AXIOM 1. For any numbers x and y (e.g., for arbitrary elements
of the set N) we have: x = y or x &lt; y or x &gt; y
AXIOM 2. If x &lt; y, then y ≮ x
AXIOM 3. If x &gt; y, then y ≯ x
AXIOM 4. If x &lt; y and y &lt; z, then x &lt; z
AXIOM 5. If x &gt; y and y &gt; z, then x &gt; z


Our next task consists in the derivation of a number of theorems from
the axioms adopted by us:


THEOREM 1. No number is smaller than itself x ≮ x
THEOREM 2. No number is greater than itself: x ≯ x


Now I have to stop and finally explain my intentions. I've heard many
times about a so-called "Curry–Howard–Lambek correspondence", and it
made sense whenever I've read examples of it. I am also not
comfortable with manually writing out the reasoning to prove the
theorems, I'd like the machinery of going through reasoning steps to
be checked by a computer for me.

So, I tried to encode the terms, axioms and potentially theorems (got
stuck earlier) in Haskell, but I failed in many ways. I won't show you
all the examples of what I did, but here's the most naive approach of
encoding propositions as types and their proofs as programs:

data Nats
  = NatX
  | NatY
  | NatZ

x :: Nats
x = NatX

data OpGt =
  OpGt Nats
       Nats

data OpLt =
  OpLt Nats
       Nats

data OpEq =
  OpEq Nats
       Nats

data OpNotLt =
  OpNotLt Nats
          Nats

data OpNotGt =
  OpNotGt Nats
          Nats

data Ax1Res
  = Ax1ResLt OpLt
  | Ax1ResGt OpGt
  | Ax1ResEq OpEq

-- how to implement best?
ax1 :: Nats -&gt; Nats -&gt; Ax1Res
ax1 = undefined

-- this doesn't describe the x and y in the type
ax2 :: OpLt -&gt; OpNotGt
ax2 = undefined


This piece of code brings more questions than it gives answers:


should axioms be implemented or kept as unimplemented functions
which we just assume to exist?
how do I limit the implementation of my functions to only rely on
available theorems and axioms if I can construct basically any term?
Should I hide the constructors?
types should obviously contain variables like x and y, I tried
that in other approaches but that gets even hairier


My questions are:


what would be a proper implementation of such proofs in Haskell?
what materials should I read in order to make a proper
implementation myself and understand the topic better?


I hope the vagueness and my level of ignorance in the question will not
put you off from answering it. Thank you!
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