DEV Community

loading...

Ephemeral Purely Functional Data Structure and Linear Type

kakkun61 profile image 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
Enter fullscreen mode Exit fullscreen mode
-- 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)
Enter fullscreen mode Exit fullscreen mode

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

Used versions

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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` ()
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

… 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 }
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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

Discussion (0)

pic
Editor guide