<commit_before>---
title: Interpreting Haskell Inside PostgreSQL With Singleton Types
---

I am currently in the early stages of a new project,
[`plhaskell`](http://github.com/ocharles/plhaskell). `plhaskell` is a
[language handler](http://www.postgresql.org/docs/current/static/sql-createlanguage.html)
for PostgreSQL that will allow you to write PostgreSQL functions in Haskell. The
project has already taught me a lot, but recently I've had a somewhat mind
bending encounter with what is almost dependently typed programming in Haskell -
and I've just got to share it with you.

Here's the problem. At runtime, we have a string containing Haskell code,
metadata about the function call which includes the function signature, and a
list of argument values. Is it possible to interpret this string as a Haskell
function and call it with the provided arguments?

Let's start by interpreting the string. The `hint` library provides a high-level
interface to GHC's API, which allows us to interpret strings as values of a
given Haskell type. The most useful function for us is:

```haskell
interpret :: Typeable a => String -> a -> m a
```

Given a `String` containing Haskell code and an expected type, `interpret` will
attempt to construct a value of that type by interpreting the given string. We
can run the interpreter using `runInterpreter`. For example:

```
> runInterpreter $ setImports ["Prelude"] >> interpret "True" (as :: Bool)
Right True

> runInterpreter $ setImports ["Prelude"] >> interpret "True" (as :: Int)
Left (WontCompile [GhcError {errMsg = "
Couldn't match expected type `GHC.Types.Int'
            with actual type `GHC.Types.Bool'"}])
```

We're making good progress, but now we hit a problem. Notice that we are
deciding the type that `interpret` should return statically, at compile
time. The problem statement above indicates that the type information isn't
known at compile time, we only learn about that at runtime. At first this seems
impossible - after all, Haskell is all about static types!

The dependent types crowd are laughing at this point. Surely we just want to
write a function with this type:

```haskell
interpret :: String -> (sig : Signature) -> (FunctionType sig)
```

Alas, we can't write this in Haskell. Or can we?

## A Type of Types

A good first step is to clear up what we mean by "types". PostgreSQL has an open
universe of types, as types can be defined at runtime. However, we'll keep
things a little simpler by considering a closed universe of the following types:

```haskell
data PgType = PgInt | PgString
```

Combining GHC's new(ish) abilities to promote data types along with type
families, we can form a mapping from PostgreSQL types to Haskell types:

```haskell
type family InterpretType (t :: PgType) :: *
type instance InterpretType 'PgInt = Int
type instance InterpretType 'PgString = String
```

The type family takes types of kind `PgType` to types of kind `*` - the kind of
types of Haskell values. It's important to remember that this is all at the type
level - we transform the *type* `PgInt` to the *type* `String`. Working at the
type level is not enough to solve the overarching problem, because runtime
information is at the value level. In order to link types and values, we can use
*singleton types*.

Intermediate Haskell programmers should be familiar with phantom types - type
variables whose sole purpose is to carry type information. Singleton types work
in a similar way - we add a type parameter to carry information up from values
to their types. For `PgType`, there is a corresponding singleton type:

```haskell
data SPgType :: PgType -> * where
  SPgInt :: SPgType 'PgInt
  SPgString :: SPgType 'PgString
```

By using a GADT, we can now learn more information about our types by pattern
matching. For example, we can write a function who's return type depends on the
value of the first parameter:

```haskell
exampleValues :: SPgType t -> InterpretType t
exampleValues SPgInt = 42
exampleValues SPgString = "Forty two"
```

At first glance this looks like nonsense, but you should take time to convince
yourself that it makes sense. If you give `exampleValues` a `SPgInt`, then by
pattern matching on that we learn that the `t` in the type signature is actually
a `'PgInt`. The type family `InterpretType` maps `PgInt` to `Int`, thus 42
is a perfectly valid return type. Similar reasoning shows that `"Forty two"` is<commit_msg>Typo correction for pl/haskell article<commit_after>---
title: Interpreting Haskell Inside PostgreSQL With Singleton Types
---

I am currently in the early stages of a new project,
[`plhaskell`](http://github.com/ocharles/plhaskell). `plhaskell` is a
[language handler](http://www.postgresql.org/docs/current/static/sql-createlanguage.html)
for PostgreSQL that will allow you to write PostgreSQL functions in Haskell. The
project has already taught me a lot, but recently I've had a somewhat mind
bending encounter with what is almost dependently typed programming in Haskell -
and I've just got to share it with you.

Here's the problem. At runtime, we have a string containing Haskell code,
metadata about the function call which includes the function signature, and a
list of argument values. Is it possible to interpret this string as a Haskell
function and call it with the provided arguments?

Let's start by interpreting the string. The `hint` library provides a high-level
interface to GHC's API, which allows us to interpret strings as values of a
given Haskell type. The most useful function for us is:

```haskell
interpret :: Typeable a => String -> a -> m a
```

Given a `String` containing Haskell code and an expected type, `interpret` will
attempt to construct a value of that type by interpreting the given string. We
can run the interpreter using `runInterpreter`. For example:

```
> runInterpreter $ setImports ["Prelude"] >> interpret "True" (as :: Bool)
Right True

> runInterpreter $ setImports ["Prelude"] >> interpret "True" (as :: Int)
Left (WontCompile [GhcError {errMsg = "
Couldn't match expected type `GHC.Types.Int'
            with actual type `GHC.Types.Bool'"}])
```

We're making good progress, but now we hit a problem. Notice that we are
deciding the type that `interpret` should return statically, at compile
time. The problem statement above indicates that the type information isn't
known at compile time, we only learn about that at runtime. At first this seems
impossible - after all, Haskell is all about static types!

The dependent types crowd are laughing at this point. Surely we just want to
write a function with this type:

```haskell
interpret :: String -> (sig : Signature) -> (FunctionType sig)
```

Alas, we can't write this in Haskell. Or can we?

## A Type of Types

A good first step is to clear up what we mean by "types". PostgreSQL has an open
universe of types, as types can be defined at runtime. However, we'll keep
things a little simpler by considering a closed universe of the following types:

```haskell
data PgType = PgInt | PgString
```

Combining GHC's new(ish) abilities to promote data types along with type
families, we can form a mapping from PostgreSQL types to Haskell types:

```haskell
type family InterpretType (t :: PgType) :: *
type instance InterpretType 'PgInt = Int
type instance InterpretType 'PgString = String
```

The type family takes types of kind `PgType` to types of kind `*` - the kind of
types of Haskell values. It's important to remember that this is all at the type
level - we transform the *type* `PgInt` to the *type* `Int`. Working at the
type level is not enough to solve the overarching problem, because runtime
information is at the value level. In order to link types and values, we can use
*singleton types*.

Intermediate Haskell programmers should be familiar with phantom types - type
variables whose sole purpose is to carry type information. Singleton types work
in a similar way - we add a type parameter to carry information up from values
to their types. For `PgType`, there is a corresponding singleton type:

```haskell
data SPgType :: PgType -> * where
  SPgInt :: SPgType 'PgInt
  SPgString :: SPgType 'PgString
```

By using a GADT, we can now learn more information about our types by pattern
matching. For example, we can write a function who's return type depends on the
value of the first parameter:

```haskell
exampleValues :: SPgType t -> InterpretType t
exampleValues SPgInt = 42
exampleValues SPgString = "Forty two"
```

At first glance this looks like nonsense, but you should take time to convince
yourself that it makes sense. If you give `exampleValues` a `SPgInt`, then by
pattern matching on that we learn that the `t` in the type signature is actually
a `'PgInt`. The type family `InterpretType` maps `PgInt` to `Int`, thus 42
is a perfectly valid return type. Similar reasoning shows that `"Forty two"` is
{'fraction_non_alphanumeric': 0.0696231099074701, 'fraction_numerical': 0.0009027307605506658, 'mean_word_length': 4.444103194103194, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5520074', 'n_tokens_mistral': 2504, 'n_tokens_neox': 2326, 'n_words': 1321}