Kazuki Okamoto

Posted on Dec 28, 2020 • Updated on Jan 1, 2021

Ephemeral Purely Functional Data Structure and Linear Type

#haskell

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)

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)
- A linear arrow is (#->), not (%1 ->)
linear-base 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.

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.

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.

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