intro.tex

\chapter{Introduction}
One of the inherent problems of engineered systems in general is that the design of the system is not proven to work. The system could be non-functional at design time. The designer may not fully understand the system environment or may have not considered the behavior of the system in rare circumstances. Then, once the design is made, there may be issues introduced by implementing the design incorrectly.

Within the context of computer programs, the current way that programs are created is by making a design or a formal specification of the program, implementing it, and testing the program against unit tests, or verifying the behavior of the program after the fact.
Formal methods are ways to mathematically prove the correctness of a system. Without formal methods, the only way to reason about a system is by testing it against various edge cases.

Within the context of a programming language, one way a programming language can be formally specified is by defining a syntax and semantics for that language.
The operational semantics of a programming language can be thought of as a transition system upon an abstract syntax tree, which is the program itself written in the language, and a state, which is a function from the variables in the tree to the current values of those variables. 
This way, real and complex programs written in natural-looking programming languages can be interpreted as strings written in formal languages. Once a programming language is defined in this way, certain properties and behavior of the language and programs written in the language can be proven.

K \cite{rosu-serbanuta-2010-jlap, KFrame} is a framework for creating the formal specification of a programming language. It then can interpret programs written in the language by running only the rules of the formal operational semantics of the programming language. This allows programs to be run and analyzed formally. This way, the formal specification of the complex programming language can be tested and analyzed with the use of a machine.
A K-configuration defines the memory structure of the programming language, which is made up of cells. The program state can be thought of as the current values of the K-configuration at a certain point in time.
Grammar can be written in K using the constructor \texttt{syntax}, and a semantic rule can be written in K using the constructor \texttt{rule}.

Haskell is a purely functional programming language with strong static typing. "Purely functional" means that the language only allows the user to make functions whose output is only dependent on the function input. Strong static typing means that before a program is run, a type inference algorithm infers the type of the program and ensures that all functions and function applications are allowed with regard to the type of the inputs and outputs. "Static" refers to the fact that type inference is performed before the code is run, and will not run during the runtime of the code. Strong typing refers to the fact that the compiler will not allow the user to perform workarounds like typecasting.

The Haskell 2010 report gives a cursory description of the type system as a Standard Hindley Milner polymorphic type system, but gives no further indication of how this applies to the specifics of the Haskell syntax.

In addition, by studying the standard Haskell compiler, one can see that there must be additional context-sensitive checks that must be made prior to type inference.

In Robin Milner's work, their type system is based on a more simple ML system. In Haskell, the semantics needs to worry about parsing, preprocessing, modules, expressions, declarations, and so on.

Also, an important part of the Haskell language is mutual recursion of functions. Functions can refer to each other within a Haskell program.

In the specification in this paper, a more complete specification of parts of the type system is presented as a family of mutually inductive rules. Such a presentation is not only the basis of an executable semantics but can later provide the basis of formal and rigorous proofs.

This project details the syntax of Haskell and the type system of Haskell in K.

The repository of the K semantics is provided at:

\url{https://github.com/liyili2/haskell-semantics/}