John Launchbury
Simon L. Peyton Jones
ABSTRACT
Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.
The security of the encapsulation is assured by the type system, using parametricity. Intriguingly, this parametricity requires the provision of a (single) constant with a rank-2 polymorphic type.
- E Barendsen L~ JEW Smetsers {Dec 1993}, "Conventional and uniqueness typing in graph rewrite systems," in Proc 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, Springer Verlag LNCS. Google Scholar
Digital Library
- DK Gifford & JM Lucassen {Aug 1986}, "Integrating functional and imperative programming,'" in A CM Conference on Lisp and Functional Programming, MIT, ACM, 28-38. Google ScholarDigital Library
- J Launchbury{June 1993}, "Lazy imperative programming,' in Proc A CM Sigplan Workshop on State in Programming Languages, Copenhagen (available as YALEU/DCS/RR- 968, Yale University), pp46-56.Google Scholar
- J Launchbury Lc SL Peyton Jones{Feb 1994}, "Lazy functional state threads," Technical report FP- 94-05, Department of Computing Science, University of Glasgow (FTP:ftp. dcs. glasgow, ac. uk: pub/glasgow-fp/tech-report s / FP-94-05: sta~e, ps. Z).Google Scholar
- NJ McCracken {June 1984}, "The typechecking of programs with implicit type structure," in Semantics of data types, Springer Verlag LNCS 173, 301-315. Google ScholarDigital Library
- JC Mitchell & AR Meyer {1985}, "Second-order logical relations," in Logics of Programs, R Parikh, ed., Springer Verlag LNCS 193. Google ScholarDigital Library
- Rishiyur Nikhil{March 1988}, "Id Reference Manual," Lab for Computer Sci, MIT.Google Scholar
- M Odersky, D Rabin & P Hudak{Jan 1993}, "Call by name, assignment, and the lambda calculus," in 20th A CM Symposium on Principles of Programming Languages, Charleston, ACM, 43- 56. Google ScholarDigital Library
- LC Paulson {1991}, ML for the working programmer, Cambridge University Press. Google ScholarDigital Library
- SL Peyton Jones L~ J Launchbury{Sept 1991}, "Unboxed values as first class citizens," in Functional Programming Languages and Computer Architecture, Boston, Hughes, ed., LNCS 523, Springer Verlag, 636-666. Google ScholarDigital Library
- SL Peyton Jones & PL Wadler {Jan 1993}, "Imperative functional programming," in 20th A CM Symposium on Principles of Programming Languages, Charleston, ACM, 71-84. Google ScholarDigital Library
- CG Ponder, PC McOeer & A P-C Ng {June 1988}, "Are applicative languages inefficient?," $iGPLAN Notices 23, 135-139. Google ScholarDigital Library
- DA Schmidt {Apr 1985}, "Detecting global variables in denotational specifications," TOPLAS 7, 299- 310. Google ScholarDigital Library
- V Swarup, US Reddy & E Ireland{Sept 1991}, "As~ signments for applicative languages," in Functional Programming Languages and Computer Architecture, Boston, Hughes, ed., LNCS 523, Springer Verlag, 192-214. Google ScholarDigital Library
- M Tofte{Nov 1990}, "Type inference for polymorphic references," information and Computation 89. Google ScholarDigital Library
Index Terms
- Lazy functional state threads
Recommendations
Lazy functional state threads
Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, ...
A Lazy Language Needs a Lazy Type System: Introducing Polymorphic Contexts
IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming LanguagesMost type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation.
First, ...
Automatic amortised analysis of dynamic memory allocation for lazy functional programs
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingThis paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and ...
Comments