Linearity via ST monads{ phantom type parameter s} -( region) that is instantiated once at start ofcomputation by a runST function of type:runST :: ∀a. (∀s. ST s a) → aresources that are allocated during computation,eg mutable cell references,cannot escape the dynamic scope of the call to runST because they are themselves tagged with thesame phantom type parameter.Region-types. With region-types such as ST, we cannot express typestates, but this is sufficientto offer a safe api for freezing array or ensuring that files are eventually closed. This simplicity(one only needs rank-2 polymorphism) comes at a cost: we’ve already mentionned in Sec. 2.2 that itforces operations to be more sequentialised than need be, but more importantly, it does not supportprima facie the interaction of nested regions.Kiselyov and Shan [2008] show that it is possible to promote resources in parent regions toresources in a subregion. But this is an explicit and monadic operation, forcing an unnatural imperative style of programming where order of evaluation is explicit. The HaskellR project [Boespfluget al. 2014] uses monadic regions in the style of Kiselyov and Shan to safely synchronise valuesshared between two different garbage collectors for two different languages. Boespflug et al. reportthat custom monads make writing code at an interactive prompt difficult, compromises code reuse,forces otherwise pure functions to be written monadically and rules out useful syntactic facilitieslike view patterns.In contrast, with linear types, values in two regions hence can safely be mixed: elements can bemoved from one data structure (or heap) to another, linearly, with responsibility for deallocationtransferred along.t everything which must be single-threaded – and that we would track with linearity – becomepart of the state of the monad. For instance, coming back to the sockets of Sec. 5.2, the type of bindwould be as follows:bind :: (sock :: Var) → SocketAddress → ST IO () [sock ::: Socket Unbound :7→ Socket Bound]Where sock is a reference into the monads’s state, and Socket Unbound is the type of sock beforebind, and Socket Bound, the type of sock after bind.Idris uses its dependent types to associate a state to the value of its first argument. Dependenttypes are put to even greater use for error management where the state of the socket depends onwhether bind succeeded or not:-- In Idris, bind uses a type-level function (or) to handle errorsbind :: (sock :: Var) → SocketAddress →ST IO (Either () ()) [sock ::: Socket Unbound :7→ (Socket Bound ‘or‘ Socket Unbound)]-- In Linear Haskell, by contrast, the typestate is part of the return typebind :: Socket Unbound ⊸ SocketAddress → Either (Socket Bound) (Socket Unbound)The support for dependent types in #ghc is not as comprehensive as #Idris . But it is conceivable toimplement such an indexed monad transformer in #Haskell. an existing lazy language, such as Haskell, can be extended withlinear types, without compromising the language, in the sense that:• existing programs are valid in the extended language without modification,• such programs retain the same operational semantics, and in particular• the performance of existing programs is not affected,• yet existing library functions can be reused to serve the objectives of resource-sensitiveprograms with simple changes to their types, and no code duplication.https://arxiv.org/pdf/1710.09756.pdf
rml