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.
In case you are a Haskeller interested in learning Idris, check out a short list of things to look out for.
You might think it’s only imperative programmers that don’t see value in function totality, but neither do many functional programmers. The ability to abstract in programming is severely impaired when totality is ignored. A programmer should strive to work in a programming language with a compiler that supports totality checking, such as Agda and Idris.
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.
The state of software engineering is best illustrated by an XKCD on voting software.
To get the Haskell IDE Engine working in the Atom editor, one has to start Atom in the directory of a project. I’d call this a bug.
It happened two months ago, but Idris 1.3.0 is out.
From Haskell’s safe-exceptions library: “[I]ncomplete pattern matches can generate impure exceptions.” This makes me think of Agda, its totality and absence of exceptions.
Haskell’s forall, in combination with some GHC extensions, allows for liberal type synonyms and scoped type variables, among others. Source: School of Haskell.