FIML(ID:6256/)
Functional and Imperative ML
- Country: jp
- Began: 1992
- Published: 1993
- Type:Lazy Evaluation FPs
- Sammet:EXP
for Functional and Imperative ML
extension of ML based on the transformation calculus. Its type system is an extension to transformations of that defined in The typed polymorphic selective lambda-calculus.
People:
Related languages
References:
Transformation calculus and its typing. Jacques Garrigue. In Proc. of the workshop on Type Theory and its Applications to Computer Systems, pages 34-45. Kyoto University RIMS Lecture Notes 851, August 1993 view details
Abstract: Many calculi supporting a notion of state have been proposed. However this notion is nearly always based on the intuition of a store, that is a binding from name to values. The exception, monads, recently focused on for I/Os, suffers from its rigidity.
The transformation calculus, an extension of lambda calculus, shows another, more general way to do that. It is different from others in that no orthogonal reduction rule is added to $\beta$-reduction, but only structural ones.
We introduce here the transformation calculus, and give our approach to its typing. Fundamental properties, like confluence, have been shown, and two type systems, simple and polymorphic, are proposed.
Garrigue, Jacques "FIML Manual" view details
External link: Online copy
Jacques Garrigue and Hassan Aït-Kaci. The typed polymorphic label-selective lambda-calculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 35-47, 1994 view details
Abstract: Formal calculi on record structures have recently been a focus of active research. However, scarcely anyone has studied formally the dual notion - i.e. argument-passing to functions by keywords, and its harmonization with currying. We have. Recently, we introduced the label-selective lambda-calculus, a conservative extension of lambda-calculus that uses a labeling of abstractions and applications to perform unordered currying. In other words, it enables some form of commutation between arguments. This improves program legibility, thanks to the presence of labels, and efficiency, thanks to argument commuting. In this paper, we propose a simply typed version of the calculus, then extend it to one with ML-like polymorphic types. For the latter calculus, we establish the existence of principal types and we give an algorithm to compute them. Thanks to the fact that label-selective lambda-calculus is a conservative extension of lambda-calculus by adding numeric labels to stand for argument positions, its polymorphic typing provides us with a keyword argument-passing extension of ML abviating the need of records. In this context, conventional ML syntax can be seen as a restriction of the more general keyword-oriented syntax limited to using only implicit positions instead of keywords.
The Transformation Calculus. Jacques Garrigue. Technical Report TR 94-09, Department of Information Science, the University of Tokyo, April 1994 view details
Abstract: The lambda-calculus, by its ability to express any computable function, is theoretically able to represent any algorithm. However, notwithstanding their equivalence in expressiveness, it is not so easy to find a natural translation for algorithms described in an imperative way. The transformation calculus, a conservative extension of lambda-calculus, corrects this flaw by re-introducing an implicit notion of state in the calculus. This is essentially done by combining two features, selective currying permitting an explicit naming of arguments, like was done in selective \lbd-calculus, and the possibility of composing terms, to express an imperative order in operations. Particularly we show how these features permit to express scope-free variables, which can be used roughly like classical mutable ones, without explicit handling of a state between the operations implying them. This calculus stays very close to lambda-calculus, and keeps most of its properties. We prove here its confluence.
Resources
|