3/5

bibliography/acm_3158093.bib

@@ -0,0 +1,18 @@
+@article{lh_bernardy_2017,
+author = {Bernardy, Jean-Philippe and Boespflug, Mathieu and Newton, Ryan R. and Peyton Jones, Simon and Spiwack, Arnaud},
+title = {Linear Haskell: practical linearity in a higher-order polymorphic language},
+year = {2017},
+issue_date = {January 2018},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {2},
+number = {POPL},
+url = {https://doi.org/10.1145/3158093},
+doi = {10.1145/3158093},
+abstract = {Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows. Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values. To demonstrate the efficacy of our linear type system — both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types — we implemented our type system in ghc, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions.},
+journal = {Proc. ACM Program. Lang.},
+month = dec,
+articleno = {5},
+numpages = {29},
+keywords = {typestate, polymorphism, linear types, linear logic, laziness, Haskell, GHC}
+}

main.tex

@@ -85,6 +85,15 @@ some similarity to \lad.
 Because of to the array-programming nature of the langauge, the shape type is fit only to arrays, but displays some flexibility, 
 which, in a way, is more akin to the constructors used in \lad than to the holes used by Minamide \cite{minamide_holes_1998}.
 
+\section{Linear Haskell: practical linearity in a higher-order polymorphic language - Bernardy et al. \cite{lh_bernardy_2017}}
+Linear logic/ typing stands at the core of the \lad type system, and its concrete form is massively influenced by Linear Haskell.
+Bernardy et al. give deeper insight into linear typing as it is the sole focus of this paper. 
+They focus on implementing linear typing in haskell but give good intuition on linear types as a whole.
+Though unrestricted types are not a core language feature but implemented in the language itself, the type system is
+very similar to \lad, in fact the calculi even share syntax for the linear function.
+Bernardy et al discuss many benefits of linear typing and \lad in it's whole bases on the idea of lienar types to make
+multiple writes on data impossible.
+
 \input{./bibliography/all.tex}
 \bibliographystyle{splncs04}
 \end{document}