diff --git a/main.tex b/main.tex index aabdb5b..6119df0 100644 --- a/main.tex +++ b/main.tex @@ -7,7 +7,7 @@ \usepackage[T1]{fontenc} % T1 fonts will be used to generate the final print and online PDFs, % so please use T1 fonts in your manuscript whenever possible. -% Other font encondings may result in incorrect characters. +% Other font encodings may result in incorrect characters. % \usepackage{graphicx} % Used for displaying a sample figure. If possible, figure files should @@ -60,36 +60,36 @@ \section{Introduction} In their work Bagrel and Spiwack \cite{bagrel_dp_2025} build on many prior contributions, both directly in their calculus grammar and semantics, but also in their structural approach regarding typing and evaluation contexts. -From now on the calculus introduced in this specific paper will be referred to as \lad. -This report will highlight a number of select works, which are of significance to the $lambda_d$ calculus. +From now on, the calculus introduced in this specific paper will be referred to as \lad. +This report will highlight a number of select works, which are of significance to the \lad calculus. \section{A Functional Representation of Data Structures with a Hole - Y. Minamide\cite{minamide_holes_1998}} This paper contributes fundamental work on holes in functional languages. It introduces a hole abstraction $\hat\lambda x. T$ to formalize data structures with a single hole. -Which, while syntactically different, in principle remains similar to the \lad calculus. +This, while syntactically different, in principle remains similar to the \lad calculus. Both utilize holes as the core features, where \lad has a type $T_1 \ltimes T_2$ to represent a structure that is missing $T_1$ to complete a $T_2$, Minamide's calculus features $(T_1, T_2) hfun$. In general Minamide focuses more on the similarity of his hole abstraction to the regular $\lambda$ abstraction -and the similarity of a structure containing a hole, to a function that returns an type $T_2$, when applied argument to an argument $T_1$. -Notably both calculi contain linearity constraints on holes, but Bagrel's work elevates some of those constraints by allowing for weakening. -Overall Minamide lays a lot of ground work, and influences that can be seen in the \lad formulation and in its discussion, as +and the similarity of a structure containing a hole, to a function that returns a type $T_2$, when applied to an argument of type $T_1$. +Notably both calculi contain linearity constraints on holes, but Bagrel's work relaxes some of those constraints by allowing for weakening. +Overall Minamide lays a lot of groundwork, and influences that can be seen in the \lad formulation and in its discussion, as similar benefits regarding tail recursion are addressed. \section{Destination-Passing Style for Efficient Memory Management - Shaikhha et al. \cite{shaikhha_array_dps_2017}} While Bagrel mostly theorizes on the advantages of the \lad calculus, -this paper give empirical evidence on runtime and memory improvements of Destination Passing Style (DPS) in a functional language. +this paper gives empirical evidence on runtime and memory improvements of Destination Passing Style (DPS) in a functional language. Shaikhha et al. demonstrate the benefits of implementing a DPS-transformation step into the compilation of an array-programming language. -The authors chose to not give any direct memory control to the programmer, but their intermediate language '\dpsf' still feature +The authors chose to not give any direct memory control to the programmer, but their intermediate language '\dpsf' still features some similarity to \lad. \dpsf is typed using a shape type, which contains the dimensions of the array, which will be written to a memory location/ destination. -Because of to the array-programming nature of the language, the shape type is fit only to arrays, but displays some flexibility, +Because of the array-programming nature of the language, 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{Tail Modulo Cons - \cite{bour_et_al_tmc_2021}} -This paper proposes a annotation controlled, compile time transformation of OCaml into a DPS intermediate language. +This paper proposes a annotation-controlled, compile time transformation of OCaml into a DPS intermediate language. The intermediate language only features structures with single holes/ single destinations. The driving goal of Tail Modulo Cons (TMC) is, as the name suggests, to elevate the issues of constructors wrapping a recursive call. -Particularly TMC allows for tail recursion, even if the recursive call is hidden behind a data constructor. +Particularly, TMC allows for tail recursion, even if the recursive call is hidden behind a data constructor. While TMC is an intermediate language it allows for some source level control, as only annotated functions are converted into DPS. @@ -99,8 +99,8 @@ Bernardy et al. give deeper insight into linear typing as it is the sole focus o 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 linear types to make -multiple writes on data impossible. +Bernardy et al. discuss many benefits of linear typing and \lad in its whole is based on the idea of linear types to make +multiple writes to data impossible. \section{A Unified View of Modalities in Type Systems - Abel and Bernardy \cite{abel_bernardy_2020}} \lad includes a notion of modality using the exponential $!_mT$, of which the ground work is laid by Abel and Bernardy in this work.