sure. consider the following simplified code.
implementation0 :: [Bool]
implementation0 =
let
sections0 = []
(initials, sections1) = partition (== False) sections0
(layouts, sections2) = partition (== False) sections1
in sections2 <> sections2 <> initials <> layouts
find an executable version of all code on the haskell playground.
first we need to convert a = b
bindings into b & \a ->
bindings as follows because linear haskell attaches linearity to function arrows.
implementation1 :: [Bool]
implementation1 =
[] & \sections0 ->
partition (== False) sections0 & \(initials, sections1) ->
partition (== False) sections1 & \(layouts, sections2) ->
sections2 <> sections2 <> initials <> layouts
the \ %'One x -> x
syntax as proposed in the ghc proposal to make lambda abstractions linear has unfortunately not been implemented yet. until implemented we have to add something like )::_ %1->_)
for every binding to the end of our list of bindings as follows.
{-# language LinearTypes, PartialTypeSignatures #-}
implementation3 :: [Bool]
implementation3 =
let
(initials, layouts, sections2) =
[] & ((\sections0 ->
partition (== False) sections0 & ((\(initials, sections1) ->
partition (== False) sections1 & ((\(layouts, sections2) ->
(initials, layouts, sections2))::_ %1->_))::_ %1->_))::_ %1->_)
in sections2 <> sections2 <> initials <> layouts
such lambda bindings can always be converted to do
syntax too as follows.
{-# language QualifiedDo #-}
implementation4 :: [Bool]
implementation4 =
let
(initials, layouts, sections2) = runIdentity $ L.do
sections0 <- pure []
(initials, sections1) <- pure $ partition (== False) sections0
(layouts, sections2) <- pure $ partition (== False) sections1
pure (initials, layouts, sections2)
in sections2 <> sections2 <> initials <> layouts
you can convince yourself that both those solutions fulfil your linearity requirements on the haskell playground.
but as others have already pointed out, you are having a scoping problem rather than a linearity problem. for example, what would you do if you had an operation there in the middle that uses the previous result twice like (sections1, partition (== False) sections1)
? the fact that partition
is linear is indeed just a lucky coincidence.
so linear types cannot solve this scoping problem in general. but shadowing can. unfortunately, shadowing is not possible in let
bindings because let
bindings are so very recursive.
so the proper solution would be adding support for non recursive let
style bindings to ghc. ideally a NoRecursiveLet
extension that requires let rec
for recursive bindings. or at least a let norec
keyword.
until then, we can use lambda bindings and do
syntax, both of which support shadowing, as follows.
implementation5 :: [Bool]
implementation5 =
[] & \sections ->
partition (== False) sections & \(initials, sections) ->
partition (== False) sections & \(layouts, sections) ->
sections <> sections <> initials <> layouts
implementation6 :: [Bool]
implementation6 = runIdentity $ do
sections <- pure []
(initials, sections) <- pure $ partition (== False) sections
(layouts, sections) <- pure $ partition (== False) sections
pure $ sections <> sections <> initials <> layouts
i would argue the linear haskell based solutions are strictly worse than these shadowing based ones, because anything you might not like about the shadowing based solutions, you will find in the linear haskell based solutions too.