abs.tex

This thesis introduces a static semantics for Haskell by utilizing the K-Framework. This implementation includes support for the module system of Haskell but not for type classes. Many layers have to be implemented in K before type inference can be performed. The first part of the implementation is the entire context-free syntax of Haskell in K. Since all the syntax is included, any program written in Haskell extended syntax can be parsed into an abstract syntax tree. However, this includes only the Haskell extended syntax, not syntactic short-cuts such as treating tabs as syntactic sugar for grouping constructs such as curly braces. Programs that include multiple modules can be parsed, but the multiple modules must be written in a single file. This is unlike how the Glasgow Haskell Compiler allows for module imports, where each module must be kept in a separate file. The multiple modules are then made as nodes in a directed acyclic graph. A directed edge in the graph represents a module importing another module. This graph is used for importing the user-defined types from one module into another module. Context-sensitive checks and type inference are then performed on modules. The static semantics specifies that, at each node in the graph, assuming all child modules are already checked and inferred, the user-defined types of each of the child modules are imported into the module at the given node. All rules of the Haskell type system must take mutual recursion into account. There is repeated layering of inferences in Haskell. Due to being written in K, the semantics introduced here is mathematically precise and executable. Since the semantics is executable, the semantics can be tested against test sets to validate the correctness of the semantics. The executability of the semantics was utilized to test both positive inferences and exceptional inferences. This is part of a larger project to give a formal semantics to Haskell.

Subject Keywords: Haskell; Type-System