Hi everyone! I'm starting a new series on Steemit. I'll be teaching you how to program in Haskell (functional programming part) and how to prove your programs.

Both parts are about formalizing and reasoning about programs. These are fundamentals in Computer Science.

You might wonder why this is important: Reasoning of programs leads to correctness. Take the Ariane 5 as a example when correctness can be expensive.
Or look for example SMART CONTRACTS. One should be able to prove them!

Today we'll look at Haskell syntax and its base types. and afterwards we'll learn how we can prove those programs and for that we'll have also a quick look on logic.

Introduction to Functional Languages

We'll look quickly at what algorithm means. 

We can say that an algorithm is actually a Turing Machine which always stops.

Therefore we can find equivalent definitions of algorithms with for example: a Java program, a executable function descripton, ...

Let's look at the difference of when definitions of algorithms with object-oriented languages as Java and functional executable descriptions.

In Java, we update memory. In functions we compute values. 

In Java we have to understand how states can change. For this we'll learn later something about Hoare Logic which lets us reason about programs.

In Haskell (which is of course the executable function description) we formalize what should be computed and not how.

Basic concepts

• Functions compute values and function are values. They can compute and return them.
• There are no side-effects. A function f(x) has always the same result. (*look at the bottom, where I have an example in Java where a function returns different results.) So we can reason mathematically.
• There are no assignments, no global variables, ...
• Instead of iteration we're using recursion

How we will use Haskell

We'll use the Glasgow Haskell Compiler (GHC).  This is available on all platforms and simple to install. You can find online many sources for how to install it on your OS. But if requested I can show it to you next time.

For now I'll assume you have GHC on you computer!

Quick GHC Guide

Go to your terminal and write

ghci

For loading the functions from your own haskell function write:

:load myProgram.hs

As you see Haskell files end with .hs .

If not you can basically use all functions which are in the Haskell Prelude.

Here some examples:

//Edited this part, some how the code block was f*cked up.

Try it yourself!

As you see in the last two lines we used gcd 70 15. This is a function from the haskell Prelude that calculates the greates common divisor of two numbers.

In mathematics we would write this as: gcd(70,15). As we see we can define the function with variables like this:
gcd(x,y).

In Haskell it's similiar. We simply write:
gcd x y

Syntax and Types

By the way the code for the gcd function in Haskell is:(maybe you can understand it ;)   )

gcd x y                     --functions + args start with lower case letter
 | x == y = x
 | x > y = gcd (x-y) y      --args seperated by whitespace and are 
 | otherwise = gcd x (y-x)  --written in sequence

We see the program has these "|". These are the cases (like if in Java).  The boolean conditions are usually called guards. They usually look like normal boolean expressions. The otherwise means if no guard is true the expression of the guard otherwise is the result.

So the general structure of programs using guards is:

functionName x1 ... xn
 | guard1 = expr1
  .
  .
  .
 | guardm = exprm 

But you can also use functions as arguments (which we will look at later on), define constants (which are actually programs),... So programs must have several definitions of functions, constants and so on.

For example we can define a constant (function with no argument that return alway the same result and use it in another function).

myConstant = 3            --This is a function too!

myFunction x = myConstant * x

Pay attention that we don't use semicolones. We use whitespaces instead.
As you can see we have a two-dimensional layout. General rule I use: whenever I think I would use TAB in Java I should use a whitespace instead.
Okay let's precise that a little bit now. 

• All definitions of functions must start at the same indentation level.
• If the definition runs over n lines, indent the lines from 2 to n further. (look at example gcd)

DO NOT USE TABS, SINCE YOU'LL HAVE TO FIND THE MISSING WHITESPACE THEN AND TABS MAKE THAT MUCH MORE DIFFICULT!

Haskell is a strongly typed language. So therefore we have types to avoid Runtime Errors like 4+False.
Before every function definitions we provide the types like this:

gcd :: Int -> Int -> Int

Which means: "The function gcd takes as first argument Int, as second argument Int and gives us an Int back.

The most left type is the type of the first argument, the one after that is the type of the second and the last one is the one of the result.

When using functions with values, the compiler will check if the types match.

• Int
  1. Values: ... , -2 , -1 , 0 , 1 , 2 , ...
  2.  Functions: +, *, ^, -, div, mod, abs 
  3. Operators can be also written in Prefix notation:     (+) 1 2     is the same as     1 + 2
  4. Operators have different binding strengths ( same as in mathematics)
  5. We can use ordering operators on two Int: <,>, ==, <=, >=
     They return either True or False
• Bool
  1. Values: True , False
  2. Binary operators (which work as you would expect them): && and ||
     unary  function not (works as expected)
•  Char
  Look this up on your own. Pretty simple
• String
  Look this up on your own. Pretty simple.
  But in addition to this I want to say that String is a List of Chars.
• Double
  Look this up on your own. Pretty simple
• Tuple
  We define Tuples like this for example (Int,Int) or (String , Char , Double). I think you'll get it.

I think that's enough for the moment. 

Next time we'll look on the beautiful lists and much more. Stay tuned! ;)

I hope you enjoyed this Introduction and are ready to learn much more about Haskell and proving your programs.

Cheers

All Lessons

Lesson 1: Introduction to Functional Programming and Formal Methods

Lesson 2: Haskell Lists Part 1