Changes between Version 14 and Version 15 of LinearTypes

Jan 8, 2018 1:51:23 PM (2 months ago)



  • LinearTypes

    v14 v15  
    1717A library to serve as a central library for linearly typed program can be found at
     19== Faq ==
     21{{{#!box help
     22= Does this proposal improve performance =
     26This proposal focuses on one thing and one thing only: letting users ascribe more precise types to functions. More precise types can mean more safety, which in turn means things that were dangerous to do before can now be viable (such as optimizations to your code). Three examples:
     28* Allocating long-lived objects in the C heap instead of the Haskell heap. This can ease pressure on the garbage collector (GC) and therefore improve tail latencies and potentially throughput as well. Difficult to guard against use-after-free or double-free errors without linear types.
     29* Zero-copy serialization. This is the largest example in the [ POPL'18] paper and is the topic of a [ blog post] as well. The idea is to skip deserialization altogether when receiving structured message types. This is very error prone in general, but the paper explains how this can be done safely with linear types.
     30* Safe mutable arrays. Mutable arrays are typically implemented in the {{{ST}}} monad. But using a monad for locally impure code over-sequentializes computations, so opportunities for parallelization are lost. Linear types let us recover the lost parallelism, allow local mutation and still guarantee that referential transparency won't be broken.
     33{{{#!box help
     34= Does this proposal change the RTS? =
     38This proposal only affects the syntax of types, the type checker and GHC's Core language.
     41{{{#!box help
     42= Why does this proposal need to change Core? =
     44There are two reasons:
     46* In GHC, the type {{{Type}}} is shared between the surface language and Core. So modifying the types implies that Core is modified as well.
     47* More importantly, because Core is a good check that our implementation works as intended. That is, a linearly typed Core will ensure that linearly-typed programs are indeed desugared to linearly-typed programs in Core. And that optimisations do not destroy linearity.
     50{{{#!box help
     51= Isn't a linear function that diverges unsound? =
     53Our proposed type system allows you to give a linear type to list concatenation:
     56(++) :: [a] ->. [a] ->. [a]
     58So we can write
     61strange :: Int ->. [Int]
     62strange x = (repeat 1) ++ [x]
     64This sounds like it's breaking the promise made by {{{strange}}} that it will consume its argument exactly once. Since {{{x}}} will ''never'' be consumed!
     66But there is no cause for panic: {{{strange}}} only promises to consume {{{x}}} if its result is consumed. Which will never happen since the result of {{{strange}}} is infinite. The properties of linear types which we need are not compromised by non-termination.
     69{{{#!box help
     70= In the motivations of the proposal, there is a linear IO monad. Isn't linear IO unsound in presence of exception? =
     72It is not, but as always, we need to careful about how we type primitives of the {{{IO}}} monad. For example, [ {{{catch}}}] should not have a linear type. It should be typed as follows:
     76  :: Exception e
     77  => IO (Unrestricted a) -> (e -> IO (Unrestricted a)) -> IO (Unrestricted a)
     79This means that neither the body nor the handler of {{{catch}}} can capture linear variables. Otherwise, you could lose track of them.
     81If, say, the body of {{{catch}}} was linear, we could write:
     84oops :: a ->. IO (Unrestricted ())
     85oops x =
     86  catch
     87    (throwIO "This is bad" >> oops a)
     88    (\_ -> return $ Unrestricted ())
     92{{{#!box help
     93= Don't linear guarantees degrade to affine in the presence of exceptions? =
     95When an exception is raised during the consumption of {{{f u}}}, {{{u}}} may not have been fully consumed. Functions whose argument is consumed ''at most'' once when their result is consumed exactly once are called affine.
     97Linear functions do have the property that: /if their result is consumed at most once, then their argument is consumed at most once/. This is a more relevant phenomenon in case exceptions are raised: exceptions interrupt the consumption of the result, which is only partial.
     99In fact, linear functions have the property that if their result is consumed with multiplicity X, then their argument is also consumed with multiplicity X. Whatever we choose X to mean. Which can be internalised in the language as follows
     102data Mult (p :: Multiplicity) (a :: *) where
     103  Mult :: a :p-> Multp p a
     105multMap :: (a ->. b) -> Mult p a -> Mult p b
     106multMap f (Mult x) = Mult (f x)
     110{{{#!box help
     111= Wouldn't it be just as good to have affine types, since they are simpler? =
     113Having affine types would makes some things easier. For instance {{{catch}}} is allowed to capture affine variables:
     116-- Writing A for the multiplicity of affine functions
     118  :: Exception e
     119  => IO (Unrestricted a) :'A-> (e -> IO (Unrestricted a)) :'A-> IO (Unrestricted a)
     121However, the Rust programming language, with its (essentially) affine language has shunned exceptions for a reason: they are still quite a complication.
     123Affine types are sufficient for abstractions based on ownership, as long as you don't care about prompt deallocation (mutable arrays on the GC heap are a good example where you don't).
     125To recover prompt deallocation, Rust relies on a bespoke mechanism (lifetime analysis) and code generation to an essentially linear language. This is something which is not reasonable to hope for in Haskell at the moment.
     127Use-cases which do not rely on uniqueness, such as Samuel Gelinaux's [ 3D-printable model example] (which he also implemented with our prototype [ here]) may not accommodate affinity so well.
     129Offering affine types in addition to linear types is possible. In fact no choice that we make now compromises the ability to add them later, because our linear types system was specifically designed to allow all manner of other multiplicities as extensions. So we propose to keep an already large proposal as small as possible, and postpone adding affine types to a future proposal, if and when the need arises.
     132{{{#!box help
     133= Do linear types guarantee resource safety? =
     135No. Linear types only gives a type to functions that consume their argument exactly once when their result is consumed exactly once.
     137Having linear types is powerful, and makes it possible to write ''resource-safe abstractions''. But this is not an intrinsic quality of the type system.
     140{{{#!box help
     141= Will base be modified to use linear types? =
     143Not at first. When it happens it will be as a separate proposal to the Core library Committee (CLC), if at all.
     145Before we are ready to make a proposal, users should put linear types to work and share idioms via a [ linearly typed library], uploaded to Hackage, and driven by the ecosystem. Anyone could, in a future proposal to the CLC, propose for some of these idioms to be standardized in base.
     148{{{#!box help
     149= Will adding linear types fragment the libraries ecosystem? =
     151The centrepiece of our design is to avoid code duplication. Crucially, the same types can be used in linear and non-linear contexts. For example, the [ {{{linear-base}}}] library uses the same types as {{{base}}}. So libraries developed with {{{linear-base}}} will be compatible with libraries developed with {{{base}}}.
     154{{{#!box help
     155= Is this type for monads in the paper correct? =
     157The linear types proposal features monads with the following interface
     160return :: a ->. m a
     161(>>=) :: m a ->. (a ->. m b) ->. m b
     163But unfolding the definitions of the Kleisli extension and unit of a monad you would get instead
     166return :: a -> m a
     167extend :: (a ->. m b) -> (m a ->. m b)
     169Which is right? The latter type is actually not very useful, but it would feel uncomfortable if the former type was not backed by well-known mathematics.
     171Fortunately, it is: it is the type of an enriched monad over the self-enrichment of the base category. Briefly:
     173* An [ enriched category] is a category whose hom-sets are taken to be objects in another category (which must be monoidal).
     174* Any closed symmetric monoidal category is enriched over itself.
     175* The category of Haskell types and linear functions is closed symmetric monoidal (with the usual [ provisos]). Let's call it LHask.
     176* Monads of LHask for which the unit and join are maps in LHask are called enriched monads.
     178This is related to the often overlooked fact that monads must be [ strong], both in Moggi's theory of effects, and as a programming language construct. It is easy to overlook because (self-)enriched monads are necessarily strong. And all monads in Hask are, naturally, self-enriched. See [ this discussion] for more details.