### Reflecting on Haskell in 2016

Well, 2016 ... that just happened. About the only thing I can put in perspective

at closing of this year is progress and innovation in Haskell ecosystem. There

was a lot inspiring work and progress that pushed the state of the art forward.

This was a monumental year of Haskell in production. There were dozens of talks

given about success stories with an unprecedented amount of commercially funded

work from small startups to international banks. Several very honest accounts of

the good and the bad were published, which gave us a rare glimpse into what it

takes to plant Haskell in a corporate environment and foster it's growth.

- A Founder's Perspective on 4 Years With Haskell by Carl Baatz
- The Story of Haskell at IMVU by Chad Austin
- Four Months with Haskell by Alexis King
- The Joy and Agony of Haskell in Production by Stephen Diehl
- Production Haskell by Reid Draper
- The day to day practice of using Haskell to write large systems by Don Stewart

#### Writing

There was a lot of excellent Haskell writing this year. One can't possible

enumerate all of them, but several stood out as concise and mind-bending

examples of practical Haskell:

- Raytracing Black Holes with Haskell by Sakari Kapanen
- Exploratory Haskell by Parsons Matt
- State of the Haskell Ecosystem by Gabriel Gonzalez
- Introducing the Hamilton Library by Justin Le
- Practical Dependent Types in Haskell: Type Safe Neural Networks by Justin Le
- Mutual Recursion in Final Encoding by Andreas Herrmann
- An Algebra of Graphs by Andrey Mokhov
- GHC optimization and fusion by Mark Karpov
- Hindley-Damas-Milner tutorial by David Luposchainsky
- Write You a Scheme 2.0 by Adam Wespiser
- Proving Stuff in Haskell by Mads Buch
- Making Movie Monad by David Lettier
- Selling Haskell in the Pub by Neil Mitchell
- Little Languages by David Laing

The second edition of Graham Hutton's book Programming in

Haskell

was released, which updated the presentation to include modern Haskell including

recent changes concerning applicative, monadic, foldable, and traversable types.

In addition there were several great lecture series by Bartosz Milewski on

relevant Haskell topics that are generally underserved in writing.

#### Uncategorized Projects

There was a lot of open source work done this year, a few that stood out as

particularly novel ideas or interesting ways of looking at problems through a

Haskell lens:

- grenade A dependently typed, practical, and fast neural network library.
- implicitCAD A math-inspired CAD engine in Haskell.
- hylogen GLSL embedded in Haskell.
- sparkle Haskell on Apache Spark.
- bench Command-line benchmark tool.
- roper A return-oriented programming exploit toolkit using genetic programming.
- tensor-ops Type-safe tensor manipulation operations in Haskell
- formal-morality A Pseudo-Rawlsian domain language in Haskell.
- protobuf-simple A simpler Protocol Buffers library for Haskell.
- rts-loader A Haskell dynamic RTS loader supporting multiple GHC APIs.
- hge2d 2D game engine written in Haskell.

#### Haskell Sucks

On a reflective note, there were quite a few dogpile

threads

in which we collectively ripped on our beloved language for it's many flaws. The

responses ranged from the obvious to the absurd, but the most voted flaws (in

order) were:

- Strings
- No documentation
- Records
- Prelude with partial functions
- Ambigious space/time complexity
- No stack traces
- Language extension overload
- Long compilation times
- No IDE

There's some truth to most of these. There's also a answer or workaround to all

of them except documentation.

#### Editor & IDEs

The traditional editors saw incremental improvements and much was written about

provisioning development environments for Haskell.

- IntelliJ plugin for Haskell
- Setting Up A Haskell Development Environment (Mac OS)
- Vim and Haskell in 2016 on OS X

FP Complete released the wonderful

Intero a background process for

interacting with Emacs to do type assisted programming and completion. Plugins

were also created to integrate Intero with the Neovim

editor.

Haskell for Mac continued to develop this year

adding new tutorial content and an interactive playground for live programming

using HTML and SVG. It remains probably the simplest way to teach students using

the Macintosh operating system.

I gave a talk on editor tooling

in Boston and updated the vim

tutorial as well.

HyperHaskell was released

which provides an IPython/Mathematica style workbook for interactive Haskell

development. It is cross-platform and runs on Linux, Mac and Windows. Hyper

extends Haskell's Show mechanism to support with a `Display`

typeclass which

can be overloaded to display graphics, mathematics, diagrams or structured HTML

when rendering Haskell values to the workbook.

On a future note, industry programmers using tools like Slack, Atom, and Visual

Studio Code seem quite happy using web applications disguised in Chromium

disguised as a native application using frameworks like

Electron. Obviously this isn't a perfectly optimal

solution, but there is definitely room for an ambitious team to take the

prebuilt haskell-ide-engine, FP Complete

haskell-ide or intero backends and shape

it into an Haskell specialized IDE environment developers who like such a fully

featured environment. Perhaps the FP Complete IDE was a good idea, just a bit

early.

#### GHC

The Glorious Glasgow Haskell Compiler had it's 8.0 release, and landed to

much rejoicing. It was a big release and landed quite a few new features. It

also staged quite a bit of partial work that will be manifest in the 8.2 which

is tentatively scheduled for release candidate in mid-February 2017 and release

in mid-April 2017. The GHC core development team did some truly progressive work

this year.

**Type In Type**

Haskell's pseudo-dependent type solution `TypeInType`

landed. The initial

solution was a bit brittle and is not actively used too much in the wild.

Simply put the `TypeInType`

extension removed the distinction between types of

kind `*`

and types of other kinds.

```
λ> :set -XTypeInType
λ> import Data.Kind
λ> :info Type
type Type = * -- Defined in ‘GHC.Types’
λ> :kind Type
Type :: *
```

Richard Eisenberg finished up the work for his

thesis and

released a status report on the

efforts.

**Type Family Dependencies**

Type families historically have not been injective, i.e. they are not guaranteed

to maps distinct elements of its arguments to the same element of its result.

The syntax is similar to the multiparmater typeclass functional dependencies in

that the resulting type is uniquely determined by a set of the type families

parameters. GHC 8.0 added support for this with the `TypeFamilyDependencies`

extension.

```
type family F a b c = (result :: k) | result -> a b c
type instance F Int Char Bool = Bool
type instance F Char Bool Int = Int
type instance F Bool Int Char = Char
```

**Kind Equalities**

Up until GHC 8.0, we've not been able to express explicit kind equality proofs.

As a result, type-level computation does not have access to kind level functions

or promoted GADTs, the type-level analogues to expression-level features that

have been so useful.

For instance in Agda if we wanted to write down a type-level proof about the

commutativity of addition over the natural numbers we can do this quite simply.

We use the usual propositional equality to express the type that two things are

equal using substitutivity (`subst`

): for any proposition (type), we can

replace a term with a propositionally equal one, without changing the meaning of

the proposition. And relatedly congruence (`cong`

): if any function f respects

propositional equality, it yields propositionally equal results if applied to

propositionally equal arguments.

```
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
0 + n = n
suc m + n = suc (m + n)
infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
subst : {A : Set} → (P : A → Set) → ∀{x y} → x ≡ y → P x → P y
subst P refl p = p
cong : {A B : Set} (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
assoc : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
assoc zero _ _ = refl
assoc (suc m) n p = cong suc (assoc n p)
```

As of GHC 8.0 we now have enough to do this kind of kind-level reasoning using

propositional equality with `TypeInType`

.

```
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
-- pattern matching on Refl introduces proof
data (==) :: forall (t :: *). t -> t -> * where
Refl :: x == x
data Nat = Z | S Nat
infixl 6 +
type family (+) a b where
Z + b = b
S a + b = S (a + b)
type family Sym (eq :: (x :: a) == (y :: a)) :: y == x where
Sym Refl = Refl
type family Cong (f :: a -> b) (p :: x == y) :: f x == f y where
Cong f Refl = Refl
type family Assoc
(a :: Nat) (b :: Nat) (c :: Nat) :: (a + b + c) == ((a + b) + c)
where
Assoc Z b c = Refl
Assoc (S a) b c = Cong S (Assoc a b c)
```

**Visible Type Applications**

Visible Type Applications was added with the `-XTypeApplications`

flag to

allow the addition of explicit type arguments directly to polymorphic

call-sites. For instance:

```
show (read @Int "42")
```

**Custom Type Errors**

As of GHC 8.0 we have the capacity to provide custom type error using type

families. The messages themselves hook into GHC and expressed using the small

datatype found in `GHC.TypeLits`

.

```
data ErrorMessage where
Text :: Symbol -> ErrorMessage
ShowType :: t -> ErrorMessage
-- Put two messages next to each other
(:<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
-- Put two messages on top of each other
(:$$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
```

An example would be creating a type-safe embedded DSL that enforces invariants

about the semantics at the type-level. We've been able to do this sort of thing

using GADTs and type-families for a while but the error reporting has been

horrible. With 8.0 we can have type-families that emit useful type errors that

reflect what actually goes wrong and integrate this inside of GHC. This is going

to a *big deal* for embedded DSL design in Haskell where failures were typically

opaque and gnarly.

```
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
type family Coerce a b where
Coerce Int Int = Int
Coerce Float Float = Float
Coerce Int Float = Float
Coerce Float Int = TypeError (Text "Cannot cast to smaller type")
data Expr a where
EInt :: Int -> Expr Int
EFloat :: Float -> Expr Float
ECoerce :: Expr b -> Expr c -> Expr (Coerce b c)
foo :: Expr Int
foo = ECoerce (EFloat 3) (EInt 4)
```

**OverloadedRecordFields**

This was a source of great pain in previous releases where common identifiers

like `id`

would have to have superfluous prefixes associated with each record,

this is no longer an issue with the `OverloadedRecordFields`

extension.

```
data A = A
{ a :: Int
, b :: Double
} deriving Show
data B = B
{ a :: String
, c :: Char
} deriving Show
mkA :: A
mkA = A {a = 23, b = 42}
upA :: A -> A
upA x = x {a = 12}
sel :: A -> Int
sel = a
main :: IO ()
main = print $ sel $ upA $ mkA
```

GHC 8.0 also introduced the `OverloadedLabels`

extension which allows a

limited form of polymorphism over record selectors and updators that share the

same name.

```
class IsLabel (x :: Symbol) a where
fromLabel :: Proxy# x -> a
```

```
instance IsLabel "true" Bool where
fromLabel _ = True
instance IsLabel "false" Bool where
fromLabel _ = False
instance IsLabel "true" Int where
fromLabel _ = 1
a :: Bool
a = #false
b :: IsLabel "true" t => t
b = #true
```

```
main = do
print a
print (b :: Bool)
print (b :: Int)
```

**MonadFail**

The MonadFail Proposal finally removed the ugly `fail`

function that was

historical cruft from the 90s. A new class

`MonadFail`

was implemented along with a set of warning flags pattern matching or guard

would introduce a `fail`

occurrence.

```
class Monad m => MonadFail m where
fail :: String -> m a
```

**DeriveLift**

8.0 added yet another automatic deriving mechanism. This time we can now

automatically derive the boilerplate for TH Lift instances allowing us to embed

free variables containing `Lift`

instances inside of the Oxford brackets.

```
{-# LANGUAGE DeriveLift #-}
module Lift where
import Language.Haskell.TH.Syntax
data Expr
= Zero
| Succ Expr
deriving (Show, Lift)
```

And in a separate module:

```
{-# LANGUAGE TemplateHaskell #-}
module Exp where
import Lift
import Language.Haskell.TH.Syntax
zero :: Q Exp
zero = [|Zero|]
suc :: Expr -> Q Exp
suc x = [|Succ x|]
x :: Expr
x = $( [|Succ Zero|] )
```

**Strict Haskell**

Haskell is normally uses a call-by-need semantics such that arguments passed to

functions are only evaluated if their value is used. Bang patterns (written as

`!x`

) are explicit annotations that can force a specific to be evaluated

before entering the function instead of as needed. GHC 8.0 introduced the

ability to enable this for all functions in a specific module.

For example given the following set of definitions:

```
data T = C a
f x = y x
let x = y in rhs
case x of y -> rhs
case x of (NewType y) -> rhs
```

Enable `-XStrict`

will automatically performs the equivalent of adding

strictness annotations to the every argument source. Effectively transforming

the above into the following:

```
data T = C !a
f !x = y x
let !x = y in rhs
case x of !y -> rhs
case x of !(NewType y) -> rhs
```

Enabling will not uniformly increase the performance of code as some care is

required when enabling it. It simply makes a slightly alters the behavior to one

extreme of the space-time compromise spectrum, optimal performance still

requires a clever mix of both laziness and strictness.

**Stack Traces**

Simon Marlow cracked the perpetual stack trace

problem

allowing a variety of approaches to getting detailed stack trace

informations when we have to panic or unwind the stack.

For explicitly defined functions we can annotate call sites with a

`HasCallStack`

constraint which can be used to to obtain a partial call-stack

at any point in the program. HasCallStack is a type constraint synonym for

threading an implicit parameter `?callStack`

.

```
type HasCallStack = ?callStack :: CallStack
```

```
import GHC.Stack
f :: HasCallStack => Int -> Int
f x = error ("Error: " ++ show x)
g :: HasCallStack => Int -> Int
g = withFrozenCallStack f
main :: IO ()
main = print $ g 23
```

For automatic stack traces across the entire program in GHCi we can compile the

with a specific set of flags and profiling enabled. The precise stack trace from

the closure where assertion was called will then be printed if the term is

evaluated. Currently this introduces a 2-3x runtime overhead when compiled.

```
$ ghci -fexternal-interpreter -prof
```

**Unboxed Sum Types**

GHC 8.2 will have `UnboxedSums`

, that enables unboxed representation for

non-recursive sum types. The extension will be enabled as an opt-in annotation

with new to explicitly unpack selected datatypes for high-performance

structures.

Unboxed types are those which instead of being represented by a pointer to heap

value are passed directly in a CPU register. The usual numerics types in Haskell

can be considered to be a regular algebraic datatype with special constructor

arguments for their underlying unboxed values.

```
data Int = I# Int#
data Integer
= S# Int# -- Small integers
| J# Int# ByteArray# -- Large GMP integers
data Float = F# Float#
```

The syntax introduced allows sums to be explicitly unboxed by delimiters `(# ... #)`

. Pattern matching syntax follows the same form, and allows explicit

unpacking of the unboxed sum in case statements.

```
type Sum1 =
(#
(# Int#, Int #)
| (# Int#, Int# #)
| (# Int, Int# #)
#)
showSum1 :: Sum1 -> String
showSum1 (# p1 | | #) = showP1 p1
showSum1 (# | p2 | #) = showP2 p2
showSum1 (# | | p3 #) = showP3 p3
```

The usual ( `Maybe a`

) type was traditionally represented by a tagged closure,

with a two pointer lookups to the parameter `a`

. With unboxed sums we simply

store the pointer to the value a alongside the flag for the sum type without the

need for extra indirection. This would effectively allow a 'zero-cost

abstraction' (with full type safety) use of the Maybe monad when fully

optimized.

**Compact Regions**

Support for 'Compact Regions' is planned for GHC 8.2. Compact regions are

manually allocated regions where the data allocated inside it are compacted and

not traversed by the GC. This is amenable for long-lived data structures that

are resident in memory without mutation frequently occurring. William Sewell

gave a great talk at the

London Haskell meetup where the issues with large `Data.Map`

structures used

for a message bus system caused non-optimal GC performance

The proposed API has been

expressed as well as a paper on

the details on extensions to the GC and runtime

system.

**GHC Education**

At the beginning of the year I felt one of the larger looming issues is that GHC

internals are too opaque. However there was a lot of great writing and talks

given this year about practical examples of extending and exploring the GHC

internals.

Simon Petyon Jones gave a brilliant talk on Into the

Core, describing the System-FC core

language at the heart of all of Haskell. He also then described the new work on

the Sequent

calculus

as a compiler intermediate language for future work.

I wrote a three part blog series on the internal GHC types, pipeline, and gave

some practical tutorials on augmenting the compiler with custom logic. Work

permitting I'll try to extend this series next year with posts on CMM and RTS

internals.

Takenobu Tani published a lovely slide deck on GHC internals

illustrated.

David Luposchainsky released a STGj, a visual

STG (Spineless Tagless G-Machine) implementation to help understand Haskell's

execution model. A talk on the subject was also given at

ZuriHac.

Alberto Sade wrote a short tutorial on manipulating the GHC

Core types from inside Haskell

programs.

Christiaan Baaij wrote a detailed

tutorial on extending

the GHC typechecker with a custom plugins which allow more complex logic to be

embedded in the type system.

#### Stack

Since last year Stack has become near ubiquitous. Every company that I've come

in contact with in the last year is using it internally for their builds. The

tooling makes some compromises on version bounds and compatibility that are

'pragmatic' and actively debated, but overall the tooling has brought more

people into the language and vastly decreased a lot of the friction we once had.

The innovation of Stack can be put quite simply as making all build commands

idempotent and sandboxes as stateless, which was a vast improvement over

stateful sandboxes which would quickly become corrupted or inconsistent and

needed to be rebuilt constantly.

```
stack ghci --package protolude
```

Stack has since grown a rich set of integrations with tooling such as Nix,

GHCjs, TravisCI, CircleCI, Docker, Kubernetes as well as broad set of templates

for quickly starting

Haskell projects.

The alternative `cabal new-build`

build system is under active development.

The new build system uses Nix-style local builds which makes a distinction

between local packages and external packages. Local packages, which users edit

and recompile and must be built per-project whereas external packages are cached

across projects and retrieved from Hackage.

There will likely still be healthy debate about best practices, but despite

whatever approach converges much of the Cabal-hell problems of years past are a

distant memory. We have ubiquitous cached builds, stateless sandboxing and easy

to use-tooling.

#### Probabilistic Programming

Probabilistic domain languages are designed to describe probabilistic models by

allowing variables defined in the language to represent stochastic quantities,

and then perform inference (Markov Chain Monte-Carlo, Gibbs Sampling, etc) on

combinations of these stochastic models according to the structure of the their

combination in the program. Probabilistic programming is an exciting, and

growing, area of research, with fantastic people in both AI/ML and PL working

together and making big strides. It is especially finding uses in quantitative

finance as of late.

Jared Tobin has written some excellent

articles on the topic of

building minimalist domain languages to model probabilistic models. There's also

been several other encodings in libraries like

hakaru and monad-bayes.

#### LLVM

LLVM is a compiler toolchain and intermediate language used in most modern

compilers. Since Haskell is heavily used in compiler and language work, the LLVM

bindings are of great interest to a lot of Haskellers. This year saw quite a few

new compilers and derived work.

Roberto Castañeda Lozano released

Unison a new

Haskell library which integrates with the LLVM toolchain as an alternative or as

a complementary approach to default register allocation algorithms which are

suboptimal for embedded or low-power systems.

Moritz Angermann gave a lovely talk on using embedded DSLs in Haskell to

generate LLVM bitcode and

presented at ICFP.

I travelled to Paris and Berlin this autumn and gave a short talk on compiling

small native languages using llvm-general Haskell bindings to build a small

compiler called 'Petit'. Andreas Herrmann also gave a brilliant talk on the

subject in Zurich with a more detailed dive

through through the internals of a

simple LLVM compiler backend.

The Summer of Code sponsored work on the LLVM backend to Accelerate, one of

Haskell's array computing librarys. The work implemented

all

of the core operators and the project should be ready widespread soon.

#### Mathematics

The arithmoi number theory library found

new maintainers and is being actively developed once again.

```
> import Math.NumberTheory.Zeta
> import Math.NumberTheory.Primes.Sieve
> take 10 primes
[2,3,5,7,11,13,17,19,23,29]
> take 3 (zetas 1e-14) :: [Double]
[-0.5,Infinity,1.6449340668482262]
```

A rather popular student project this year was a implementation of the Wolfram

Language, a simple M-Expression language

based on term rewriting. The project demonstrated the obvious strength Haskell

has for modeling mathematical domain languages. There is most definitely a lot

of low-hanging fruit for building the core machinery for classic computer

algebra problems. A basic implementation of the following would go quite far

toward advancing Haskell in computational algebra:

*Gröbner basis*calculation for solving systems of polynomials in commutative algebras.*Normal-Risch algorithm*for symbolic integration.*Strong Generating Sets/Coset*algorithms for tensor index canonicalization.*Horner scheme*for evaluation of univariate polynomials over arbitrary domains.

#### Cryptography

Due to commercial investment, cryptography libraries in Haskell have gotten much

more mature this year. We have a complete complement of the industry standard

algorithms for various tasks:

- Poly1305 for message authentication codes.
- Blake2b or Keccak-256 for hashing.
- Scrypt or Argon2 for password key derivation.
- Chacha20-256 for symmetric key encryption.
- Curve25519 for elliptic curve public key cryptography.

Also a friendly reminder that the NSA has likely developed the capability to

decrypt a large number of HTTPS, SSH, and VPN connections using an attack on

common primes used in the parameters of the Diffie-Hellman key exchange

algorithm with keys less than 2048 bits. Some estimates also put decryption with

the D-Wave computers within 10 years which poses a threat to current

cryptographic approaches based on the discrete-logarithm problem in finite fields

and elliptic curves. Be safe as we go into uncertain territory in 2017.

At ICFP there was a fascinating

presentation on interesting work

on implementing somewhat homomorphic encryption

(SHE) and lattice cryptography

in Haskell.

#### Committees

The Haskell 2020 committee formed with the goal of forming a new language report

that GHC 8.8 would implement. There is a mailing list for haskell

prime as well as several RFC

projects on Github to track the progress. The GHC project also started tracking

proposal discussion on Github using pull requests in a more public

forum.

The DataHaskell github organization was formed

with the stated goal of improving the environment for data science in Haskell.

It has since become an incubator for several ambitious projects to advance the

state of numerical computing libraries and documentation.

#### Serialization

Well-Typed and FPComplete both released two binary serialization libraries.

Both are high performance serialization libraries with different encodings,

endianness choices and performance characteristics, especially around fixed-size

vectors and traversals times of input types.

#### HalVM

Development on HalVM out of Galois picked up with some public statements on

project. HalVM is a framework for writing Haskell programs that run lightweight

virtual machines run directly on the Xen hypervisor. This potentially opens up

the opportunity for deploying "containers" that are single purpose programs with

minimal exposure to the usual baggage Linux operating system carry and their

potential exploits.

Tooling was also published to deploy these Unikernels to standard Amazon EC2

infrastructure. See: ec2-unikernel

#### Languages

Los Alamos National Laboratory released an interesting

auto-parallelizing Haskell

subset called APPFL.

microML is a simple functional programming

language designed for teaching at University College of London for the BBC

micro:bit microcomputer.

Fugue developed an internal language called Fugue which is

used for automating cloud deployments. The technology was demoed at ICFP

talk this year.

Summer of Code sponsored work on a "blocky"

interface for composing Haskell programmers, used

for teaching basic functional programming.

Swift Navigation released Plover, an

embedded Haskell DSL for compiling linear algebra routines into C for running on

embedded systems.

Daan Leijen continued development on Koka

an experiment in effect typing using row polymorphism.

The Corrode project was introduced

which provided a semantics-preserving automatic translation tool from C to Rust,

for migrating legacy code. Using Haskell to remove legacy C code from this world

can only be a good thing.

Paul Chiusano continued development on

Unison a 'next

generation programming platform' implemented in Haskell and designed for

building large-scale distributed systems.

Gabriel Gonzalez released

Dhall,

a total non-Turing complete programming language specialized for configuration

files. Including a standard library hosted on permanent web

IPFS

node.

#### Prelude

The single largest reported pain point for the Haskell language is simply from

certain "naughty" historical things in the Prelude which no longer reflect

modern thinking. The default Prelude makes it much too accidentally shoot oneself

in the foot by using suboptimal String types, partial functions, impure

exception throwing, and a variety of other paper cuts.

Earlier this year I released my perspective on the issue:

Protolude. Protolude is likely the least

ambitious alt-prelude ever. It doesn't do anyting new, just fixes Base exports

with the legacy bits masked and much of the mental overload of String

conversions smoothed over. Notably it maintains ABI compatibility with existing

Haskell code. Judging by the number of uses of Github it seems well-received and

is being used in the core of major projects like PostgREST and Purescript.

There are plenty of other approaches to prelude

design and I believe the

explosion is a healthy reaction to a standard library which many users consider

not suitable for industrial use. No one prelude will be suitable for everyone

for all use cases. The two concerning factors to keep in mind when exploring

this space are:

- Keep the transitive dependency tree small.
- Maintain compatibility with base whenever possible.

For a new projects in 2017, consider just starting with `NoImplicitPrelude`

in your cabal file and importing a sensible set of defaults from your library

of choice.

```
default-extensions:
NoImplicitPrelude
```

Or use a stack template like:

```
$ stack new protolude
```

#### Foundation

Alternate preludes are only routing around the problem because of the

constraints of being unable to fix problems upstream. The Foundation library is a bit grander in scope and

aims to fix quite a few of the overarching problems with the ecosystem.

- UTF8 based strings are default and are stored as packed array of codepoints.
- FilePath are algebraic datatypes and can be manipulated and inspected without

string munging. - IO actions read into ByteStrings and conversion into the appropriate type is

left to the user. - Partial functions are either removed or wrapped in a
`Partial`

monad.

Non-empty datatypes are provided by default. - An abstract container interface is provided that allows multiple data

structures (Set, Map, Vector, etc) to use the same functions overloaded by a

type class with associated data families to track elements or index types. - More granular numerical tower that doesn't require partial implementations of

functions that aren't relevant.

For a quick taste:

```
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoImplicitPrelude #-}
import Foundation
import Foundation.IO
import Foundation.String
import Foundation.VFS.FilePath
import Foundation.Collection
example :: String
example = "Violence is the last refuge of the incompetent."
bytes :: UArray Word8
bytes = toBytes UTF8 example
file :: IO (UArray Word8)
file = readFile "foundation.hs"
fileString :: IO (String, Maybe ValidationFailure, UArray Word8)
fileString = fromBytes UTF8 <$> file
xs :: NonEmpty [Int]
xs = fromList [1,2,3]
x :: Int
x = head xs
```

I'm not aware anyone currently using this library, but it most certainly

something to watch as it matures in 2017. It might be the "new hope" we've been

looking for which consolidates industrial Haskell best practices.

#### Generics

Generics in 8.0 extended the generics structure to include a richer set of

queryable data. We now have full access to the lifted status, strictness

annotations, datatype names, selector names, constructors, and newtype status of

all symbols in a Generic instance.

The implementation of `DeriveAnyClass`

pragma has also allowed classes which

provide fully default signatures to automatically derived without empty instance

declarations. Aeson for instance can now automatically derive JSON serializes

and de serializes for any instance of Generic for free.

```
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
import Data.Text
import Data.Aeson
data Sample = Sample
{ a :: Text
, b :: Text
} deriving (Show,Generic,FromJSON,ToJSON)
-- decode { "a": "foo", "b": "bar" } :: Sample
```

Libraries like `optparse-generic`

have implemented prototypes of building

entire command line interfaces using generics on top of vanilla Haskell data

structures.

Andres Löh gave an hour long lecture on the new approach of using generic

sums-of-products with generics-sop at ZuriHac

2016.

I wrote a short blog post

amount implementing custom generics functionality and how the internals of

Generic deriving works.

Ryan Scott wrote a detailed blog post detailing all of the substantial

changes

in GHC 8.2 and changes to metadata format.

#### Idris

Idris is a pure functional language with full dependent types, and is itself

written in Haskell. Idris is not likely to be the tool I'll reach for most of my

day-to-day work, but it's maturing quite rapidly and pushing the envelope of

practicality in dependent types more so than any other language. It was

announced that Idris is heading toward a 1.0

milestone.

There is also initial work on a Java Virtual Machine

backend to Idris to supplement the

builtin native code generator and Javascript backends.

There is also work on porting Benjamin Pierce's seminal work 'Software

Foundations' into Idris.

Most notably 0.9 introduced elaboration reflection using Idris as its own

metalanguage. To explain, Idris is type checked in two stages: first, a

metaprogram known as an elaborator translates the surface language into a small

core language (called TT), after which the resulting TT program is type checked

. Incomplete programs can be introduced as holes, which in the context of the

rest of the program, have a set of unification constraints to be solved.

Elaboration allows us to 'script' the automatic completion of these holes with

reusable logic that can access the full typing environment. This used to exist

in a dedicated tactic system (ala Coq)

but now these tactics can themselves be expressed using the elaborators

reflection in Idris itself using a small set of monadic combinators.

```
-- Convert a hole to make it suitable for bindings
attack : Elab ()
-- Introduce a lambda binding around the current hole and focus on the body
intro : (n : TTName) -> Elab ()
-- Place a term into a hole, unifying its type.
fill : Raw -> Elab ()
-- Substitute a guess into a hole.
solve : Elab ()
```

For example to elaborate a polymorphic identity function:

```
mkId : Elab ()
mkId = do
x <- gensym "x"
attack
intro x
fill (Var x); solve
solve
idNat : Nat -> Nat
idNat = %runElab mkId
```

The latest version now ships with a standard library of proof tactics called

Pruviloj

that work with Idris's elaborator. For example we can automate induction proofs

to prove associativity of numerical operations.

```
import Pruviloj
auto : Elab ()
auto = do
compute
attack
try intros
hs <- map fst <$> getEnv
for_ hs $ \ih => try (rewriteWith (Var ih))
hypothesis <|> search
solve
ind : Elab ()
ind = do
attack
n <- gensym "x"
intro n
try intros
ignore $ induction (Var n) `andThen` auto
solve
assoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
assoc = %runElab ind
```

Will then automatically fill in the term:

```
assoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
assoc Z k l = Refl
assoc (S j) k l = let rec = assoc j k l in rewrite rec in Refl
```

#### Agda

Agda is the most mature dependently typed functional programming language, and

is itself written in Haskell. It is regularly used for research and for build

complex type-level constructions to extract into Haskell.

Agda actually has quite lovely documentation

now and is far more approachable than

5-6 years ago. There was recently a full course entitled Agda from Nothing

(video,

source) by which walks

one Scott Fleischman through the basics of dependently typed programming from

first principles. It's never been easier to learn.

#### Javascript

Javascript unfortunately continues to exist. While I remain skeptical of the

entire transpiling phenomenon and think it will lead to an endless amount of

wasted person-hours and legacy code. However the pragmatist in me also knows

that the browser vendors are not economically incentivized to change the status

quo, so nothing will change quickly and we should adapt ourselves to the least

worst solution.

Last year I said I would revisit Elm if anything changed. Nothing has changed.

It's as uninteresting a language as it was last year. It's 2017, languages

should have a coherent story for polymorphism that doesn't involve manual code

duplication. I remain unconvinced by arguments attempting to reframe 'primitive'

technology as 'simple'.

Purescript on the other hand is increasingly becoming a more mature and robust

language fully grounded in modern ideas. There was a lovely book

written this year as well as variety of

language improvements like newtype deriving, generics, type directed search,

source maps, better error reporting, and custom package manager.

The Purescript community developed

Halogen

which is a a toolkit for building reactive web apps using signal functions and

a virtual DOM. It exposes a set of combinator for acting on signals which vary

over time and dispatch to DOM event changes. This provides a proposal to the

current trend of React/Redux-style application construction.

The GHCjs solutuion has gotten more mature and stable, and integrated with the

Stack ecosystem. There were some impressive demos on compiling the entirety of

Pandoc into Javascript, which is quite a feat of

engineering. Nevertheless, I remain somewhat skeptical that compiling Haskell to

enormous blobs of auto-generated Javascript that contain the entire Haskell

runtime is a sustainable solution for large commercial codebases. With

WebAssembly on the horizon I might be convinced otherwise in 2017.

#### Eta

Eta is a Java Virtual Machine Backend for GHC

7.10. The stated goal of the project is to compile the entirety of Haskell to

run with full core library and concurrent runtime support. The first release is

estimated in January of 2017. The codebase is under active development by Rahul

Muttineni and taking contributions.

Most notably the library will first class support for integrating with existing

Java libraries through FFI, much like we do with C today.

```
import Java
data {-# CLASS "java.util.List" #-} List a = List (Object# (List a))
deriving Class
foreign import java unsafe "@new" newArrayList :: Java c (ArrayList a)
```

#### Formal Verification

Haskell continues to find use in verification and auditing of cryptography.

Although not new developments, both the Galois Cryptol library and Tamarin

Prover (both Haskell-based tools) are being used for industrial strength uses in

high-assurance work. Haskell continues to have best in class integration with

external solvers such as Z3 and CVC4.

The National Science Foundation is currently funding work out of University of

Pennsylvania and MIT to build an entire ecosystem of language tools that have

end-to-end correctness proofs called DeepSpec. The

CoreSpec program aims to develop a

formal Coq specification of the GHC Core Language, type system, and semantics.

The Lean theorem prove recently added a complete Homotopy Type

Theory library

with a complete mapping of the

chapters from the

textbook.

#### Liquid Haskell

Refinement types allow us to enrich Haskell's type system with predicates that

precisely describe the sets of valid inputs and outputs of functions These

predicates are compiled down into a specific core language which can be

discharged to an SMT solver for which there are fast decision procedures for

testing the validity of the type.

For example we can construct refinements over a `Int`

variable `v`

.

```
{-@ type Zero = {v:Int | v == 0} @-}
{-@ type NonZero = {v:Int | v /= 0} @-}
```

And constrain our function definitions so that the functions carry around a

proof that a non-zero term will not be passed to it.

```
{-@ zero :: Zero @-}
zero = 0 :: Int
{-@ one, two, three :: NonZero @-}
one = 1 :: Int
two = 2 :: Int
three = 3 :: Int
```

We can combine these predicates to prove non-trivial properties about arithmetic

relations, properties about data structures and pointer memory

access

to prevent bugs like Heartbleed.

```
import Prelude hiding (mod, gcd)
{-@ mod :: a:Nat -> b:{v:Nat| 0 < v} -> {v:Nat | v < b} @-}
mod :: Int -> Int -> Int
mod a b
| a < b = a
| otherwise = mod (a - b) b
{-@ gcd :: a:Nat -> b:{v:Nat | v < a} -> Int @-}
gcd :: Int -> Int -> Int
gcd a 0 = a
gcd a b = gcd b (a `mod` b)
```

LiquidHaskell has developed a lovely and approachable set of documentation

this year, and is now quite usable in production.

#### Linear Types

Intuitively linear types model finite resources by a notion of *consumption* of

variables in scope. A linear variable needs to be consumed in the same concept

it was introduced and can not be "duplicated" or "destroyed". In a linear

λ-calculus we have typing rules in which statements such as “this function will

use its argument exactly once” can be checked which can be used to enforce

invariants on resource usage such as memory, channels, sockets, tokens, file

descriptors, etc.

At the Haskell Exchange and ICFP there was some very early discussion about the

possibility of introducing linear types into GHC. The proposed addition would

allow weight inference and annotations to variables allowing users to constrain

variable usage. The proposal and semantics are being actively discussed on the

issue tracker.

An implementation likely remains in the far future.

An undergraduate project at Chalmers presented a simple prototype Haskell-like

language Lollipop using linear typing.

Jeff Polokow presented a construction

by which a full linear lambda calculus can be deeply embedded in the current

type system using advanced type features.

#### Backpack

Backpack is Haskell's partial answer to "module problem", of having

cross-package libraries which are currently duplicated to provide similar

interfaces. Backpack will allow libraries which are parametrized by signatures,

letting users decide how to instantiate them at a later point in time.

This work is still very early, but Edward Yang gave a insightful talk at NYC

Haksell Meetup on the current

design decisions taken in the prototype implementation. There is also a thorough

description of the applications of Backpack to solve the problem of reusable

string

libraries

that work over different underlying string representations.

In the early prototype we can construct an abstract `Str`

signature module

which provides a set of types:

```
signature Str where
data Str
data Elem
instance Eq Str
instance Ord Str
instance Show Str
instance Monoid Str
empty :: Str
length :: Str -> Int
```

This is then exposed in the cabal file for the library in the `signatures`

field.

```
name: str-sig-major1
library
signatures: Str
build-depends: base >= 4.9 && < 4.10,
deepseq
default-language: Haskell2010
```

An implementation of this signature then imports then library, and can then be

implement the interface downstream by using a `mixin`

.

```
name: str-text
library
mixins:
str-text (Str.Text as Str)
build-depends:
base,
str-sig-major1
```

The concrete implementation of the module would look like the following:

```
module Str.Text (
Str,
Elem,
empty,
length,
) where
import qualified Data.Text as T
type Str = T.Text
type Elem = Char
empty :: Str
empty = T.empty
length :: Str -> Int
length = T.empty
```

The work is still early, so this precise form may or may not end up in the final

release of Backpack.

#### Databases

Earlier this year I commented that compromises in type-safe database libraries

consisted of the following traedoffs:

Haskell SQL libraries: endless boilerplate, opaque metaprogramming, or wall of

15 language exts and no inference. Pick two.

A lot of industrial Haskell sadly still uses string interpolation for SQL

synthesis, or fall back on libraries that use TemplateHaskell to unsafely lock a

specific build to a snapshot of a database at compile-time. Both of these

trade-offs are suboptimal and fall short of what we can do in other robust

frameworks like SQLAlchemy in Python. There's three different key points that

need to be addressed:

- Definition of a schema tied to a specific databases and migration handling

that can done at runtime. - Consistency checking of schema against definitions of SQL statements with

type-safety. - Composition and reuse of units of SQL statements and values that preserve

type safety under composition.

The challenge I continue to pose, that occurs quite frequently in data

warehousing and ETL, is given a dynamic (i.e. at runtime) specification of a

table in some embedding of DDL: create a table, query it, and dump the results

into an existing table of the same schema. Doing this in a safe manor requires a

rather complex reflection

framework by which a

table object can load the `information_schema`

and check the constancy of the

query before evaluation.

I don't think the ideal library is quite there yet, but year I was most

impressed by Jake Wheat's very early

`hssqlppp`

which implements a

restricted domain language for modeling and typechecking a Postgres SQL subset

and generating queries. The full integration with a runtime SQL type-checker is

a lovely piece of

work and it

would be follow naturally to lift this into a type-safe quasiquoter which would

give the ideal solution of unifying both the dynamic and static semantics of SQL

program synthesis at runtime and compile-time.

#### Industrial Users

Facebook quietly retains and recruits some of the legendary-level Haskell

talent. See: Haskell in the Datacentre

Barclay's in the UK is also quietly building up an impressive team. See: Full-time

Haskell jobs in London, at Barclays

JP Morgan funded development on a transaction modeling language

Hopper.

Ambiata presented at ICFP this year about a new query language

Icicle for streaming time series, with a

novel approach to fusion

and released source code.

Awake Networks is building a next generation network security and analytics

platform, utilizing using Purescript and Haskell.

Google has been pushing out Haskell bindings to some of their core

infastructure, including Tensorflow. See: Haskell

Tensorflow

There's a fairly large group of Haskellers very quietly working on building

smart contract solutions based on functional programming and formal methods. A

lot of is happening behind doors at banks but some truly amazing work is being

done in this space by singularly talented people. Watch for some amazing

future-tech to drop in 2017.

Lots of exciting things going on at Barclay's, Facebook, Target, Ambiata, Tweag,

Takt, Zalora, Galois, JP Morgan, Helium, Silk, Lumi Guide, Awake Networks,

FrontRow, Clearmatics, Standard Chartered, Digital Asset Holdings and Microsoft.

#### Stephen

Since last year I've been criss-crossing the globe through Germany, London,

Paris, San Francisco, Zurich, Portland, New York and Boston doing some mix of

advising, consulting, and investments. Late this year, I finally ended up

starting a new company, which I'll speak about publicly in the next few

months.

I'm especially grateful for the warmth and kindness I felt traveling across

European programming scene. I consistently always had a friend in whatever city

I visited and it's been a pleasure meeting many of you. Wish you all Merry

Christmas and a Functional New Year!