Ephemeral Purely Functional Data Structure and Linear Type
Tags: haskell
Published: 2020-12-28 16:13:39

The Japanese version is at [はてなブログ](https://kakkun61.hatenablog.com/entry/2020/12/25/%E5%88%B9%E9%82%A3%E7%9A%84%E7%B4%94%E7%B2%8B%E9%96%A2%E6%95%B0%E7%9A%84%E3%83%87%E3%83%BC%E3%82%BF%E6%A7%8B%E9%80%A0%E3%81%A8%E7%B7%9A%E5%BD%A2%E5%9E%8B).

----

Chapter 5.2 of “[Purely Functional Data Structures](https://www.cambridge.org/core/books/purely-functional-data-structures/0409255DA1B48FA731859AC72E34D494)” (PFDS) explains an ephemeral purely functional queue.

This queue has a constraint that you can operate just once for each value because of its computational complexity. For example, the first following operations are accepted, but the second may take a long time.

```haskell
-- a good example
ops =
  let
    q0 = empty
    q1 = enqueue 0 q0
    q2 = enqueue 1 q1
    Just (a, _) = dequeue q2
  in
    a
```

```haskell
-- a bad example
ops =
  let
    q0 = empty
    q1 = enqueue 0 q0
    q2 = enqueue 1 q1
    q2' = enqueue 2 q1 -- q1 is used twice
    Just (a, _) = dequeue q2
    Just (b, _) = dequeue q2'
  in
    (a, b)
```

The theme of this article is that linear types can save this constraint.

# Used versions

- [GHC 9.0.1 alpha 1 (9.0.0.20200925)](https://mail.haskell.org/pipermail/ghc-devs/2020-September/019286.html)
  - A linear arrow is `(#->)`, not `(%1 ->)`
- [linear-base 341007891ae77959ac7b147f008e3a1d9c46e96b](https://github.com/tweag/linear-base/tree/341007891ae77959ac7b147f008e3a1d9c46e96b)

# Implementation

I implemented it with the continuation-passing style (CPS) because the GHC adopts linear arrows as linear types. For instance, `empty` has the following type.

```haskell
empty :: (Queue a #-> b) #-> b
```

Its continuation has `Queue a #-> b` type and so a value of `Queue a` type is used only once in this function.

I implemented others too. Please refer to the PFDS for these computational complexities.

```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE Strict #-}

data Queue a where
  Queue :: [a] -> [a] -> Queue a
  deriving (Show)

empty :: (Queue a #-> b) #-> b
empty k = k (Queue [] [])

null :: Queue a #-> ((Bool, Queue a) #-> b) #-> b
null (Queue l m) k = k (P.null l, Queue l m)

enqueue :: a -> Queue a #-> (Queue a #-> b) #-> b
enqueue a (Queue l m) k = k (check l (a:m))

dequeue :: Queue a #-> (Maybe (a, Queue a) #-> b) #-> b
dequeue (Queue (a:l) m) k = k (Just (a, check l m))
dequeue (Queue _ _) k = k Nothing

check :: [a] -> [a] -> Queue a
check [] m = Queue (reverse m) []
check l m = Queue l m
```

The reason for using GADT is to implement functions like `null`. If not using GADT, the linearity was required for `l` and `m` of `Queue l m` recursively and so `l` cannot be used twice.

This implementation has one inconvenient stuff, that values of `Queue a` type cannot be removed, because linear types request exactly one use. They must get to be return values. Therefore I made `Queue a` be an instance of the `Consumable` type class of the `Prelude.Linear` module of the linear-base package.

```haskell
instance Consumable a => Consumable (Queue a) where
  consume (Queue l m) = l `lseq` m `lseq` ()
```

Now I will try to use this.

```haskell
> import Prelude.Linear (lseq)
> import Data.Queue.Ephemeral
> empty (\q0 -> enqueue 0 q0 (\q1 -> dequeue q1 (\(Just (a, q2)) -> q2 `lseq` a))) :: Int
0
```

… Ah, yeah, It can be used. It can just be used, it cannot be used comfortably.

# Continuation monad

You can use “do” notation to write/read it easily because CPS functions are monad instances.

Now can linear CPS functions be linear monad instances? Let me try. … (three days after) They can be! The following type can be a linear monad instance. It was more difficult than I expected to type validly because I was not familiar with linear types.

```haskell
newtype ContT r m a = ContT { runContT :: (a #-> m r) #-> m r }
```

I will try to use it.

```haskell
> :set -XQualifiedDo
> import Prelude.Linear (lseq)
> import qualified Prelude.Linear as PL
> import Data.Queue.Ephemeral
> import Control.Monad.Trans.Cont.Linear
> import qualified Control.Monad.Linear as ML
> :{
| PL.flip runCont PL.id $ ML.do
|   q0 <- cont empty
|   q1 <- cont (enqueue (0 :: Int) q0)
|   Just (a, q2) <- cont (dequeue q1)
|   q2 `lseq` ML.pure a
| :}
0
```

Yahoo!

Meh, there is a loophole to escape from the constraint with `pure`.

# Repository

https://github.com/kakkun61/ephemeral-linear-data/tree/fd2f936ffea1a8d98445947dea460234217286b1

# Additional article

{% post kakkun61/ephemeral-purely-functional-data-structure-and-linear-type-again-4mnm %}