Can Linear Type help using a binding only once?

Learn
#1

There is a problem I have often enough which is using different variable names (with number) to represent the different stages of the computation of the same value : something that would probably be achieved with mutation in traditionnal langage. I know the topic is regularly discussed and I haven’t find a nice solution yet.

Today this problem occurs with

type or paste code hermakeScenario :: [(HeaderType, (DocumentHash, Text))]  -> Either Text Scenario
makeScenario sections0 = do -- Either
  let (initials, sections1) = partition (( InitialH==). fst) sections0
      (layouts, sections2) = partition (( LayoutH==). fst) sections1
      something with sections2

What is important is that sections<n> should be only used once except for the last one sections2.
Today I need to add

    (colorMap, sections3) = partition (( ColorMapH==) . fst) sections2

and make sure that I replace everywhere sections2 with sections3.
I know there are alternatives ( using runState, renaming sections2 sothat it is not used elsewhere,etc) , but what I am interested in is "is there anyway to force sections2 to be used only once using linear type ?

2 Likes
#2

I know it’s not an answer to original question, but usually in such cases I find myself just using State monad with state function.

#3

I though about that, and it’s seems a good idea. However I am already within a Either monad and reaching for monad transformers just for that seems an overkill.

1 Like
#4

Linear types also seem an overkill, although I’ve never used them so maybe it’s not so bad.

That said, I’m also curious about an answer.

1 Like
#5

Fwiw, linear-base has the equivalent partition:

partition :: Dupable a => (a %1 -> Bool) -> [a] %1 -> ([a], [a])

My question would be, is it an interesting guarantee to the API user of makeScenario to have the guarantee of your “section” is consumed once and only once? If so you should be able to declare this, pull in linear-base dependency, and import qualified Data.List.Linear as LL as an almost drop-in replacement (you can’t use let binding yet, and you may need to enable ImpredicativeType sometimes to get some type inference stuff work):

type SomeSection = [(HeaderType, (DocumentHash, Text))] -- ?
hermakeScenario ::  SomeSection ⊸ Either Text Scenario

If such guarantee is not interesting to your user, probably an overkill. Also your user will pay the price of not allowed to use the section any more.

#6

In theory it is not even guarantee to the user, as I am only talking of the internal variables sessions<0-2>. sessions3 can be used more than once (or not).
However in practice, it is likely that sessions3 will be used exactly once, so your solution might work.
If it’s not interesting for the user , I guess I can wrap the lollipop version to hide it can I ?
I’m still interest out of curiosity if what I am asking is possible even if it’s an overkill.
Maybe in the future something like

   (initials, sections1 %1) = ...

Would be possible …

#7

IMO, you should just structure your program so that there aren’t bindings in scope that you don’t need or want in scope.

makeScenario :: [(HeaderType, (DocumentHash, Text))]  -> Either Text Scenario
makeScenario = somethingWith . sectionsOf

  where
    somethingWith (layouts, sections) = ...
    sectionsOf stuff = let (initials, sections) = partition ((InitialH ==) . fst) stuff in
                         partition ((LayoutH ==) . fst) sections
#8

It’s a good idea, but in this particular case I need to do something with initials, layouts and colorMap.
Using a where clause or equivalent becomes quiclky a bit tedious.

#9

It shouldn’t. You can still structure your app the way you need while still providing bindings for only what you need.

Here a couple of ideas:

-- Take a list of filter functions and return a list of matching value sets in order.
filtered :: [a] -> [a -> Bool] -> [[a]]
filtered xs = fst . foldl' (\(r, ins) x -> let (y,n) = partition x ins in (r<>[y], n)) ([], xs)

This might be a bit difficult to use because you can’t easily prove correctness, but if you mix in a State monad, you get something much closer to what you want. e.g.:

section :: Eq a => a -> State [(a,b)] [(a,b)]
section a = state (partition ((==a) . fst))

I don’t have a complete code example, so I’m not sure where that was going, but it’d be something like this:

makeScenario :: [(HeaderType, (DocumentHash, Text))]  -> Either Text Scenario
makeScenario = flip runState go
    where
        go = do
            initials <- section InitialH
            layouts <- section LayoutH
            -- something with layouts
            colorMap <- section ColorMapH
#10

Alternatively, you could use a Map instead of a [] and avoid all the partitions.

makeScenario stuff = do
      let initials = lu InitialH
          layouts = lu LayoutH
          colorMap = lu ColorMapH
      -- do things
    where
       m = Map.fromListWith (<>) [ (a,[b]) | (a,b) <- stuff ]
       lu k = Map.findWithDefault [] k m

There are other ways, but I still think the answer is to try to avoid making bindings instead of trying to avoid using them.

1 Like
#11

@maxigit if you ever figure out the answer to your original question, let me know.

#12

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.

2 Likes
#13

That’s a great answer. Implementation3 shows that my intiution was correct and that it was possible to use linear type (regarless of it practicability) to guarantee single use.

Maybe a syntax like let session %1 = ... would be nice if possible.

Having said that, I agree that even though counter intuitive, the shadowing approach might actually be the best.

#14

See implementation3 of @rednaZ @redna answer

#15

thanks for reminding me of linear let bindings. i only remembered that linear haskell decided to “attach linearity to function arrows” (linear haskell paper) instead of types in general. but forgot that semantics for linear let bindings were still included too.

incidentally, @aspiwack did request to merge an implementation of linear let bindings a week ago.

2 Likes
#16

I’m a bit confused, the tile refers to let bindings but then says that recursive let are left inrestricted. How would that work with implemention3 ?

#18

by “recursive let” they mean let bindings that the compiler detected to actually be recursive. none of the code we discussed is actually recursive, is it?

#19

No it is not recursive. I didn’t know the compiler was trying to detect recursive let.