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
- 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
Top comments (0)