Gave a Talk on Function Totality

As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.

Continue reading

Function Totality: Abstraction Tool in Programming

Edsger Dijkstra said the following of abstraction:

“The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”

Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this article I will explore an important tool in achieving abstraction in programming: function totality.

Continue reading

Typed Functional Programming and Software Correctness

Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.

Continue reading

Less bad MTL

I stumbled upon a recording of a talk by George Wilson on the monad transformer library (MTL) in Haskell. He goes on to demonstrate how monad transformers can be made more composable by using constraints instead of directly putting a monad transformer in the return type of a function. What is presented there is definitely an improvement, however it is still unsatisfactory. In particular, in his examples there is no separation of describing and running a program, which means everything happens in the IO monad (the MonadIO constraint in function signatures in the examples). In other words, anything goes and such functions are again too powerful.

Continue reading

Haskell IDE The Memory Hog Engine

Momentarily, the Haskell IDE Engine (HIE) is in a bad shape. In its version 0.2.2, it eats a huge amount of memory, much more than my machine can provide (I have 8 GB in total). Users have already reported this, and even though there is a memory leak in GHC, Haskell IDE Engine developers haven’t started tackling this problem yet. What you can do in the meantime is to provide runtime system (RTS) options to an engine executable to limit its heap and stack memory sizes. For example, you can write a wrapper script around the hie executable that would run it with the following RTS options:

hie +RTS -c -M1500M -K1G -A16M -RTS --lsp $@

This limits the heap size to 1500 MB and the stack size to 1 GB. The executable will crash once it surpasses these limits, but your editor (e.g., Atom) should restart it. In other words, HIE will keep on crashing and restarting in a loop, which is ugly, but that’s what we have now.