Fresh Objective Caml user manual
Contents
1. 13 3 5 Abstracti PACS e e AE oco ee A BG EO e 14 3 6 Swapping bindable names sia a Ra a RRA 16 3 7 The freshness relation 5 4 6 x wad oe A ew oS 18 3 8 Abstraction types in general ecos coe aa ROH E AMG oD 18 3 9 Ref erenc cells A a ee Ret ek OA EH ee REL E oe ee ae 20 Bibliography 21 1 1 1 2 Introduction About the language Fresh O Caml extends Objective Caml www ocaml org to provide seamless and cor rect manipulation of object language binding constructs inside a metalanguage The language enables the programmer to concentrate on the algorithmic essence of their syntax manipulating programs without having to concern themselves with the te dious matters of ensuring that properties of a convertible object language names are correctly respected Importantly an algebraic datatype in Fresh O Caml may involve the use of a novel abstraction type former which enables one to incorporate repre sentations of object level binding operations into meta level syntax trees without any further ado Such representations are first class citizens in the metalanguage just like products sums and the like the resulting syntax trees correctly represent object level syntax up to a conversion of the bound names as proved in 4 The result is a style of metaprogramming which feels natural and elegant yielding concise name and binder manipulating code which exhibits real correspondence to the underlying algo rithms Our2. val listBvars term gt var list lt fun gt Perhaps the intention was for listBvars e to return a list of names of binding variables in the object level term represented by e However such a list of binding variables makes no sense at the level of a equivalence classes of object level terms i e values of type term and indeed all listBvars does is to return a list of fresh atoms rather than the actual atoms occurring in some value to which it is applied listBvars el var list name_0 name_1 We can count the length of such a list but we do not have access to the names of the atoms in it Compare this with the following declaration of a function listFvars which makes use of the List filter function 2 Sect 20 17 let rec listFvars e match e with Var x gt x Fn lt lt x gt gt e1 gt List filter lt gt x listFvars el App e1 e2 gt listFvars el listFvars e2 Letfun lt lt f gt gt lt lt x gt gt e1 e2 gt List filter lt gt f List filter lt gt x listFvars e1 listFvars e2 val listFvars term gt var list lt fun gt 3 6 16 CHAPTER 3 HANDLING OF BINDING OPERATIONS When applied to a value of type term the function listFvars returns a list of atoms possibly with repeats corresponding to the free variables of the object language term represented by the value Although we cannot see the names of those atoms directly we can comp
3. programming with binders using it The Fresh O Caml code samples referred to in this manual are linked to from that page 5 1 3 1 4 6 CHAPTER 1 INTRODUCTION The current release of Fresh O Caml is based on release 3 08 2 of the Objective Caml system It is known to compile successfully on Linux and Mac OS X systems and should work without difficulty on other UNIX like platforms It has not been tested on Microsoft Windows Fresh O Caml is currently only distributed as source code You can download the latest distribution which at the time of writing is version 3 08 2 4 of 14 January 2005 or browse the example files Commands similar to the following should suffice to build and install the system tar fxz fresh ocaml 3 08 2 4 tar gz cd fresh ocaml 3 08 2 4 configure make world make opt make install If you wish to install the system somewhere other than the default installation location of usr local then use the prefix option to the configure script for example configure prefix fresh ocaml Note that we strongly advise not installing Fresh O Caml with the same prefix as your existing O Caml installation The web site www fresh ocaml org will be updated with revised Fresh O Caml distri butions and or installation instructions as they appear The toplevel system The interpreter is started by executing fresh ocaml This produces a modified ver sion of the O Caml interactive topleve
4. same length The freshness relation The boolean valued expression expr freshfor expr is true iff expr is an expression of bindable name type that evaluates to an atom occurring in the algebraic support which we here abbreviate to just support of the value to which expr evaluates The notion of support comes from the intended denotational semantics of Fresh O Caml in the universe of FM cppos see 4 It gives a syntax independent notion of the set of free atoms of a value We refer the reader to 1 for a full account of this notion and simply note that the support of a Fresh O Caml representation of some object language term corresponds to the set of free variables in that term The freshfor relation thus provides a built in not a free variable of test for object language terms For example the freshfor relation holds between an atom and a value of the type term declared in Sect 3 2 just in case the atom does not occur in the list returned by applying the listFvars function of Sect 3 5 to the value x freshfor e0 bool false List mem x listFvars e0 bool true y freshfor e0 bool true List mem y listFvars e0 bool false Abstraction types in general So far we have given examples of abstraction types lt lt tyexpr gt gt tyexpr and val ues vi v2 where tyexpr is a type of bindable names and hence v is an atom Fresh O Caml
5. the EU FP5 IST thematic network IST 2001 38957 APPSEM II Tallinn Estonia April 2004 M R Shinwell A M Pitts and M J Gabbay FreshML Programming with binders made simple In Eighth ACM SIGPLAN International Conference on Func tional Programming ICFP 2003 Uppsala Sweden pages 263 274 ACM Press August 2003 21
6. value a 0 a b 3 2 of type lt lt lt lt a name gt gt a name list gt gt a name a name behaves in all respects like a b 8 J a d 3 3 but is a different value from Llao olb a 4 3 4 since a is in the support of the value in 3 3 The general form of abstraction is useful for specifying object level binding operations whose binding names rather than bound names occur in a concrete data structure of some fixed type For example let us add pair expressions and patterns to the fragment of ML we have been using as a running example by redeclaring term as follows type pat patterns p VarPat of var x PairPat of pat pat p1 p2 type term terms e Var of var x Pair of term term el e2 Fn of lt lt pat gt gt term fn p gt e App of term term el e2 Letfun of let fun f p el in e2 lt lt var gt gt lt lt pat gt gt term term For example the ML first projection function fn x y x can be represented by the value Fun PairPat a b Var a of the above type term assuming a and b are atoms of type var This change to term hardly affects the definition of capture avoiding substitution in Fresh O Caml which becomes let rec subst e x e match e with Var y gt if x y then e else Var y Pair e1 e2 gt Pair subst e x el subst e x e2 Fn lt lt p gt gt e1
7. Technical Report as Number 621 nee UNIVERSITY OF CAMBRIDGE Computer Laboratory Fresh Objective Caml user manual Mark R Shinwell Andrew M Pitts February 2005 15 JJ Thomson Avenue Cambridge CB3 OFD United Kingdom phone 44 1223 763500 http hwww cl cam ac uk 2005 Mark R Shinwell Andrew M Pitts Technical reports published by the University of Cambridge Computer Laboratory are freely available via the Internet http hwww cl cam ac uk Tech Reports ISSN 1476 2986 Contents 1 Introduction 5 1 1 About the lanistagel zii iaa Aaa a RSG 5 1 2 Obtaining and installing Fresh OCaml 5 1 3 The toplevel system ts ee a e ia ERS 6 1 4 Batch compilation ra RAR E e 6 2 Concrete syntax 9 21 KeyWords s so a ee bbe eee hee ORS ee ESS 9 2 2 Values y a FW Ow Dh ee a a a eH A 9 2 3 Type EXpTESSIONS veia gece ed ek OR ek ee Ge ed ea 10 24 Pattern ei a Sch O ae ee eae ES 10 2 5 EXpressiOns aaa daa o whe oe a OE ek A S we ook ae 10 3 Handling of binding operations 11 3 1 Types of bindable name i hs ao ad Ae Sw aa we 11 3 2 Abstraction values and types o o o ooo e e 11 3 3 Declari g fresh atomis ae A e A ad ae 12 3 4 Structural equality and alpha conversion
8. abstractions see sec tion 3 2 and for testing whether a bindable name is fresh for an expression see section 3 7 expr fresh fresh bindable name swap expr and expr in expr swapping lt lt expr gt gt expr abstraction lt expr gt expr with alternative syntax expr freshfor expr freshness relation rest of grammar as in 2 Sect 6 7 The typing of these expressions can be deduced from the following interaction with the Fresh O Caml toplevel As can be seen from the first response the interactive system prints atoms as name_n for n 0 1 2 fresh _a name name_0 function x gt function y gt function z gt swap x and y in Z a name gt a name gt b gt b lt fun gt function x gt function y gt lt lt x gt gt y a gt b gt lt lt a gt gt b lt fun gt function x gt function y gt lt x gt y a gt b gt lt lt a gt gt b lt fun gt function x gt function y gt x freshfor y a name gt b gt bool lt fun gt 3 1 3 2 Handling of binding operations This chapter gives an informal explanation of Fresh O Caml s facilities for computing with binders Types of bindable names Fresh O Caml provides a polymorphic family a name of types of bindable names For each type tyexpr the values of type tyexpr name are called atoms and behave
9. approach differs from approaches which use higher order abstract syntax internally not least because Fresh O Caml gives direct access to the names of bound entities Fresh O Caml is the latest in a series of languages based on the Gabbay Pitts theory of FM sets and metaprogramming 1 This theory first yielded a language with quite a complicated static type system for controlling the dynamic effects of fresh name gen eration 3 More recently such a type system has been found to be unnecessary for the basic correctness properties of representing object level syntax up to a conversion of bound names as a result of this discovery the FreshML language described in 6 was created Whilst an interpretive system was created for this language it is no longer supported Instead Fresh O Caml is now used which transfers these ideas to the Objective Caml language This User Manual provides an informal introduction to the features of Fresh O Caml that are new compared with O Caml It assumes familiarity with the ML programming idiom and terminology in general and with O Caml 2 in particular A very much more detailed discussion of the Fresh O Caml language and its correctness properties are provided in a journal paper and Shinwell s PhD thesis 4 Obtaining and installing Fresh O Caml To obtain Fresh O Caml visit the website at www fresh ocaml org which also con tains examples of
10. ction indicates this is indeed what we get 3 5 ABSTRACTION PATTERNS 15 The declaration of subst manages to implement this capture avoiding behaviour be cause of the way Fresh O Caml matches atom abstraction patterns using fresh atoms for abstracted identifiers For example when evaluating subst Var y x e0 we fall through to the second match clause Fn lt lt y gt gt e1 gt Fn lt lt y gt gt subst e x el and reach a point where the environment contains the associations x gt a e gt Var b where b is the atom the environment associates with y and we are attempting to match Fn lt lt y gt gt e1 against the value associated with e0 namely Fn b Var a The match succeeds in associating y with a fresh atom b say and e1 with the result of swapping b with Dd in Vara which is Vara again Then the right hand side of the clause Fn lt lt y gt gt subst x e e1 is evaluated in this environment and with the current state augmented by 0 resulting in the value Fn b Var b as expected So matching that involves abstraction patterns may have the side effect of dynamically generating fresh names For example consider the following declaration let rec listBvars e match e with Var _ gt Fn lt lt x gt gt e1 gt x listBvars el App e1 e2 gt listBvars el listBvars e2 Letfun lt lt f gt gt lt lt x gt gt e1 e2 gt f x listBvars el listBvars e2
11. el e2 amp amp eq swap f1 and f2 in el e2 _ _ gt false val eq term gt term gt bool lt fun gt We mentioned in Sect 3 4 that the built in structural equality function imple ments the appropriate notion of a equivalence for values of type term and in fact the function eq coincides with the built in structural equality function for this type For example with e1 e2 and e3 as declared in Sect 3 4 eq el e2 bool false eq e1 e3 bool true let f fresh var val f var name_0 let e6 Letfun lt lt f gt gt lt lt x gt gt Var x App Var f Var y val e6 expr Letfun lt lt name_1 gt gt lt lt name_0 gt gt Var name_0 App Var name_1 Var name_2 let e7 Letfun lt lt x gt gt lt lt y gt gt Var y App Var x Var y val e7 expr Letfun lt lt name_1 gt gt lt lt name_0 gt gt Var name_0 App Var name_1 Var name_2 eq e6 e7 bool true e6 e7 bool true Fresh O Caml also provides a standard library module Freshness which contains a function to swap multiple atoms at once Calling 3 7 3 8 18 CHAPTER 3 HANDLING OF BINDING OPERATIONS Freshness swap_multiple_atoms 11 12 v where 11 and 12 are lists of bindable names returns that value formed by swapping the first element of 11 with the first element of 12 throughout v and so forth to the end of the lists Both lists must therefore be the
12. el a equivalence For example consider the following declarations let el Fn lt lt x gt gt Fn lt lt x gt gt App Var x Var x let e2 Fn lt lt x gt gt Fn lt lt y gt gt App Var x Var x let e3 Fn lt lt x gt gt Fn lt lt y gt gt App Var y Var y These associate with the identifiers e1 e2 and e3 values of type term corresponding to the a equivalence classes of the terms fnr gt fnr gt rr fnr gt fny gt srr Mmai gt fny gt yy respectively The first and the second of these terms are not a equivalent whereas the first and the third are Fresh O Caml knows this This is discussed at length in 4 3 5 14 CHAPTER 3 HANDLING OF BINDING OPERATIONS el e2 bool false el e3 bool true Abstraction patterns Deconstruction of an abstraction value v va is performed using an abstraction pattern lt lt pattern gt gt pattern This matches against the structure of the values in the binding position and in the body of the abstraction rather like a pair pattern Crucially how ever during matching Fresh O Caml ensures that any atoms which occur inside these values and which are bound by an abstraction are suitably freshened before the values are associated with identifiers in the environment This is achieved by consistently swapping these existing atoms inside the values with as many fresh ones as necessary This form of matching ensures that these co
13. elds or methods They are the values inhabiting the types of bindable names a name see section 3 1 Abstraction values Abstraction values are given by pairs written v v2 where v and v2 are values They are the values inhabiting abstraction types which are written lt lt tyexpr gt gt tyexpro see section 3 2 1The name atom is used for historical reasons to do with the mathematical universe 1 that under lies the semantics of Fresh O Caml 2 3 2 4 2 5 10 CHAPTER 2 CONCRETE SYNTAX Type expressions Fresh O Caml adds to O Caml a distinguished type constructor for types of bindable names and a binary operation for forming abstraction types typexpr tyexpr name type of names lt lt tyexpr gt gt tyexpr abstraction type rest of grammar as in 2 Sect 6 4 Patterns Fresh O Caml adds to O Caml patterns for abstraction values see section 3 5 There are two alternative forms of syntax Since the first one lt lt gt gt interferes with the Camlp4 preprocessor quotation mechanism it is recommended to use the second one lt 1 gt if Camlp4 is in use pattern lt lt pattern gt gt pattern abstraction lt pattern gt pattern with alternative syntax the rest as in 2 Sect 6 6 Expressions Fresh O Caml adds to O Caml expressions for creating fresh bindable names see sec tion 3 3 for swapping bindable names see section 3 6 for
14. gt Fn lt lt p gt gt subst e x el App e1 e2 gt App subst e x el subst e x e2 Letfun lt lt f gt gt lt lt p gt gt e1 e2 gt Letfun lt lt f gt gt lt lt p gt gt subst e x el subst e x e2 val subst term gt var gt term gt term lt fun gt 30f course linearity conditions on object level patterns are not enforced by the declaration of term so for example Fun PairPat a a Var a is also a value of type term 3 9 20 CHAPTER 3 HANDLING OF BINDING OPERATIONS Reference cells The interactions between reference cells and the model of name binding employed by Fresh O Caml may be surprising to the reader For the address of a reference cell is treated as being pure that is to say it is treated as containing no atoms It follows that any swapping operations on the address of the cell will not have any effect in particular the contents of the cell are unchanged We can illustrate the semantics with the following code fragment which always pro duces the result false let a fresh let x lt lt a gt gt ref a match x with lt lt a gt gt a gt a la Compare this to the following fragment which always produces true let a fresh let x lt lt a gt gt a match x with lt lt a gt gt a gt a a This semantics for swapping operations on reference cells is theoretically straightfor ward but perhaps pragmatically unsatisfactor
15. l system waiting for you to type Fresh O Caml programs fresh ocaml Fresh Objective Caml version 3 08 2 4 Write your programs using the concrete syntax of O Caml 2 Chapter 6 augmented by the syntax described in Chapter 2 The features that Fresh O Caml adds to O Caml are described in Chapter 3 Batch compilation For batch compilation the following compilers are provided These correspond to those from the standard Objective Caml distribution The features that Fresh O Caml adds to O Caml are described in Chapter 3 e fresh ocamlc compilation to bytecode 1 4 BATCH COMPILATION 7 e fresh ocamlc opt compilation to bytecode but with the compiler itself com piled to native code e fresh ocamlopt compilation to native code e fresh ocamlopt opt compilation to native code but with the compiler itself also compiled to native code 2 1 2 2 Concrete syntax This chapter describes the additions Fresh O Caml makes to the concrete syntax of O Caml The meaning of the new syntactic forms is described in Chapter 3 Keywords The following identifiers are reserved as keywords in Fresh O Caml and cannot be employed otherwise name fresh freshfor swap The following character sequences are also keywords lt lt gt gt lt gt Values Atoms There is a countably infinite collection of atoms Atoms form a name space distinct from other O Caml name spaces such as names of record fi
16. ncrete values are always suitably fresh many side conditions to do with the freshness of names which crop up in operational semantics and the like are then automatically satisfied For example consider the following function subst term gt var gt term gt term It implements capture avoiding substitution subst e x e computes a representation of the object language term obtained by capture avoiding substitution of the term represented by e for all free occurrences of the variable named x in the term repre sented by e let rec subst e x e match e with Var y gt if x y then e else Var y Fn lt lt y gt gt e1 gt Fn lt lt y gt gt subst e x e1 App e1 e2 gt App subst e x el subst e x e2 Letfun lt lt f gt gt lt lt y gt gt e1 e2 gt Letfun lt lt f gt gt lt lt y gt gt subst e x el subst e x e2 For example with e0 as declared above let e4 subst Var y x e0 val e4 term Fn lt lt name_1 gt gt Var name_0 let e5 Fn lt lt x gt gt Var y val eb term Fn lt lt name_1 gt gt Var name_0 el eb bool true The value binding for e4 carries out the substitution of y for the free occurrence of x in the term represented by e0 which is fn y gt x We expect to obtain as a result a value corresponding not to the term fn y y but rather to the term fn z gt y where z is any variable other than y such as x As the above intera
17. of the generative nature of the declaration type t in Fresh O Caml to which to apply the type construction name Now we can declare a suitable datatype for parse trees of terms in our example object language or rather for a equivalence classes of them type term terms e Var of var x Fn of lt lt var gt gt term fn x gt e App of term term el e2 Letfun of let fun f x el in e2 lt lt var gt gt lt lt var gt gt term term The types we have used in this declaration tell the system exactly which data con structors are binders and in which way their arguments are bound For example in the term let fun f x e1 in eg end there is a binding occurrence of the variable f whose scope is both of e and e2 and a binding occurrence of the variable x whose scope is just e1 These binding scopes are reflected by the type of corresponding constructor Letfun For example if a and b are atoms of type var then a b App Var a Var b Var a is a value of type lt lt var gt gt lt lt var gt gt term term and then Letfun aj b App Var a Var b Var a 3 1 is a value of type term representing the a equivalence class of the term let fun fx fx in f end For example renaming a to some fresh atom a then the value Letfun a b App Var a Var b Var a behaves in all respects like 3 1 Fresh O Caml codifies a common practice in math ematics when it c
18. omes to dealing with binders its programs allow the user to ma nipulate a equivalence classes by naming one of their representatives through the use of value identifiers naming specific bindable names However as shown in 5 Fresh O Caml is designed in such a way that well typed programs can only use such representatives in ways that are independent up a equivalence of which particular representative is chosen Declaring fresh atoms We can create values of type term by applying its constructors to previously con structed values with the constructor Var getting us off the ground However initially there are no constants of type var and to get some bindable names we have to create them using the fresh expression For example to get a parse tree of type term that represents the a equivalence class of the first projection function fn x gt fn y gt 1 we can use the declarations let x y fresh var fresh var let fst Fn lt lt x gt gt Fn lt lt y gt gt Var x 3 4 3 4 STRUCTURAL EQUALITY AND ALPHA CONVERSION 13 The first one associates with the value identifiers x and y atoms not used so far in the current environment a and b say and then the second one associates with the value identifier fst the value Fn a Fn b Var a of type term Note that lt lt x gt gt is not a meta level binding operation Thus in the above decla ration of fst the occurrences of x and y are not locally b
19. ound value identifiers as they would be in function x gt function y gt Var x for example but refer to the previously declared values of type var For example we can re use those values to declare an open term let e0 Fn lt lt y gt gt Var x The system s response to the above declarations is val x var name_0 val y var name_0 val fst term Fn lt lt name_0 gt gt Fn lt lt name_1 gt gt Var name_0 val e0 term Fn lt lt name_1 gt gt Var name_0 This tells us that we have associated with fst and e0 values of type term and it gives us a textual representation of those values In this representation atoms are printed as name_n with distinct atoms getting distinct numbers n Note from the first two lines of the system s response that this numbering works on a per response basis rather like the renaming of type variables by an ML system to start from a for each response the particular atoms assigned to each name are hidden from the user Structural equality and alpha conversion The important correctness property of Fresh O Caml is that values of types like term are observationally equivalent iff they correspond to a equivalent terms of the object language Thus we obtain working up to a conversion for free In particular when the function a gt a gt bool that tests for structural equality 2 Sect 19 2 is applied to values of type term it computes object lev
20. permits values of arbitrary type in binding position that is within the double angle brackets Using some types of value in this position may cause Invalid_argument exceptions to be raised upon evaluation in the same way that for example using structural equality between function values raises this exception 2 Sect 19 2 The reason for this has to do with the semantics of matching alluded to in Sect 3 5 Fresh O Caml freshens bound values by swapping all the atoms in their support see Sect 3 7 with dynamically generated fresh ones For this process to be seman tically sound the system has to calculate the support of a value accurately overes timation by just finding all the atoms occurring in the value can be unsound This is not possible for function values so the Invalid_argument exception is raised upon encountering such values during matching For example 3 8 ABSTRACTION TYPES IN GENERAL 19 let absApply lt lt f gt gt x f x val absApply lt lt a gt b gt gt a gt b lt fun gt absApply lt lt function x int gt x gt gt 0 Exception Invalid_argument Invalid value in binding position The semantics of Fresh O Caml matching ensures that values of the form v v2 are indistinguishable up to freshening all the atoms in the support of the value v which occur in the value v2 For example swapping atoms a and b with different atoms a and 0 respectively the
21. rather like values of the ML type unit ref they provide an inexhaustible supply of names which may take part in binding operations at the object level The user has access to this supply via the expression fresh of type a name which yields a fresh atom each time it is evaluated Each type of bindable names is isomorphic to any other the use of the type parameterised family a name is simply to provide as many different such types as the user needs whilst subsuming polymorphism over the different kinds of name under the usual mechanisms for polymorphic types Abstraction values and types We are going to use as a running example of an object language a small ML like language with the following kinds of terms x variables fnx gt e function abstraction 1 2 function application let fun f x e in eg end local recursive function We will name variables such as x and f in the above terms using a type of bindable names in order to be able to take advantage of Fresh O Caml s ability to handle a conversion and freshness of atoms automatically type t and var t name to which the system responds type t type var t name This is a simpler approach than the bindable_type declaration used by FreshML 6 11 3 3 12 CHAPTER 3 HANDLING OF BINDING OPERATIONS It is the type var that we want to use as a type of bindable names the abstract type t just provides us with some type a fresh one because
22. s to replace the bound names in a number of abstraction with the same name For example consider declaring a function eq of type term gt term gt bool to compute equality of a equivalence classes of terms in the fragment of ML we are using as a running example When comparing the 3 6 SWAPPING BINDABLE NAMES 17 equivalence classes of two function abstractions we can always choose representatives of the classes that have the same fn bound variable and then compare the bodies of the function abstractions for equality modulo a equivalence Thus we might be tempted to use a clause like Fn lt lt x gt gt e1 Fn lt lt x gt gt e2 gt eq el e2 in the declaration of eq This is not possible in Fresh O Caml because for simplicity it adopts the same linearity constraint on patterns as does O Caml there must be at most one occurrence of any value identifier in a pattern In the clause for Fn in the declaration of eq we must use distinct bound names in the function abstractions and then swap them and similarly for the other binder Letfun let rec eq ee match e e with Var x Var y gt x y Fn lt lt x1 gt gt e1 Fn lt lt x2 gt gt e2 gt eq swap x1 and x2 in el e2 App e1 e1 App e2 e2 gt eq el e2 amp amp eq el e2 Letfun lt lt f1 gt gt lt lt x1 gt gt e1 e1 Letfun lt lt f2 gt gt lt lt x2 gt gt e2 e2 gt eq swap f1 and f2 in swap x1 and x2 in
23. ute with them The following interaction illustrates the difference be tween listBvars and listFvars recall that e0 was declared to be Fn lt lt y gt gt Var x listFvars e0 x bool true listBvars e0 y bool false The second equality is false because listBvars e0 computes a fresh atom for e0 s bound variable An even more extreme example is listBvars e0 listBvars e0 bool false The value is false because listBvars e0 computes a fresh atom each time it is evaluated Swapping bindable names Fresh O Caml has name swapping expressions of the form swap expr and expr in exprs Here expr and expr must be expressions of the same type of bindable names The swap expression evaluates expr and expr to find which atoms they stand for and then interchanges all occurrences of those atoms in the value obtained by evaluating expr3 For example swap x and y in App Var x Var y App Var y Var x bool true Name swapping can express the operation from 3 of concreting an abstraction at a fresh atom let function lt lt x gt gt e term gt function x var gt swap x and x in e val 00 lt lt var gt gt term gt var gt term lt fun gt lt lt x gt gt Fn lt lt y gt gt App Var x Var x y term Fn lt lt name_1 gt gt App Var name_0 Var name_0 A more typical use of swap expressions i
24. y However it is not yet clear how the situation could be improved and further research will be required 4As of the time of writing February 2005 there is a bug in the released versions of the Fresh O Caml system which causes incorrect results when using reference cells This will be fixed in the near future Bibliography 1 2 3 4 5 6 M J Gabbay and A M Pitts A new approach to abstract syntax with variable binding Formal Aspects of Computing 13 341 363 2002 Special issue in honour of Rod Burstall To appear X Leroy D Doligez J Garrigue D R my and J Vouillon The Objective Caml Sys tem Institut National de Recherche en Informatique et en Automatique INRIA release 3 06 edition August 2002 A M Pitts and M J Gabbay A metalanguage for programming with bound names modulo renaming In R Backhouse and J N Oliveira editors Mathematics of Program Construction 5th International Conference MPC2000 Ponte de Lima Por tugal July 2000 Proceedings volume 1837 of Lecture Notes in Computer Science pages 230 255 Springer Verlag Heidelberg 2000 M R Shinwell The Fresh Approach functional programming with names and binders PhD thesis University of Cambridge Computer Laboratory 2005 M R Shinwell and A M Pitts On a monadic semantics for freshness Theoretical Computer Science 2005 To appear a preliminary version appears in the proceed ings of the second workshop of
Download Pdf Manuals
Related Search