DEV Community

loading...

Ephemeral Purely Functional Data Structure and Linear Type: Again

kakkun61 profile image Kazuki Okamoto ・2 min read

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


Additional information for the previous article.

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.

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

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

Discussion (0)

pic
Editor guide