## DEV Community is a community of 617,782 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

# Ephemeral Purely Functional Data Structure and Linear Type Kazuki Okamoto Updated on ・3 min read

The Japanese version is at はてなブログ.

Chapter 5.2 of “Purely Functional Data Structures” (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.

``````-- a good example
ops =
let
q0 = empty
q1 = enqueue 0 q0
q2 = enqueue 1 q1
Just (a, _) = dequeue q2
in
a
``````
``````-- 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)
``````

# 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.

``````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.

``````{-# 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.

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

Now I will try to use this.

``````> 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.

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.

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

I will try to use it.

``````> :set -XQualifiedDo
> import Prelude.Linear (lseq)
> import qualified Prelude.Linear as PL
> import Data.Queue.Ephemeral
> 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 