# input-output-hk/plutus

This reverts commit 033df54.
 @@ -20,7 +20,6 @@ all: pdf pdf: ${PDF}${DOC}.pdf: ${SRC} -rm -f${DOC}.bbl ${DOC}.aux${LATEX} ${DOC}${BIBTEX} ${DOC}${LATEX} ${DOC} # to make sure the (cross)references are correct  @@ -42,7 +42,7 @@ \cksteps{\ckforward{s&}{\error{A}}&} {&\ckerror{}}\\ \\[-10pt] %% Put some vertical space between compute and return rules, but not a whole line \cksteps{\ckbackward{\cdot&}{V}&} {&\square V}\\ \cksteps{\ckbackward{s, \inInstLeftFrame{A}&}{\abs{\alpha}{K}{V}}&} {&\ckbackward{s}{V}}\\ \cksteps{\ckbackward{s, \inInstLeftFrame{A}&}{\abs{\alpha}{K}{M}}&} {&\ckforward{s}{M}}\\ \cksteps{\ckbackward{s, \inWrapRightFrame{A}{B}&}{V}&} {&\ckbackward{s}{\wrap{A}{B}{V}}}\\ \cksteps{\ckbackward{s, \inUnwrapFrame{}&}{\wrap{A}{B}{V}}&} {&\ckbackward{s}{V}}\\ \cksteps{\ckbackward{s, \inAppLeftFrame{N}&}{V}&} {&\ckforward{s, \inAppRightFrame{V}}{N}}\\  @@ -21,16 +21,6 @@ @book{Pierce:ATTAPL homepage = {http://www.cis.upenn.edu/~bcpierce/attapl} } @incollection{Pitts:typed-operational-reasoning, author={Pitts, A.M.}, title={Typed Operational Reasoning}, chapter=7, editor = {Benjamin C. Pierce}, booktitle = {Advanced Topics in Types and Programming Languages}, publisher = {MIT Press}, year = 2005 } @book{Harper:PFPL, author = {Harper, Robert}, title = {Practical Foundations for Programming Languages}, @@ -64,6 +54,8 @@ @article{Friedman-Lazy-Krivine issn = {1388-3690}, pages = {271--293}, numpages = {23}, url = {http://dx.doi.org/10.1007/s10990-007-9014-0}, doi = {10.1007/s10990-007-9014-0}, acmid = {1325155}, publisher = {Kluwer Academic Publishers}, address = {Hingham, MA, USA}, @@ -83,6 +75,8 @@ @article{Felleisen-Hieb issn = {0304-3975}, pages = {235--271}, numpages = {37}, url = {http://dx.doi.org/10.1016/0304-3975(92)90014-7}, doi = {10.1016/0304-3975(92)90014-7}, acmid = {136297}, publisher = {Elsevier Science Publishers Ltd.}, address = {Essex, UK}, @@ -108,7 +102,8 @@ @inproceedings{reynolds-type-structure volume = {19}, series = {Lecture Notes in Computer Science}, month = apr, publisher = {Springer} publisher = {Springer}, url = {http://www.springerlink.com/content/p5801737k78207p7/} } @unpublished{Scott-encoding, @@ -125,10 +120,13 @@ @inproceedings{Koopman:2014 booktitle = {Proceedings of the 26Nd 2014 International Symposium on Implementation and Application of Functional Languages}, series = {IFL '14}, year = {2014}, isbn = {978-1-4503-3284-2}, location = {Boston, MA, USA}, pages = {4:1--4:12}, articleno = {4}, numpages = {12}, url = {http://doi.acm.org/10.1145/2746325.2746330}, doi = {10.1145/2746325.2746330}, acmid = {2746330}, publisher = {ACM}, address = {New York, NY, USA}, @@ -148,6 +146,8 @@ @article{Ahmed:2017 pages = {39:1--39:28}, articleno = {39}, numpages = {28}, url = {http://doi.acm.org/10.1145/3110283}, doi = {10.1145/3110283}, acmid = {3110283}, publisher = {ACM}, address = {New York, NY, USA}, @@ -181,9 +181,12 @@ @inproceedings{Yakushev2009 booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP '09}, year = {2009}, isbn = {978-1-60558-332-7}, location = {Edinburgh, Scotland}, pages = {233--244}, numpages = {12}, url = {http://doi.acm.org/10.1145/1596550.1596585}, doi = {10.1145/1596550.1596585}, acmid = {1596585}, publisher = {ACM}, address = {New York, NY, USA}, @@ -195,6 +198,7 @@ @book{Princeton-bitcoin-book author = {Narayanan, Arvind and Bonneau, Joseph and Felten, Edward and Miller, Andrew and Goldfeder, Steven}, title = {Bitcoin and Cryptocurrency Technologies: A Comprehensive Introduction}, year = {2016}, isbn = {0691171696, 9780691171692}, publisher = {Princeton University Press}, address = {Princeton, NJ, USA}, } @@ -229,18 +233,3 @@ @article{Zahnentferner18-UTxO } @inproceedings{compiling-to-fomega-2019, author = {Roman Kireev and Chad Nester and Michael Peyton Jones and Philip Wadler and Vasilis Gkoumas and Kenneth {MacKenzie}}, title = {Unraveling recursion: compiling an {IR} with recursion to {System~$F$}}, booktitle = {Proceedings of MPC 2019}, year={2019}, note = {To appear} } @inproceedin{system-F-in-Agda, author = {James Chapman and Roman Kireev and Chad Nester and Philip Wadler}, title = {{System~$F$} in {Agda}, for fun and profit}, booktitle = {Proceedings of MPC 2019}, year={2019}, note = {To appear} }  @@ -448,18 +448,16 @@ \subsubsection{Recursive types} Plutus Core: \texttt{ifix A B} is a type such that \texttt{ifix A B$\cong\$ A (ifix A) B} where \texttt{A} is a \textit{pattern functor}~\citep[2.4]{backhouseetal98} and \texttt{B} is an index. Pattern functors that \texttt{ifix} receives bind two variables: one for building recursive occurrences and the other to act as an index. Indices can be used in order to get parameterised data types, but also in order to control the shape of the data type: depending on an index, recursive occurrences can be instantiated differently. This allows us to encode a wide variety of data types, including non-regular and mutually recursive data types.% \blue{\footnote{\blue{We could do with more detail (or perhaps an example) here, since it'll be much more difficult for the reader to work out what's going on than with standard \texttt{fix}. Is the compilation paper sufficient?}}} See~\cite{compiling-to-fomega-2019} for more details. index. Pattern functors that \texttt{ifix} receives bind two variables: one for building recursive occurrences and the other to act as an index. Indices can be used in order to get parameterised data types, but also in order to control the shape of the data type: depending on an index, recursive occurrences can be instantiated differently. This allows us to encode a wide variety of data types, including non-regular and mutually recursive data types\blue{\footnote{\blue{We could do with more detail (or perhaps an example) here, since it'll be much more difficult for the reader to work out what's going on than with standard \texttt{fix}. With luck we'll soon have a publication to refer to.}}}. Note that we have an \textit{isomporhism} of types here rather than equality: fixpoint types are @@ -499,10 +497,8 @@ \subsubsection{The value restriction} number of difficulties. For example, Standard ML's value restriction is required to avoid a number of problems when (implicit) type abstractions include non-values; other issues are explored in~\citep[2.4]{Ahmed:2017} and~\citep[7.4.1]{Pitts:typed-operational-reasoning}. Plutus Core's restriction to values avoids these problems and is not very onerous in practice. in~\citep[2.4]{Ahmed:2017}. Plutus Core's restriction to values avoids these problems and is not very onerous in practice. \section{Type Correctness}