As Haskell is increasingly used in production environments, the Haskell toolchain is of critical importance to a growing number of people and organisations. At the heart of this toolchain is GHC (The Glasgow Haskell Compiler). Conceived nearly thirty years ago as a research project by Simon Peyton Jones, GHC has long existed at the intersection of research and commercial use, due to the increasing popularity of Haskell. To provide stability and a basic level of support, the project was generously supported by Microsoft Research for many years. However, as more and more companies and others are using GHC in mission-critical ways, the bar is going up. We need a solid, reliable, well-engineered, predictable GHC toolchain; and we need to achieve that without compromising GHC innovation and vitality.
Shared responsibility
In response to this situation, GHC HQ and several stakeholder organisations decided to work together to improve the situation and to provide shared leadership and a broader pool of resources for the DevOps aspects of GHC development. As a concrete first step in this new partnership, we announced the formation of the GHC DevOps Group at the 2017 Haskell Implementors’ Workshop in Oxford.
Our mission
As set out in the group’s charter, the mission of the GHC DevOps Group is threefold:
- to take leadership of the DevOps aspects of GHC,
- to resource it better, and
- to broaden the sense of community ownership and control of GHC.
As important as the goals are the group’s non-goals. The GHC DevOps group is exclusively concerned with the processes and tools for code development, community contributions, and regular, reliable & well-tested releases. It is about how and when features get into GHC and are shipped to users. In contrast, it is not concerned with the choice of which features go into GHC, let alone the content of the libraries it ships with. This is the responsibility of the GHC Steering Committee and proposals process and the Core Libraries Committee, respectively.
Our current goals
During its formation, the group identified two initial goals:
- moving to two calendar-based GHC releases per year, and
- lowering the barrier to contributing to GHC.
Quality calendar-based releases every six months
As Ben Gamari documented in detail in his Reflections on GHC’s release schedule, actual GHC release dates are hard to predict and initial release quality is often low due to critical bugs. These are the typical symptoms that modern DevOps processes, such as continuous and automated integration, testing, and delivery, are designed to eliminate. Hence, we are working towards reliable continuous building and testing of GHC as well as pre-merge commit testing. Automating everything leads to the entire set of release artefacts being built and provided during that same process.
The main choice that we are currently facing is whether to build our own solution and maintain our own infrastructure based on Jenkins or whether to use 3rd party services, such as CircleCI and AppVeyor, instead. Jenkins provides more flexibility (especially with respect to the supported architectures and operating systems), but at the expense of greater development and maintenance costs — that is, developer time that could otherwise be invested in improving GHC itself. In principle, the use of CircleCI and AppVeyor minimises the work needed to set up and maintain the infrastructure, but at the cost of being dependent on those 3rd parties, including their choice of directly supported architectures and operating systems.
Other key requirements involve security and the ability for anyone that forks GHC to also trivially fork and then modify the build infrastructure at will. For a summary of the requirements as well as the pros and cons of the two alternative approaches, have a look at the CI Trac Wiki page.
Lowering the barrier to entry
Although only a limited number of developers will feel confident in, say, extending GHC’s type checker, there are many parts of the compiler and associated tools and libraries that are well within reach of any competent Haskell developer. Hence, we feel that —just like other prominent open-source projects— we should make it as easy as possible to build, modify, and contribute to GHC. For better or worse, today, the gold standard for source control and processing code contributions is GitHub — if only, because virtually every professional developer, especially if engaged in open source work, is already familiar with it.
In contrast, GHC currently requires contributors to use the Phabricator tool. This is not only unfamiliar to most, but also requires the local installation of the command line tool Arcanist. In addition, Phabricator requires maintaining our own Phabricator installation and is known to be cumbersome to integrate with CI tool chains (tying this in with the first goal).
Lowering the barrier to entry involves other changes too of course (e.g., documentation structure). But to start with, what we are discussing is an attempt at encouraging more contributions while simultaneously lowering our set up and maintenance costs. This may well involve moving from Phabricator to GitHub.
Transparency and contributions
If you are interested in the details of the discussion, please have a look at the ghc-dev-ops@haskell.org archives. To provide transparency to the wider GHC user and developer community, all discussions of the GHC DevOps Group will be recorded on that mailing list.
Please let us know what you think. Feel free to approach any member of the GHC DevOps Group with feedback or suggestions. For a broader discussion, you may want to follow up on the general ghc-devs mailing list.
All this requires resources: time and money. To make this work, we will need significant contributions from companies that get value from GHC (which is itself free). But in exchange we get something valuable: a GHC ecosystem that we can rely on. If you think your company could help, in cash or kind, please get in touch.
is the product of the predecessors ![{[n,...,1]}](https://s0.wp.com/latex.php?latex=%7B%5Bn%2C...%2C1%5D%7D&bg=ffffff&fg=000000&s=0 "{[n,...,1]}")
of 
. The predecessors can be computed with an unfold: ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{preds} &::& \mathit{Integer} \rightarrow [\mathit{Integer}] \\ \mathit{preds} &=& \mathit{unfoldr}\;\mathit{step} \; \mathbf{where} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{step}\;0 &=& \mathit{Nothing} \\ \mathit{step}\;n &=& \mathit{Just}\;(n, n-1) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bpreds%7D+%26%3A%3A%26+%5Cmathit%7BInteger%7D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bpreds%7D+%26%3D%26+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bstep%7D+%5C%3B+%5Cmathbf%7Bwhere%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bstep%7D%5C%3B0+%26%3D%26+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Bstep%7D%5C%3Bn+%26%3D%26+%5Cmathit%7BJust%7D%5C%3B%28n%2C+n-1%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{preds} &::& \mathit{Integer} \rightarrow [\mathit{Integer}] \\ \mathit{preds} &=& \mathit{unfoldr}\;\mathit{step} \; \mathbf{where} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{step}\;0 &=& \mathit{Nothing} \\ \mathit{step}\;n &=& \mathit{Just}\;(n, n-1) \end{array} \end{array}")
![\displaystyle \begin{array}{@{}lcl@{}} \mathit{prod} &::& [\mathit{Integer}] \rightarrow \mathit{Integer} \\ \mathit{prod} &=& \mathit{foldr}\;(\times)\;1 \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bprod%7D+%26%3A%3A%26+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5Cmathit%7BInteger%7D+%5C%5C+%5Cmathit%7Bprod%7D+%26%3D%26+%5Cmathit%7Bfoldr%7D%5C%3B%28%5Ctimes%29%5C%3B1+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{prod} &::& [\mathit{Integer}] \rightarrow \mathit{Integer} \\ \mathit{prod} &=& \mathit{foldr}\;(\times)\;1 \end{array}")
to reformat a list of lists to a given length;
to sort a list;
to convert a fraction from base 
to base 
;
to encode a text in binary by “arithmetic coding”.
![\displaystyle \begin{array}{ll} & \mathit{factorial}\;0 \\ = & \qquad \{ \mathit{factorial} \} \\ & \mathit{prod}\;(\mathit{preds}\;0) \\ = & \qquad \{ \mathit{preds} \} \\ & \mathit{prod}\;[\,] \\ = & \qquad \{ \mathit{prod} \} \\ & 1 \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5Cmathit%7Bfactorial%7D%5C%3B0+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmathit%7Bfactorial%7D+%5C%7D+%5C%5C+%26+%5Cmathit%7Bprod%7D%5C%3B%28%5Cmathit%7Bpreds%7D%5C%3B0%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmathit%7Bpreds%7D+%5C%7D+%5C%5C+%26+%5Cmathit%7Bprod%7D%5C%3B%5B%5C%2C%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmathit%7Bprod%7D+%5C%7D+%5C%5C+%26+1+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & \mathit{factorial}\;0 \\ = & \qquad \{ \mathit{factorial} \} \\ & \mathit{prod}\;(\mathit{preds}\;0) \\ = & \qquad \{ \mathit{preds} \} \\ & \mathit{prod}\;[\,] \\ = & \qquad \{ \mathit{prod} \} \\ & 1 \end{array}")
: ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{foldl} &::& (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta \\ \mathit{foldl}\;f\;b\;(a:x) &=& \mathit{foldl}\;f\;(f\;b\;a)\;x \\ \mathit{foldl}\;f\;b\;[\,] &=& b \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bfoldl%7D+%26%3A%3A%26+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5Cbeta+%5C%5C+%5Cmathit%7Bfoldl%7D%5C%3Bf%5C%3Bb%5C%3B%28a%3Ax%29+%26%3D%26+%5Cmathit%7Bfoldl%7D%5C%3Bf%5C%3B%28f%5C%3Bb%5C%3Ba%29%5C%3Bx+%5C%5C+%5Cmathit%7Bfoldl%7D%5C%3Bf%5C%3Bb%5C%3B%5B%5C%2C%5D+%26%3D%26+b+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{foldl} &::& (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta \\ \mathit{foldl}\;f\;b\;(a:x) &=& \mathit{foldl}\;f\;(f\;b\;a)\;x \\ \mathit{foldl}\;f\;b\;[\,] &=& b \end{array}")
![\displaystyle \begin{array}{@{}lcl@{}} \mathit{unfoldr} &::& (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow \beta \rightarrow [\gamma] \\ \mathit{unfoldr}\;g\;b &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{unfoldr}\;g\;b' \\ \mathit{Nothing} &\rightarrow& [\,] \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bunfoldr%7D+%26%3A%3A%26+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D+%5C%5C+%5Cmathit%7Bunfoldr%7D%5C%3Bg%5C%3Bb+%26%3D%26+%5Cmathbf%7Bcase%7D%5C%3Bg%5C%3Bb%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BJust%7D%5C%3B%28c%2Cb%27%29+%26%5Crightarrow%26+c+%3A+%5Cmathit%7Bunfoldr%7D%5C%3Bg%5C%3Bb%27+%5C%5C+%5Cmathit%7BNothing%7D+%26%5Crightarrow%26+%5B%5C%2C%5D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{unfoldr} &::& (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow \beta \rightarrow [\gamma] \\ \mathit{unfoldr}\;g\;b &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{unfoldr}\;g\;b' \\ \mathit{Nothing} &\rightarrow& [\,] \end{array} \end{array}")
![\displaystyle \begin{array}{l} \mathit{meta} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma] \\ \mathit{meta}\;g\;f\;b = \mathit{unfoldr}\;g \cdot \mathit{foldl}\;f\;b \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bl%7D+%5Cmathit%7Bmeta%7D+%3A%3A+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5B%5Cgamma%5D+%5C%5C+%5Cmathit%7Bmeta%7D%5C%3Bg%5C%3Bf%5C%3Bb+%3D+%5Cmathit%7Bunfoldr%7D%5C%3Bg+%5Ccdot+%5Cmathit%7Bfoldl%7D%5C%3Bf%5C%3Bb+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{l} \mathit{meta} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma] \\ \mathit{meta}\;g\;f\;b = \mathit{unfoldr}\;g \cdot \mathit{foldl}\;f\;b \end{array}")
![{[A]}](https://s0.wp.com/latex.php?latex=%7B%5BA%5D%7D&bg=ffffff&fg=000000&s=0 "{[A]}")
to output of type ![{[C]}](https://s0.wp.com/latex.php?latex=%7B%5BC%5D%7D&bg=ffffff&fg=000000&s=0 "{[C]}")
: in the first phase, 
, it consumes all the input into an intermediate value of type 
; in the second phase, 
, it produces all the output.
function as follows: ![\displaystyle \begin{array}{@{}lcl@{}} \multicolumn{3}{@{}l}{\mathit{stream} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma]} \\ \mathit{stream}\;g\;f\;b\;x &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{stream}\;g\;f\;b'\;x \\ \mathit{Nothing} &\rightarrow& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} a:x' &\rightarrow& \mathit{stream}\;g\;f\;(f\;b\;a)\;x' \\ {[\,]} &\rightarrow& [\,] \end{array} \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmulticolumn%7B3%7D%7B%40%7B%7Dl%7D%7B%5Cmathit%7Bstream%7D+%3A%3A+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5B%5Cgamma%5D%7D+%5C%5C+%5Cmathit%7Bstream%7D%5C%3Bg%5C%3Bf%5C%3Bb%5C%3Bx+%26%3D%26+%5Cmathbf%7Bcase%7D%5C%3Bg%5C%3Bb%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BJust%7D%5C%3B%28c%2Cb%27%29+%26%5Crightarrow%26+c+%3A+%5Cmathit%7Bstream%7D%5C%3Bg%5C%3Bf%5C%3Bb%27%5C%3Bx+%5C%5C+%5Cmathit%7BNothing%7D+%26%5Crightarrow%26+%5Cmathbf%7Bcase%7D%5C%3Bx%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+a%3Ax%27+%26%5Crightarrow%26+%5Cmathit%7Bstream%7D%5C%3Bg%5C%3Bf%5C%3B%28f%5C%3Bb%5C%3Ba%29%5C%3Bx%27+%5C%5C+%7B%5B%5C%2C%5D%7D+%26%5Crightarrow%26+%5B%5C%2C%5D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \multicolumn{3}{@{}l}{\mathit{stream} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma]} \\ \mathit{stream}\;g\;f\;b\;x &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{stream}\;g\;f\;b'\;x \\ \mathit{Nothing} &\rightarrow& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} a:x' &\rightarrow& \mathit{stream}\;g\;f\;(f\;b\;a)\;x' \\ {[\,]} &\rightarrow& [\,] \end{array} \end{array} \end{array}")
. It maintains a current state 
, which is like the body of an unfold; this may produce a first element 
; when it yields no element, the next element 
of the input is consumed using function 
, which is like the body of a 
. From here we have two choices: we can either produce the output 
; or we can consume first to get the intermediate state 
, and again try to produce. The streaming condition says that this intermediate state 
.![{\mathit{meta}\;\mathit{uncons}\;(\mathbin{{+}\!\!\!{+}})\;[\,]}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Bmeta%7D%5C%3B%5Cmathit%7Buncons%7D%5C%3B%28%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D%29%5C%3B%5B%5C%2C%5D%7D&bg=ffffff&fg=000000&s=0 "{\mathit{meta}\;\mathit{uncons}\;(\mathbin{{+}\!\!\!{+}})\;[\,]}")
, where ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{uncons}\;x &=& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} [\,] &\rightarrow& \mathit{Nothing} \\ c:x' &\rightarrow& \mathit{Just}\;(c,x') \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Buncons%7D%5C%3Bx+%26%3D%26+%5Cmathbf%7Bcase%7D%5C%3Bx%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5B%5C%2C%5D+%26%5Crightarrow%26+%5Cmathit%7BNothing%7D+%5C%5C+c%3Ax%27+%26%5Crightarrow%26+%5Cmathit%7BJust%7D%5C%3B%28c%2Cx%27%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{uncons}\;x &=& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} [\,] &\rightarrow& \mathit{Nothing} \\ c:x' &\rightarrow& \mathit{Just}\;(c,x') \end{array} \end{array}")
, so 
as a 
and 
(as you may check), so ![{\mathit{regroup}\;n = \mathit{meta}\;(\mathit{chunk}\;n)\;(\mathbin{{+}\!\!\!{+}})\;[\,]}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Bregroup%7D%5C%3Bn+%3D+%5Cmathit%7Bmeta%7D%5C%3B%28%5Cmathit%7Bchunk%7D%5C%3Bn%29%5C%3B%28%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D%29%5C%3B%5B%5C%2C%5D%7D&bg=ffffff&fg=000000&s=0 "{\mathit{regroup}\;n = \mathit{meta}\;(\mathit{chunk}\;n)\;(\mathbin{{+}\!\!\!{+}})\;[\,]}")
where ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{chunk}\;n\;[\,] &=& \mathit{Nothing} \\ \mathit{chunk}\;n\;x &=& \mathit{Just}\;(\mathit{splitAt}\;n\;x) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bchunk%7D%5C%3Bn%5C%3B%5B%5C%2C%5D+%26%3D%26+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Bchunk%7D%5C%3Bn%5C%3Bx+%26%3D%26+%5Cmathit%7BJust%7D%5C%3B%28%5Cmathit%7BsplitAt%7D%5C%3Bn%5C%3Bx%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{chunk}\;n\;[\,] &=& \mathit{Nothing} \\ \mathit{chunk}\;n\;x &=& \mathit{Just}\;(\mathit{splitAt}\;n\;x) \end{array}")
yields 
where 
, with 
when 
and 
otherwise). This transforms an input list of lists into an output list of lists, where each output `chunk’ except perhaps the last has length 
, but it doesn’t quite work with the formulation so far. The problem is that 
is too aggressive, and will produce short chunks when there is still some input to consume. (Indeed, the streaming condition does not for 
—why not?) One might try the more cautious producer 
: 
![\displaystyle \begin{array}{@{}lcl@{}} \multicolumn{3}{@{}l@{}}{\mathit{fstream} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma]} \\ \mathit{fstream}\;g\;h\;f\;b\;x &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{fstream}\;g\;h\;f\;b'\;x \\ \mathit{Nothing} &\rightarrow& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} a:x' &\rightarrow& \mathit{fstream}\;g\;h\;f\;(f\;b\;a)\;x' \\ {[\,]} &\rightarrow& h\;b \end{array} \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmulticolumn%7B3%7D%7B%40%7B%7Dl%40%7B%7D%7D%7B%5Cmathit%7Bfstream%7D+%3A%3A+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5B%5Cgamma%5D%7D+%5C%5C+%5Cmathit%7Bfstream%7D%5C%3Bg%5C%3Bh%5C%3Bf%5C%3Bb%5C%3Bx+%26%3D%26+%5Cmathbf%7Bcase%7D%5C%3Bg%5C%3Bb%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BJust%7D%5C%3B%28c%2Cb%27%29+%26%5Crightarrow%26+c+%3A+%5Cmathit%7Bfstream%7D%5C%3Bg%5C%3Bh%5C%3Bf%5C%3Bb%27%5C%3Bx+%5C%5C+%5Cmathit%7BNothing%7D+%26%5Crightarrow%26+%5Cmathbf%7Bcase%7D%5C%3Bx%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+a%3Ax%27+%26%5Crightarrow%26+%5Cmathit%7Bfstream%7D%5C%3Bg%5C%3Bh%5C%3Bf%5C%3B%28f%5C%3Bb%5C%3Ba%29%5C%3Bx%27+%5C%5C+%7B%5B%5C%2C%5D%7D+%26%5Crightarrow%26+h%5C%3Bb+%5Cend%7Barray%7D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \multicolumn{3}{@{}l@{}}{\mathit{fstream} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\gamma]} \\ \mathit{fstream}\;g\;h\;f\;b\;x &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{fstream}\;g\;h\;f\;b'\;x \\ \mathit{Nothing} &\rightarrow& \mathbf{case}\;x\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} a:x' &\rightarrow& \mathit{fstream}\;g\;h\;f\;(f\;b\;a)\;x' \\ {[\,]} &\rightarrow& h\;b \end{array} \end{array} \end{array}")
![{h :: \beta \rightarrow [\gamma]}](https://s0.wp.com/latex.php?latex=%7Bh+%3A%3A+%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D%7D&bg=ffffff&fg=000000&s=0 "{h :: \beta \rightarrow [\gamma]}")
; when the cautious producer 
to flush out the remaining output elements from the state. Clearly, specializing to ![{h\;b=[\,]}](https://s0.wp.com/latex.php?latex=%7Bh%5C%3Bb%3D%5B%5C%2C%5D%7D&bg=ffffff&fg=000000&s=0 "{h\;b=[\,]}")
retrieves the original ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{apo} &::& (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow \beta \rightarrow [\gamma] \\ \mathit{apo}\;g\;h\;b &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{apo}\;g\;h\;b' \\ \mathit{Nothing} &\rightarrow& h\;b \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bapo%7D+%26%3A%3A%26+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D+%5C%5C+%5Cmathit%7Bapo%7D%5C%3Bg%5C%3Bh%5C%3Bb+%26%3D%26+%5Cmathbf%7Bcase%7D%5C%3Bg%5C%3Bb%5C%3B%5Cmathbf%7Bof%7D+%5C%5C+%26+%26+%5Cquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BJust%7D%5C%3B%28c%2Cb%27%29+%26%5Crightarrow%26+c+%3A+%5Cmathit%7Bapo%7D%5C%3Bg%5C%3Bh%5C%3Bb%27+%5C%5C+%5Cmathit%7BNothing%7D+%26%5Crightarrow%26+h%5C%3Bb+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{apo} &::& (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow \beta \rightarrow [\gamma] \\ \mathit{apo}\;g\;h\;b &=& \mathbf{case}\;g\;b\;\mathbf{of} \\ & & \quad \begin{array}[t]{@{}lcl@{}} \mathit{Just}\;(c,b') &\rightarrow& c : \mathit{apo}\;g\;h\;b' \\ \mathit{Nothing} &\rightarrow& h\;b \end{array} \end{array}")
behaves like 
![\displaystyle \begin{array}{@{}lcl@{}} \mathit{regroup}\;n\;\mathit{xs} &=& \mathit{fmeta}\;(\mathit{chunk'}\;n)\;(\mathit{unfoldr}\;(\mathit{chunk}\;n))\;(\mathbin{{+}\!\!\!{+}})\;[\,]\;\mathit{xs} \\ &=& \mathit{fstream}\;(\mathit{chunk'}\;n)\;(\mathit{unfoldr}\;(\mathit{chunk}\;n))\;(\mathbin{{+}\!\!\!{+}})\;[\,]\;\mathit{xs} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bregroup%7D%5C%3Bn%5C%3B%5Cmathit%7Bxs%7D+%26%3D%26+%5Cmathit%7Bfmeta%7D%5C%3B%28%5Cmathit%7Bchunk%27%7D%5C%3Bn%29%5C%3B%28%5Cmathit%7Bunfoldr%7D%5C%3B%28%5Cmathit%7Bchunk%7D%5C%3Bn%29%29%5C%3B%28%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D%29%5C%3B%5B%5C%2C%5D%5C%3B%5Cmathit%7Bxs%7D+%5C%5C+%26%3D%26+%5Cmathit%7Bfstream%7D%5C%3B%28%5Cmathit%7Bchunk%27%7D%5C%3Bn%29%5C%3B%28%5Cmathit%7Bunfoldr%7D%5C%3B%28%5Cmathit%7Bchunk%7D%5C%3Bn%29%29%5C%3B%28%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D%29%5C%3B%5B%5C%2C%5D%5C%3B%5Cmathit%7Bxs%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{regroup}\;n\;\mathit{xs} &=& \mathit{fmeta}\;(\mathit{chunk'}\;n)\;(\mathit{unfoldr}\;(\mathit{chunk}\;n))\;(\mathbin{{+}\!\!\!{+}})\;[\,]\;\mathit{xs} \\ &=& \mathit{fstream}\;(\mathit{chunk'}\;n)\;(\mathit{unfoldr}\;(\mathit{chunk}\;n))\;(\mathbin{{+}\!\!\!{+}})\;[\,]\;\mathit{xs} \end{array}")
: the streaming condition does hold for 
, and once the input has been exhausted, the process can switch to the more aggressive 
will never get started, but the ![\displaystyle \begin{array}{@{}lcl@{}} \mathit{fromBase3} &=& \mathit{foldr}\;\mathit{stepr}\;0 \quad \mathbf{where}\;\mathit{stepr}\;d\;x = (d+x)/3 \\ \mathit{toBase7} &=& \mathit{unfoldr}\;\mathit{next} \quad \mathbf{where}\; \begin{array}[t]{@{}lcl@{}} \mathit{next}\;0 &=& \mathit{Nothing} \\ \mathit{next}\;x &=& \mathbf{let}\;y=7\times x\;\mathbf{in}\;\mathit{Just}\;(\lfloor y\rfloor, y-\lfloor y\rfloor) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BfromBase3%7D+%26%3D%26+%5Cmathit%7Bfoldr%7D%5C%3B%5Cmathit%7Bstepr%7D%5C%3B0+%5Cquad+%5Cmathbf%7Bwhere%7D%5C%3B%5Cmathit%7Bstepr%7D%5C%3Bd%5C%3Bx+%3D+%28d%2Bx%29%2F3+%5C%5C+%5Cmathit%7BtoBase7%7D+%26%3D%26+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bnext%7D+%5Cquad+%5Cmathbf%7Bwhere%7D%5C%3B+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bnext%7D%5C%3B0+%26%3D%26+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Bnext%7D%5C%3Bx+%26%3D%26+%5Cmathbf%7Blet%7D%5C%3By%3D7%5Ctimes+x%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7BJust%7D%5C%3B%28%5Clfloor+y%5Crfloor%2C+y-%5Clfloor+y%5Crfloor%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{fromBase3} &=& \mathit{foldr}\;\mathit{stepr}\;0 \quad \mathbf{where}\;\mathit{stepr}\;d\;x = (d+x)/3 \\ \mathit{toBase7} &=& \mathit{unfoldr}\;\mathit{next} \quad \mathbf{where}\; \begin{array}[t]{@{}lcl@{}} \mathit{next}\;0 &=& \mathit{Nothing} \\ \mathit{next}\;x &=& \mathbf{let}\;y=7\times x\;\mathbf{in}\;\mathit{Just}\;(\lfloor y\rfloor, y-\lfloor y\rfloor) \end{array} \end{array}")
is of the wrong kind; but we have also 
can be seen as a defunctionalized representation of the function 
, and 
applies this function to 
: 
![\displaystyle \begin{array}{@{}lcl@{}} \mathit{toBase7} \cdot \mathit{extract} &=& \mathit{unfoldr}\;\mathit{next'} \quad \mathbf{where}\; \begin{array}[t]{@{}lcl@{}} \mathit{next'}\;(0,v) &=& \mathit{Nothing} \\ \mathit{next'}\;(u,v) &=& \begin{array}[t]{@{}l} \mathbf{let}\;y = \lfloor{7 \times u \times v}\rfloor\;\mathbf{in} \\ \mathit{Just}\;(y,(u - y/(v \times 7), v \times 7)) \end{array} \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7BtoBase7%7D+%5Ccdot+%5Cmathit%7Bextract%7D+%26%3D%26+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bnext%27%7D+%5Cquad+%5Cmathbf%7Bwhere%7D%5C%3B+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlcl%40%7B%7D%7D+%5Cmathit%7Bnext%27%7D%5C%3B%280%2Cv%29+%26%3D%26+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Bnext%27%7D%5C%3B%28u%2Cv%29+%26%3D%26+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathbf%7Blet%7D%5C%3By+%3D+%5Clfloor%7B7+%5Ctimes+u+%5Ctimes+v%7D%5Crfloor%5C%3B%5Cmathbf%7Bin%7D+%5C%5C+%5Cmathit%7BJust%7D%5C%3B%28y%2C%28u+-+y%2F%28v+%5Ctimes+7%29%2C+v+%5Ctimes+7%29%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}lcl@{}} \mathit{toBase7} \cdot \mathit{extract} &=& \mathit{unfoldr}\;\mathit{next'} \quad \mathbf{where}\; \begin{array}[t]{@{}lcl@{}} \mathit{next'}\;(0,v) &=& \mathit{Nothing} \\ \mathit{next'}\;(u,v) &=& \begin{array}[t]{@{}l} \mathbf{let}\;y = \lfloor{7 \times u \times v}\rfloor\;\mathbf{in} \\ \mathit{Just}\;(y,(u - y/(v \times 7), v \times 7)) \end{array} \end{array} \end{array}")
and 
. For example, 
, but 
, so it is premature to produce the first digit 2 in base 7 having consumed only the first digit 1 in base 3. The producer 
and 
. If these both start with the same digit in base 7, then (and only then) is it safe to produce that digit. So we define 
(as you may check), and therefore 
Erik Meijer
(agent ‘a’ believes A)![[\alpha] A](https://s0.wp.com/latex.php?latex=%5B%5Calpha%5D+A&bg=ffffff&fg=000000&s=0 "[\alpha] A")
(A holds true after action 
).
– multiples of 3 in binary.
![[-] : 2^{\textsf{Pom}_{\Sigma}}](https://s0.wp.com/latex.php?latex=%5B-%5D+%3A+2%5E%7B%5Ctextsf%7BPom%7D_%7B%5CSigma%7D%7D&bg=ffffff&fg=000000&s=0 "[-] : 2^{\textsf{Pom}_{\Sigma}}")
.
then terminates.
not 
. (I wasn’t sure if this was an open question or whether there was a solution in this paper).
, e.g., scan [1,2,3,4] = [1,3,6,10]
is a 4-vector.
. This work shows the formal relation (that indeed these two systems are equivalent). A proof is partially given in Geuvers ’93, but a full Coq formalisation was given by Kaiser, Tebbi and Smolka at POPL 2017. In this work, the proof is replayed across three tools to provide a useful comparison of the three systems: Coq, Abella and Beluga.
in PTS can correspond to 
and 
. Have to also keep track of context assumptions. One (of many) “topics of interest” in this comparison is how to manage contexts (which is interesting to me as I am quite interested in CMTT in Beluga).
that gives it meaning ![[\Gamma \vdash K]](https://s0.wp.com/latex.php?latex=%5B%5CGamma+%5Cvdash+K%5D&bg=ffffff&fg=000000&s=0 "[\Gamma \vdash K]")
. There is no concept of free variable., e.g., in Coq 
is provable but in Belluga 
is ![\textsf{scale} \; (c : \mathbb{R}) \; (n : [\textsf{abs} \; c] \mathbb{R}) : \mathbb{R}](https://s0.wp.com/latex.php?latex=%5Ctextsf%7Bscale%7D+%5C%3B+%28c+%3A+%5Cmathbb%7BR%7D%29+%5C%3B+%28n+%3A+%5B%5Ctextsf%7Babs%7D+%5C%3B+c%5D+%5Cmathbb%7BR%7D%29+%3A+%5Cmathbb%7BR%7D&bg=ffffff&fg=000000&s=0 "\textsf{scale} \; (c : \mathbb{R}) \; (n : [\textsf{abs} \; c] \mathbb{R}) : \mathbb{R}")
for some startup cost 
and 
iterations and 
a cost for the loop. You might then collect some results and do linear regression (best fist line) to see if this model is confirmed. Bayesian linear regression gives you many lines for different kinds of fit.
observations into a replication like combination (
where 
is above 
and 
(partial expressions). Forward slicing preserves meets in the lattice; backward slicing should be consistent and minimal with respect to forward slicing (
and 
which form a Galois connection, i.e., 
. [Given one of the slicings we don’t necessarily get the other for free].
; (!l1, !l)
. For example, take 
and 
to be notions of program equivalence (equivalent inputs produce equivalent outputs). Another relation might be in information-flow security where relations 
mean “these two programs are low-level equivalent” (low-security).![S(Y_!, Y_@) = Pr[Y_1] \leq e^\epsilon Pr[Y_2]](https://s0.wp.com/latex.php?latex=S%28Y_%21%2C+Y_%40%29+%3D+Pr%5BY_1%5D+%5Cleq+e%5E%5Cepsilon+Pr%5BY_2%5D&bg=ffffff&fg=000000&s=0 "S(Y_!, Y_@) = Pr[Y_1] \leq e^\epsilon Pr[Y_2]")
.
(giving an upper bound computed in terms of the inputs and underlying relations). This is useful for guaranteeing compile optimisations (not worse, or definitely better), ruling out side-channel attacks (i.e., the ![\textsf{cost}(e[v_1/x]) - \textsf{cost}(e[v_2/x]) = 0](https://s0.wp.com/latex.php?latex=%5Ctextsf%7Bcost%7D%28e%5Bv_1%2Fx%5D%29+-+%5Ctextsf%7Bcost%7D%28e%5Bv_2%2Fx%5D%29+%3D+0&bg=ffffff&fg=000000&s=0 "\textsf{cost}(e[v_1/x]) - \textsf{cost}(e[v_2/x]) = 0")
, such that different inputs do not yield different costs thus information about the inputs is not leaked).
. Talk about relational properties of the input and relational properties of the output. Usually, if we interpret to relations then we want to prove soundness as: ![(\bar{v_1}, \bar{v_2}) \in [\Gamma] \Rightarrow ([t_1[\bar{v_1}/\Gamma]], t_2[\bar{v_2}/Gamma]]) \in [\tau]](https://s0.wp.com/latex.php?latex=%28%5Cbar%7Bv_1%7D%2C+%5Cbar%7Bv_2%7D%29+%5Cin+%5B%5CGamma%5D+%5CRightarrow+%28%5Bt_1%5B%5Cbar%7Bv_1%7D%2F%5CGamma%5D%5D%2C+t_2%5B%5Cbar%7Bv_2%7D%2FGamma%5D%5D%29+%5Cin+%5B%5Ctau%5D&bg=ffffff&fg=000000&s=0 "(\bar{v_1}, \bar{v_2}) \in [\Gamma] \Rightarrow ([t_1[\bar{v_1}/\Gamma]], t_2[\bar{v_2}/Gamma]]) \in [\tau]")
.\
where 
is the upper bound and 
is the lower bound execution cost, which are thought of as a unary effect. A relational judgement 
where 
is the upper bound on the relative cost of the two programs. The types have an annotation function type (like in normal effect systems) 
and data types for integers and lists have indices to express dependencies.
.
this can be refined (with the type ![n : \textsf{int}[5]](https://s0.wp.com/latex.php?latex=n+%3A+%5Ctextsf%7Bint%7D%5B5%5D&bg=ffffff&fg=000000&s=0 "n : \textsf{int}[5]")
in the indices, which will change the bound to $\vdash^{k+1}_{k+1}$.
.
.
.
captures lists which differ in less than 
and 
meaning 
has a relatively smaller cost. Plugging this into the higher-order function and doing the type derivation again gives a looser bound.
which contains term variable assertions 
and relational assertion 
. In the type system, some rules are synchronous (building up the related two terms with the same syntactic construct) or asynchronous (building up one of the terms).
is a monadic meta language with a specific cost effect (with 
introducing a cost. Intuition: if a term 
is closed and $m \Downarrow_n v$ then $m \cong \textsf{cstep}_n(v)$.We can define formulae in HOL which all us to reason about these explicit cost terms and their quantities: we can define what we need in the logic.
. Using the system , we can prove this property, using a suitable invariant/predicate over the input and output list(s).
.
(I forgot what the constant c was). This work introduces references and arrays to enable analysis of programs where resource consumption depends on the data stored in mutable structures (references and arrays).
that is it can contribute 
units of potential where 
across the two variables. Benjamin walked us through a nice example with appending to a list.
is the principle type of 
if 
and for all types 
such that 
there exists a substitution 
.
is inhabited by the K combinator 
but is not principally inhabited (
. Define relations on paths, 
as the minimal equivalence relation for a beta-normal term 
which defines an equivalence relation on paths of paths with common subpaths (capture constraints on subformulae on types).
(note the two occurrences of 
) where intersection is associative, commutative and (possibly) idempotent. In 1994, Gardner introduces a system which is not idempotent, where types are now multisets (rather than sets in the earlier formulations). This has the flavour of linear logic resources (
)
.
This has been used mainly to make termination arguments.
induces a multiset path order 
, (
if 
is 
, or 
some 
(recursive function to create a splay tree). A type system for this was shown, with cost annotation judgment (no time to copy down any details).
(Hillerstrom, Lindley 2016) – lambda calculus with effect handlers (separate syntactic category but contains lambda terms), row polymorphism, and monadic metalanguage style constructs for effectful let binding and ‘return’. The CPS translation is a homomorphism on all the lambda calculus syntax, but continuation passing on the effectful fragment (effectful let and return). One part of the interpretation for the effectful operation term: ![[[\textbf{do} \, l \, V]] = \lambda k . \lambda h . \; h (l \; \langle[[V]], \lambda x . k \; x \; h\rangle)](https://s0.wp.com/latex.php?latex=%5B%5B%5Ctextbf%7Bdo%7D+%5C%2C+l+%5C%2C+V%5D%5D+%3D+%5Clambda+k+.+%5Clambda+h+.+%5C%3B+h+%28l+%5C%3B+%5Clangle%5B%5BV%5D%5D%2C+%5Clambda+x+.+k+%5C%3B+x+%5C%3B+h%5Crangle%29&bg=ffffff&fg=000000&s=0 "[[\textbf{do} \, l \, V]] = \lambda k . \lambda h . \; h (l \; \langle[[V]], \lambda x . k \; x \; h\rangle)")
(
These can be used to express monotonicity properties, are syntax directed, and exploit structural similarities of code. However, say we want to prove the naturality of 
where 
is a binary predicate on properties of the two terms and ![\dfrac{\Gamma, x_1 : \sigma_1, x_2 : \sigma_2 \mid \Psi, \phi' \vdash t_1 : \tau_1 \sim t_2 : \tau_2 \mid \phi} {\Gamma \mid \Psi \vdash \lambda x_1 : t_1 : \sigma_1 \rightarrow \tau_1 \sim \lambda x_2 . t_2 : \sigma_2 \rightarrow \tau_2 \mid \forall x_1 . \phi' \Rightarrow \phi[r_1 x_1 / r_1, \, r_2 x_2 / r_2]}](https://s0.wp.com/latex.php?latex=%5Cdfrac%7B%5CGamma%2C+x_1+%3A+%5Csigma_1%2C+x_2+%3A+%5Csigma_2+%5Cmid+%5CPsi%2C+%5Cphi%27+%5Cvdash+t_1+%3A+%5Ctau_1+%5Csim+t_2+%3A+%5Ctau_2+%5Cmid+%5Cphi%7D+%7B%5CGamma+%5Cmid+%5CPsi+%5Cvdash+%5Clambda+x_1+%3A+t_1+%3A+%5Csigma_1+%5Crightarrow+%5Ctau_1+%5Csim+%5Clambda+x_2+.+t_2+%3A+%5Csigma_2+%5Crightarrow+%5Ctau_2+%C2%A0%5Cmid+%5Cforall+x_1+.+%5Cphi%27+%5CRightarrow+%5Cphi%5Br_1+x_1+%2F+r_1%2C+%5C%2C+r_2+x_2+%2F+r_2%5D%7D&bg=ffffff&fg=000000&s=0 "\dfrac{\Gamma, x_1 : \sigma_1, x_2 : \sigma_2 \mid \Psi, \phi' \vdash t_1 : \tau_1 \sim t_2 : \tau_2 \mid \phi} {\Gamma \mid \Psi \vdash \lambda x_1 : t_1 : \sigma_1 \rightarrow \tau_1 \sim \lambda x_2 . t_2 : \sigma_2 \rightarrow \tau_2 \mid \forall x_1 . \phi' \Rightarrow \phi[r_1 x_1 / r_1, \, r_2 x_2 / r_2]}")
.
? It depends on call-by-value, call-by-name, call-by-need, or full beta then you get different answers. The call-by-value, call-by-name, and call-by-need strategies are called weak because they do not reduce underneath lambda abstraction. As a consequence, they do not compute normal forms on their own.![t[v[u/y]/x] \rightarrow t[u/y][v/x]](https://s0.wp.com/latex.php?latex=t%5Bv%5Bu%2Fy%5D%2Fx%5D+%5Crightarrow+t%5Bu%2Fy%5D%5Bv%2Fx%5D&bg=ffffff&fg=000000&s=0 "t[v[u/y]/x] \rightarrow t[u/y][v/x]")
).
only when the number of reference to 
is less than or equal to 1 (so things don’t explode).
implies 
which can be provided by relational parametricity, see Reynolds “related things map to related things”, applies identity extension lemma).
is however 
. Suppose $B = U$ then we can leak details of the implementation (rerepresentation type is returned as data) 
(has this type). This violates the identity extension lemma used in the above proof for System F.
ill typed. The proof of parametricity for 
(cf Bernardy, Coquand, and Moulin 2015, on bridge/path-based proofs) which gives a basis for proving the core idea of “related things map to related things” where 
is connected with the type 
(in the above type) and 
is connected to the type 
via a switching term 
(see paper for the proof) (I think this is analogous to setting up a relation between 
, you can define 
.
but also 
. Intuition: sizes are irrelevant in terms, but relevant in types only.
, where sizes uses as indexes can be marked as irrelevant in the context. Here is one of the rules for type formation when abstracting over an irrelevantly typed argument:
for necessity (true without any hypotheses) 
(if something A is possible true then possibility can propagate to the context– doesn’t change the “possibleness”). Various intuitionistic substructural and modal logics/type systems: linear/affine, relevant, ordered, bunched (separation logic), coeffects, etc. Cohesive HoTT: take dependent type theory and add modalities (int, sharp, flat). S-Cohesion (Finster, Licata, Morehouse, Riley: a comonad and monad that themselves are adjoint, ends up with two kind of products which the modality maps between). Motivation: what are the common patterns in substructural and modal logics? How do we construct these things more systematically from a a small basic calculus.
which is modelled by 
. In the sequent calculus style, use the notion of context to form the type. Linear logic ! is similar (but with no weakening). The rules for 
follow the same kind of pattern: e.g., 
where the context “decays” into the logical operator (rather than being literally equivalent): the types inherent the properties of the context (cf. also exchange).
where 
the meaning of this sequent depends on the equations/inequations on the context descriptor:, e.g.,if you have associativity of 
then you get a relevant logic, etc. Bunched implication will have two kinds of nodes in the context descriptor. For a modality, unary function symbols, e.g. 
means that the left part of the context is wrapped by a modality.
where we have weakend in the sequent calculus but the context descriptor is unchanged (i.e., we can’t use 
to prove 
. All of the left rules become instances of one rule on F: ![\dfrac{\Gamma, \Delta \vdash_{\beta[\alpha / x]} B}{\Gamma, x : F_\alpha(\Delta) \vdash B}](https://s0.wp.com/latex.php?latex=%5Cdfrac%7B%5CGamma%2C+%5CDelta+%5Cvdash_%7B%5Cbeta%5B%5Calpha+%2F+x%5D%7D+B%7D%7B%5CGamma%2C+x+%3A+F_%5Calpha%28%5CDelta%29+%5Cvdash+B%7D&bg=ffffff&fg=000000&s=0 "\dfrac{\Gamma, \Delta \vdash_{\beta[\alpha / x]} B}{\Gamma, x : F_\alpha(\Delta) \vdash B}")
which gives you all your left-rules (a related dual rule gives the right sequent rules).
and 
where the first parameter is contravariant and second is covariant may have dinatural transformations between them. (Dinaturality is weaker than naturality). Yields a family of maps 
which separate the contravariant and covariant actions in the coherence condition (see 
and proofs/terms by dinautral transformations. Due to Girard, Scedrov, Scott 1992 there is the theorem that: if 
then 
-normal and (syntactically) dinatural then 
– this is a dinatural transformation and its dinaturality hexagon is representable by lambda terms.
then $n \leq h$, there are various others; see paper).
) of types in a universe 
every identification 
induces an (Id)-isomorphism 
. U is univalent “if all Id-isomorphisms 
” (want this expressed in type theory) (this is a simpler restating of Voevodsky’s original definition due to Licata, Shulman, et al.). This paper: towards answering, are there models for usual type theory which contain such univalent universes?
implies 
. Univalence is telling you that the notion of identification is richer subsuming ETT where there is an identification between two types then they are already equal, which is much smaller/thinner.
are paths from point 
in a space 
is a “constant path” (transporting along such a path does nothing to the element).
for these identifications, but we need to restrict to families of type 
carrying structure to guarantee substitution operations (in this DTT context). “Holes” is diagrams are filled using path reversals and path composition. Solution is “Moore” paths.
in 
and an extent function 
satisfying 
and 
. These paths have a reversal operator by truncated subtraction 
. (note this is idempotent on constant paths as required, allowing holes in square paths to be filled (I had to omit the details, too many diagrams)). But topological spaces don’t give us a model of MLTT, so they replace it by an arbitrary topos (modelling extensional type theory) and instead of 
for path length/shape use any totally ordered commutative ring. All the definition/properties of Moore paths are the expressed in the internal language of the topos. This successfully gives you a category with families (see Dybjer) modelling intensional Martin-Lof type theory (with Pi). This also satisfies dependent functional extensionality thus its probably a good model as univalence should imply extensionality. But haven’t yet got a proof that this does contain a univalence universe (todo).
[Ahmed, Findler, Siek, Wadler POPL’11] (fixed a few problems) and proves parametricity for it.![\lambda x . x + 1 : \ast \Rightarrow^p \forall X . X \rightarrow X) [int] 4](https://s0.wp.com/latex.php?latex=%5Clambda+x+.+x+%2B+1+%3A+%5Cast+%5CRightarrow%5Ep+%5Cforall+X+.+X+%5Crightarrow+X%29+%5Bint%5D+4&bg=ffffff&fg=000000&s=0 "\lambda x . x + 1 : \ast \Rightarrow^p \forall X . X \rightarrow X) [int] 4")
returns 5 but we want to raise a “blame” for the coercion 
here (coercing a monomorphic to polymorphic type is bad!).
(that is, casts to the dynamic type and back again cancel out).
(
this has a type that makes it look like a constant function 
. When executing this we want to raise blame rather than actually produce a value (e.g. for ![add 3 [\textsf{int}] 2](https://s0.wp.com/latex.php?latex=add+3+%5B%5Ctextsf%7Bint%7D%5D+2&bg=ffffff&fg=000000&s=0 "add 3 [\textsf{int}] 2")
). Solution: use runtime type generation rather than substitution for type variables.
provides a dictionary mapping type variables to types.![\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X]](https://s0.wp.com/latex.php?latex=%5CSigma+%5Crhd+%28%5CLambda+X+.+v%29+%5BB%5D+%5Cmapsto+%5CSigma%2C+%5Calpha+%3A%3D+B+%5Crhd+v%5B%5Calpha%2FX%5D&bg=ffffff&fg=000000&s=0 "\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X]")
i.e., instead of substituting the ![\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X] : A[\alpha/X] \Rightarrow^{+\alpha} A[B/X]](https://s0.wp.com/latex.php?latex=%5CSigma+%5Crhd+%28%5CLambda+X+.+v%29+%5BB%5D+%5Cmapsto+%5CSigma%2C+%5Calpha+%3A%3D+B+%5Crhd+v%5B%5Calpha%2FX%5D+%3A+A%5B%5Calpha%2FX%5D+%5CRightarrow%5E%7B%2B%5Calpha%7D+A%5BB%2FX%5D&bg=ffffff&fg=000000&s=0 "\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X] : A[\alpha/X] \Rightarrow^{+\alpha} A[B/X]")
where 
(
are tuples of the type-name stores, and relations about when concealed values should be related. See paper: also shows soundness of the logical relations wrt. contextual equivalence. There was some cool stuff with “concealing” that I missed really.
where 
defines type consistency. Idea: extend this to include notions of consistency between polymorphic and dynamic types. An initial attempt breaks conservativity since there are ill-typed System F terms which are well-typed in System Fg then.
– 
so that it can not be used inside of 
(term level) and 
(type level).
. But inference is highly non-trivial.
and 
(here the natural number has a size too).
. Then we need to find a concrete interpretation of 
.
</figure>
