# CS course at ELTE

This page is to collect all the bits and pieces of source code and other material that I created during my studies at Eötvös Lóránd University. Expect it to be mostly in Hungarian.

# MSc thesis

Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism: My 2011 MSc thesis. For the software behind it, and other details, please check this page.

# Theoretical subjects

## Relational Programming

Read this introductory paper to get an idea of what this is all about. I've put some problems and solutions online. If you understand Hungarian, you're in luck because there's an online textbook in two parts.

## Functional programming languages

• Alef: Interpreter for a toy functional language with lazy evaluation and Hindley-Milner type inference
• Dependent types with Agda: Literate Agda source file and presentation slides, in Hungarian

# Practical subjects

## Programming Environments

Programming assignments for the fall semester of 2005-2006:

## Programming Languages/C++

The assignment was to write a solver for the Sudoku puzzle. Input format: 81 digits (separated by whitespace) describing the board row by row, 0 denoting unspecified cells. Output format: the 81 digits of the solution, or 81 zeros if an error occured (such as wrong input format, or unsolvable puzzle).

To aid testing, I also wrote a small Python script that checks solved Sudoku boards of the format described above.

# Blog

## The case for compositional type checking

23 October 2010 (programming haskell language ELTE) (1 comment)

This is an based on a chapter of the M.Sc. thesis I am writing at ELTE, supervised by Péter Diviánszky.

For my M.Sc. thesis, I've been working on writing a compositional type checker for Haskell 98. The basic idea is to extend Olaf Chitil's compositional type system with ad-hoc polymorphism, Haskell 98's major extension to the Hindley-Milner type system. In this post, I'm showing the motivation behind wanting to go compositional.

A property shared by both commonly-used algorithms for doing Hindley-Milner type inference, W and M, is that both W and M infer the type of composite expressions by inferring one subexpression (in some sense, the “first” one) and using its results in inferring the type of the “next” one. They are linear in the sense that partial results are threaded throughout the type inference.

The effect of linearity on type inference is that certain sub-expressions (those that are processed earlier) can have greater influence on the typing of other subexpressions. This is bad because it imposes a hierarchy on the subexpressions that is determined solely by the actual type checking algorithm, not by the type system; thus, it can lead to misleading error messages for the programmer.

For example, let's take the following definition of a Haskell function:

foo x = (toUpper x, not x)

There are two ways to typecheck this definition using W: either we first typecheck toUpper x, using the context {x :: α}, resulting in the type equation α ~ Char, then checking not x with {x :: Char}, or do it the other way around, by first looking at not x, then as a result recursing into toUpper x with the context {x :: Bool}.

GHC, it seems, does the former, resulting in the following error message:

Couldn't match expected type `Bool' against inferred type `Char'
In the first argument of `not', namely `x'
In the expression: not x
In the expression: (toUpper x, not x)

Whereas Hugs 98 does the latter:

ERROR "test.hs":1 - Type error in application
*** Expression : toUpper x
*** Term : x
*** Type : Bool
*** Does not match : Char

The problem is that they are both misleading, because there is nothing wrong with either not x or toUpper x by itself. The problem only comes from trying to unify their respective views on the type of x.

A compositional type checker, in contrast, descends into toUpper x and not x using the same context, {x :: α}. The first one results in the typing (which is defined to be not just the type of an expression, but also a mapping of monomorphic variables to their types) {x :: Char} ⊢ Char, and the second one in {x :: Bool} ⊢ Bool. Only afterwards are these two typings tried to be unified.

This is better because it becomes meaningful to talk about the typing of a subexpression. For the example above, my work-in-progress compositional type checker can report errors with an (IMO) much more helpful message:

input/test.hs:1:8-25:
(toUpper x, not x)
Cannot unify `Char' with `Bool' when unifying `x':
toUpper x    not x
Char         Bool
x ::  Char         Bool

Of course, the devil's in the details — but that's what my thesis will be about.