A Kind System for a Functional Programming Language
Name
Liisi Kerik
Abstract
Static type systems find some classes of bugs before the program is run, thereby assisting in writing safer code. Many functional languages, for example, Haskell and Idris, are statically typed.
The more expressive a language's type system is, the more bugs can be found during type checking. Some languages, for example, Idris, use dependent types, which result in an expressive albeit complex type system. Promotion, which has been recently introduced in Haskell, improves the expressiveness of the type system without resorting to dependent types by endowing the language with type level data, like type level natural numbers and lists. Together with generalised algebraic data types it allows the programmer to construct, for example, statically sized vectors and tuples of arbitrary length.
The aim of this work was to develop a statically typed functional language with a type system that has been enriched via promotion. The language which is the result of this work, Awful, shows that promoted kinds and types have many useful applications even in a language that does not have generalised algebraic data types.
Instead of generalised algebraic data types Awful employs a more restrictive but also considerably simpler new way of constructing new data types. Branching data types enable construction of many useful data structures, like statically sized vectors, for which we would use generalised algebraic data types in Haskell or Idris.
The more expressive a language's type system is, the more bugs can be found during type checking. Some languages, for example, Idris, use dependent types, which result in an expressive albeit complex type system. Promotion, which has been recently introduced in Haskell, improves the expressiveness of the type system without resorting to dependent types by endowing the language with type level data, like type level natural numbers and lists. Together with generalised algebraic data types it allows the programmer to construct, for example, statically sized vectors and tuples of arbitrary length.
The aim of this work was to develop a statically typed functional language with a type system that has been enriched via promotion. The language which is the result of this work, Awful, shows that promoted kinds and types have many useful applications even in a language that does not have generalised algebraic data types.
Instead of generalised algebraic data types Awful employs a more restrictive but also considerably simpler new way of constructing new data types. Branching data types enable construction of many useful data structures, like statically sized vectors, for which we would use generalised algebraic data types in Haskell or Idris.
Graduation Thesis language
Estonian
Graduation Thesis type
Master - Computer Science
Supervisor(s)
Härmel Nestra
Defence year
2018