text: I have been wondering about linear logic for a while, and after reading Edsko de Vries' blog post: Linearity, Uniqueness, and Haskell, I finally got to dump my thoughts on the topic.
  Edsko starts with two example functions, where the second one is following:
  frugal :: a -> (a, a) frugal x = (x, x)
  In Haskell functions can reuse their arguments, as
  frugal does. Later he shows that linear setting we can forbid such functions.
  ## Pairs
  A taste of linear logic by Philip Wadler is a very nice introduction to the intuitionistic linear logic. One of the take aways, is that in linear logic, there are two kind of pairs, "ands". And there's still single "or".
  So to recap, Take
  A to be the proposition "I have ten zlotys",
  B to be the proposition "I have a pizza", and
  C to be the proposition "I have a cake". We can say
  And there are three ways to "pair" the terms:
  In natural language we'd might say: whichver I choose from a cake or a pizza. That's confusing.
  In the Edsko's post, the pairs are assumed to be of the first kind: ⊗, tensors. We cannot write
  fst or
  snd variants for the tensor, but
  uncurry :: (a -o b -o c) -o a ⊗ b -o c uncurry f p = case p of (x, y) -> f x y
  is ok.
  However, if we work with the second kind of the pair, "with", we cannot write
  uncurry, but can have
  fst and
  snd:
  fst :: a & b -o a fst (x, _) = a snd :: a & b -o b snd (_, y) = y
  And with this pair we can write something like:
  haveAndEat :: Vector Double -o Vector Double & Vector Double heveAndEat arr = (write 0 2.3 arr, arr) -- one should really have different constructor for tensor and with
  There is no problem, as a callee cannot use both sides of the with, they have to choose only (and exactly) one half.
  I.e. we can write
  frugal as
  frugal :: a -o a & a frugal x = (x, x)
  ## With
  IMHO
  with is a very interesting construction. It seems it cannot exist in a strict language: only when we apply
  fst or
  snd will force it. In addition, when we force one half, the thunk for the other can be released immediately.
  I guess this can be useful in non-backtracking infinite solution-space traversals, by using with we could be sure we don't introduce space leaks by accidentally retaining other paths.
  ## Linear State
  Recall a state monad
  newtype State a = State { runState :: s -> (a, s) }
  We can have linear version of it, and the
  Monad instance would type-check:
  newtype LinearState a = LinearState { runLinearState :: s -o a ⊗ s } instance Monad LinearState where return x = \s -> (x, s) m >>= k = LinearState $ \s -> case runLinearState m s of (a, s') -> runLinearState (k a) s'
  The interesting part, is that this type isn't an instance of
  MonadState. We cannot write
  get or
  put. And we cannot write
  MonadReader with
  ask = get either. But we can have a different class:
  class Monad m => MonadLinearState s m | m -> s where linearModify :: (s -o s) -o m () instance MonadLinearState s (LinearState s) where linearModify f = LinearState $ \s -> ((), f s)
  Also
  LinearWriter, i.e. the one without
  listen or
  pass.
  AFAICS, we could have
  MonadLinearState RealWorld# IO, without problems!
  ## do-notation
  It seems, that if we had linearity, then we can use linearity to handle resources. We can write
  bracket like functions, where we have to return the token at the end:
  -- Not sure about the arrows, should they be lollipops? withFile :: FilePath -> (Handle -o IO (Handle ⊗ a)) -> IO a getFileContents :: Handle -o IO (Handle & String) lineCount :: FilePath -> IO Int lineCount fp = withFile fp $ \h -> do (h, contents) <- getFileContents h return (h, length $ lines contents)
  That's something where
  LinearStateT will make code nicer. Or we can change
  getFileContents :: Handle OPENED -o IO (Handle CLOSED ⊗ String), or actually we'd need to have
  withFile :: FilePath -> (forall s. Handle s OPENED -o IO (Handle s CLOSED ⊗ a)) -> IO a
  The type variable
  s will index our
  Handle, so don't pass a wrong one when we have nested
  withFiles.
  But then we couldn't use
  do notation, as state variable will change. We'd need indexed monads, oh dear.
  At this point, I have to mention, that linear types would give us great power, but explaining this kind of IO (or any "magic" involcing them) to a beginner won't be easy.
  FWIW,
  withMutableArray from Edsko's post is simpler example of this idea of handling resources.
  ## Point free
  phadej @pl \xs -> map f (filter g xs) lambdabot map f . filter g -- looks linear phadej @pl \x -> x * x lambdabot join (*) -- but join isn't (Reader) phadej @pl \p -> (fst p, snd p) lambdabot id -- sometimes pl is smart phadej @pl \p -> (fst p, snd p + 2) lambdabot liftM2 (,) fst ((2 +) . snd) -- sometimes it isn't phadej @pl \p -> uncurry (\x y -> (x, y + 2)) p lambdabot second (2 +) -- so you have to help it
  TL;DR concatative languages are linear by default, as there are special operators to contract and weaken!
  ## Traversals
  It's probablty not obvious, but the type
  traverse :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
  is ok to linearise into:
  linearTraverse :: (LinearApplicative f, LinearTraversable t) => (a -o f b) -> t a -o f (t b)
  Or can we reuse
  Applicative f? Hard to say at this point. What arrows should be there? Polymorphic in arrows, with some relations?
  ## Conclusion
  In this post I used different syntax than in used by Edsko, the one I learned from watching lectures and reading papers on linear logic. And I have to agree, it's hard to evaluate how well type system will work in practice. Will we need with, how higher order functions or polymorphism will fit etc. I'm also looking forward how Haskell could support linearity, and what cool stuff we can do with it!