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 >)
 A linear arrow is
 linearbase 341007891ae77959ac7b147f008e3a1d9c46e96b
Implementation
I implemented it with the continuationpassing 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 linearbase 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/ephemerallineardata/tree/fd2f936ffea1a8d98445947dea460234217286b1
Discussion (0)