The Japanese version is at はてなブログ.
Additional information for the previous article.
Meh, there is a loophole to escape from the constraint with
I wrote it carelessly, I was noticed good information on Reddit.
I think the solution to the problem with
emptymight be to use the
Ur(for "unrestricted") datatype from linear-base:
empty :: (Queue a #-> Ur b) #-> Ur b
Trying to run
empty Urshouldn't typecheck, because the
Urconstructor 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!
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ɪ̟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
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