GHC is awesome. It actually implements not one, but two¹ programming languages. The Haskell type system (with some extensions) allows arbitrary computation. From now on I will refer to that Haskell subset as Type level Haskell, or TLH.

There were several attempts to make use of this beast², but writing complete programs in it is remarkably difficult due to lack of built-in IO facilities. In this post I will demonstrate how to write a simple command line program which reads lines from standard input and writes lines to standard output.

Note: most of this post is boring, you can skip to the meat.

The language

We will use type families. Multi parameter type classes with functional dependencies also offer the functionality we need, but with ugly syntax.

Since the term-level functionality of Haskell is no longer relevant to us, we can redefine some names to avoid (or create?) confusion:

• TLH values are Haskell types.
• TLH types are Haskell kinds. Kinds are types in GHC8, but the compiler sometimes still refers to them as kinds.
• TLH functions are Haskell type families.

The IO library

First, we need a way to represent the data we will be reading and writing. TLH has a built-in type Symbol with convenient syntax:

λ> :set -XDataKinds 
λ> :kind "hello"
"hello" :: GHC.Types.Symbol

At first glance it seems an excellent choice, but it has one problem: it’s completely opaque. We can’t take a substring of a Symbol, or concatenate two Symbols.

To allow arbitrary manipulation (writing a parser, for example), we will represent strings as lists of numeric values of bytes.

type Bytes = [Nat]

For example, '[104,101,108,108,111] is our representation of the string "hello".

λ> type Hello = '[104,101,108,108,111]
λ> :kind Hello
Hello :: [GHC.Types.Nat]

As a bonus, since debugging this will involve deciphering ASCII from raw numbers, using this representation will make us feel more like old-school assembly hackers reading raw memory values. Now that’s “close to the metal”!

Now we should define the type of programs. A program is an action paired with a continuation, defining what to do next. In Haskell, this would be as simple as:

data IO = Exit | Write Bytes IO | Read (Bytes -> IO)

This is similar to a free monad approach, but simpler (the computations don’t produce values).

For example, here is a program that writes “hello” and exits (in Haskell):

hello = [104,101,108,108,111]
helloProgram = Write hello Exit

Not interesting. Here is another, that prompts the user for his name and replies with a greeting:

-- "Enter your name:"
prompt = [69,110,116,101,114,32,121,111,117,114,32,110,97,109,101,58]
-- "Hello, "
hello = [72,101,108,108,111,44,32]
-- "!"
exclamation = [33]

helloProgram2 = Write prompt
  $             Read
  $ \name ->    Write (hello ++ name ++ exclamation)
  $             Exit

This program, however, can’t be directly translated into TLH, as is contains a lambda, and we don’t have such facilities in TLH. We have to extract it into its own function:

helloProgram2   = Write prompt
                $ Read
                $ handleName

handleName name = Write (hello ++ name ++ exclamation)
                $ Exit

But that still doesn’t translate into TLH, because it contains a partial function application, and Haskell doesn’t allow partial application of type families. Luckily, there’s this one weird trick called defunctionalization, which lets you transform a program that uses partially applied functions to one that doesn’t. The above program is not a good demonstration of the technique, so I will not explain it there; for reference, go to ³. To make use of it, we have to alter our definition of IO a bit:

data IO = Exit | Write Bytes IO | Read Cont
-- where Cont is defined in the program

Our final program (still in Haskell) looks like this:

data Cont = HandleName

helloProgram2         = Write prompt
                      $ Read
                      $ HandleName

apply HandleName name = Write (hello ++ name ++ exclamation)
                      $ Exit

Hello John Smith in TLH

We’re ready to translate our silly application into TLH:

{-# LANGUAGE DataKinds, TypeOperators, TypeInType, TypeFamilies, UndecidableInstances #-}
module Hello where

import Prelude hiding (Read, IO)
import GHC.TypeLits (Nat)

-- the IO library
type Bytes = [Nat]
data IO = Exit | Write Bytes IO | Read Cont

-- The program

-- "Enter your name:"
type Prompt = '[69,110,116,101,114,32,121,111,117,114,32,110,97,109,101,58]
-- "Hello, "
type Hello = '[72,101,108,108,111,44,32]
-- "!"
type Exclamation = '[33]

data Cont = HandleName

type Main                   = Write Prompt
                            $ Read
                            $ HandleName
type family Apply f x where
      Apply HandleName name = Write (Hello ++ name ++ Exclamation)
                            $ Exit

For this to work, we need to port some utilities from plain Haskell:

type family f $ x where f $ x = f x
infixr 0 $

type family xs ++ ys where
    '[] ++ ys = ys
    (x ': xs) ++ ys = x ': (xs ++ ys)

The interpreter

We don’t yet have a runtime that could execute the program, so we will do it manually (only the IO part - all computations will be done by TLH interpreter, also known as GHCi). To evaluate TLH expressions we will use a rather obscure command of GHCi, :kind!. From :help:

:kind[!] <type>             show the kind of <type>
                            (!: also print the normalised type)

It turns out that “normalisation” doesn’t always involve expanding type synonyms:

λ> :kind! Prompt
Prompt :: [Nat]
=  rompt

The workaround is:

type family Force x where Force x = x

-- evaluate the argument to Write, for convenience
type Write b = 'Write (Force b)

So our evaluation command is :kind! Force (<expr>).

Running it

λ> :kind! Force Main
Force Main :: IO
= 'Write
    '[69, 110, 116, 101, 114, 32, 121, 111, 117, 114, 32, 110, 97, 109,
      101, 58]
    ('Read 'HandleName)

This tells us to output the string '[69, 110, 116, 101, 114, 32, 121, 111, 117, 114, 32, 110, 97, 109, 101, 58], which is "Enter your name:". Good!

The next step is 'Read 'HandleName. Suppose the user entered "John Smith" ('[74,111,104,110,32,83,109,105,116,104]):

λ> :kind! Apply 'HandleName '[74,111,104,110,32,83,109,105,116,104]
Apply 'HandleName '[74,111,104,110,32,83,109,105,116,104] :: IO
= 'Write
    '[72, 101, 108, 108, 111, 44, 32, 74, 111, 104, 110, 32, 83, 109,
      105, 116, 104, 33]
    'Exit

The output is "Hello, John Smith!", and next step is to end the program.

Here’s full transcript of our interaction with the program:

Enter your name:
John Smith
Hello, John Smith!

Works as expected. Success!

Runtime

This was tedious, so I hacked up a program that does the above steps automatically, using the excellent hint library. It’s ugly, but it works. Here’s the repository: https://github.com/zyla/tlh-hello-world. You can use it to experiment with your own TLH programs.

Conclusions

Type level computation facilities in Haskell can certainly be used to write useful programs. Nothing prevents us from doing iteration (via recursion), or branching (via pattern matching in type families).