Ephemeral Purely Functional Data Structure and Linear Type: Again

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

---

Additional information for the previous article.

Ephemeral Purely Functional Data Structure and Linear Type

Kazuki Okamoto ・ Dec 28 '20 ・ 3 min read

#haskell

No loopholes using pure

Meh, there is a loophole to escape from the constraint with pure.

I wrote it carelessly, I was noticed good information on Reddit.

I think the solution to the problem with empty might be to use the Ur (for "unrestricted") datatype from linear-base:

empty :: (Queue a #-> Ur b) #-> Ur b

Trying to run empty Ur shouldn't typecheck, because the Ur constructor is not linear. This seems to be an idiom used in other places of linear-base.

Queue a cannot get escaped because of making the type of the return value Ur b. Passing Queue a to Ur is not allowed because the parameter of Ur :: a -> Ur a may be used many times. How smart!

No need for CPS

I found that functions other than generators (empty in this case) are no need for CPS.

When applying a linear arrow to a value that is a parameter of another linear arrow, it seems that its return value has linearity too. I must check typing rules about this.

o̞͑kä̝mo̞͑to̞͑ kä̝zʊ̠kɪ̟

@kakkun61

idl の返り値の a も1回しか使えないという性質を引き継いでるんだな。まあそうじゃないと困るが。

05:37 AM - 21 Dec 2020

In other words, It is not necessary to make enqueue etc. CPS because their return values must be used once when applying them in a continuation Queue a #-> Ur b of empty.

null :: Queue a #-> (Ur Bool, Queue a)
null (Queue l m) = (Ur (P.null l), Queue l m)

enqueue :: a -> Queue a #-> Queue a
enqueue a (Queue l m) = check l (a:m)

dequeue :: Queue a #-> (Ur (Maybe a), Queue a)
dequeue (Queue (a:l) m) = (Ur (Just a), check l m)
dequeue (Queue l m) = (Ur Nothing, Queue l m)

That being so, user codes are as the following. It was easy to write/read if the “let” expression could be used.

  it "empty → enqueue → dequeue" $ do
    let
      f :: Queue Int #-> Ur Int
      f q =
        enqueue 0 q PL.& \q ->
        dequeue q PL.& \(Ur (Just a), q) ->
        q `lseq` Ur a
      Ur a = empty f
    a `shouldBe` 0