Misplaced Pages

#791208

68-491: POP2 and similar names may refer to: POP-2 , a programming language developed around 1970 Post Office Protocol (POP) version 2, a 1985 email exchange protocol Prince of Persia 2: The Shadow and the Flame , a 1993 video game POP2, a gene related to the enzyme 4-aminobutyrate—pyruvate transaminase Pop 2 (mixtape) , a 2017 mixtape by Charli XCX Pop2! The Second 20 Hits ,

136-491: A doublet function : this is a function that had another function attached as its updater , which is called on the receiving side of an assignment. Thus, if the variable a contains an array, then is equivalent to the builtin function updater returning the updater of the doublet. Of course, updater is a doublet and can be used to change the updater component of a doublet. Variables can hold values of any type, including functions, which are first-class objects. Thus,

204-476: A 2009 album in the Erasure discography Pop 2! The Exploding Musical Mind of Dana Countryman , a 2014 album by Dana Countryman Punk Goes Pop Volume Two , a 2009 album of punk pop music [REDACTED] Topics referred to by the same term This disambiguation page lists articles associated with the same title formed as a letter–number combination. If an internal link led you here, you may wish to change

272-428: A broader result in closed monoidal categories : Currying is the statement that the tensor product and the internal Hom are adjoint functors ; that is, for every object B {\displaystyle B} there is a natural isomorphism : Here, Hom denotes the (external) Hom-functor of all morphisms in the category, while B ⇒ C {\displaystyle B\Rightarrow C} denotes

340-402: A category is not closed , and thus lacks an internal hom functor (possibly because there is more than one choice for such a functor). Another way is if it is not monoidal , and thus lacks a product (that is, lacks a way of writing down pairs of objects). Categories that do have both products and internal homs are exactly the closed monoidal categories. The setting of cartesian closed categories

408-430: A common end-of-if-clause notation yet). There are no special language constructs to create arrays or record structures as they are commonly understood: instead, these are created with the aid of special builtin functions, e.g., newarray (for arrays that can contain any type of item) and newanyarray to create restricted types of items. Thus, array element and record field accessors are simply special cases of

476-414: A function f : ( X × Y ) → Z {\displaystyle f:(X\times Y)\to Z} that takes two arguments, one from X {\displaystyle X} and one from Y , {\displaystyle Y,} and produces objects in Z . {\displaystyle Z.} The curried form of this function treats the first argument as

544-540: A function currying constructs a new function That is, g {\displaystyle g} takes an argument of type X {\displaystyle X} and returns a function of type Y → Z {\displaystyle Y\to Z} . It is defined by for x {\displaystyle x} of type X {\displaystyle X} and y {\displaystyle y} of type Y {\displaystyle Y} . We then also write Uncurrying

612-478: A function with more than two arguments can be defined by induction. Currying is useful in both practical and theoretical settings. In functional programming languages , and many others, it provides a way of automatically managing how arguments are passed to functions and exceptions. In theoretical computer science , it provides a way to study functions with multiple arguments in simpler theoretical models which provide only one argument. The most general setting for

680-582: A function, that takes f {\displaystyle f} as an argument, and returns a function that maps each x {\displaystyle x} to f x . {\displaystyle f_{x}.} The proper notation for expressing this is verbose. The function f {\displaystyle f} belongs to the set of functions ( X × Y ) → Z . {\displaystyle (X\times Y)\to Z.} Meanwhile, f x {\displaystyle f_{x}} belongs to

748-425: A homotopy of two functions from Y {\displaystyle Y} to Z {\displaystyle Z} , or, equivalently, a single (continuous) path in Z Y {\displaystyle Z^{Y}} . In algebraic topology , currying serves as an example of Eckmann–Hilton duality , and, as such, plays an important role in a variety of different settings. For example, loop space

SECTION 10

#1733085545792

816-409: A natural complement to the language of category theory , as discussed below. This is because categories, and specifically, monoidal categories , have an internal language , with simply-typed lambda calculus being the most prominent example of such a language. It is important in this context, because it can be built from a single type constructor, the arrow type. Currying then endows the language with

884-890: A natural product type. The correspondence between objects in categories and types then allows programming languages to be re-interpreted as logics (via Curry–Howard correspondence ), and as other types of mathematical systems, as explored further, below. Under the Curry–Howard correspondence , the existence of currying and uncurrying is equivalent to the logical theorem ( ( A ∧ B ) → C ) ⇔ ( A → ( B → C ) ) {\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))} (also known as exportation ), as tuples ( product type ) corresponds to conjunction in logic, and function type corresponds to implication. The exponential object Q P {\displaystyle Q^{P}} in

952-507: A parameter, so as to create a family of functions f x : Y → Z . {\displaystyle f_{x}:Y\to Z.} The family is arranged so that for each object x {\displaystyle x} in X , {\displaystyle X,} there is exactly one function f x . {\displaystyle f_{x}.} In this example, curry {\displaystyle {\mbox{curry}}} itself becomes

1020-413: A program runs (both of which are features of dynamic compilation ), without the overhead of an interpreted language. POP-2's syntax is ALGOL -like, except that assignments are in reverse order: instead of writing one writes The reason for this is that the language has explicit notion of an operand stack . Thus, the prior assignment can be written as two separate statements : which evaluates

1088-428: A result, the application of f {\displaystyle f} and subsequently, g {\displaystyle g} , to those arguments. The process can be iterated. Currying provides a way for working with functions that take multiple arguments, and using them in frameworks where functions might take only one argument. For example, some analytical techniques can only be applied to functions with

1156-528: A single argument. Practical functions frequently take more arguments than this. Frege showed that it was sufficient to provide solutions for the single argument case, as it was possible to transform a function with multiple arguments into a chain of single-argument functions instead. This transformation is the process now known as currying. All "ordinary" functions that might typically be encountered in mathematical analysis or in computer programming can be curried. However, there are categories in which currying

1224-495: A variety of data structures . In parallel with that, Steve Hardy at University of Sussex implemented a subset of POP-2, which he named POP-11 which ran on a Digital Equipment Corporation (DEC) PDP-11/40 computer. It was originally designed to run on the DEC operating system RSX-11D, in time-shared mode for teaching, but that caused so many problems that an early version of Unix was installed and used instead. That version of Pop-11

1292-653: Is a programming language developed around 1970 from the earlier language POP-1 (developed by Robin Popplestone in 1968, originally named COWSEL ) by Robin Popplestone and Rod Burstall at the University of Edinburgh . It drew roots from many sources: the languages Lisp and ALGOL 60 , and theoretical ideas from Peter J. Landin . It used an incremental compiler , which gave it some of the flexibility of an interpreted language , including allowing new function definitions at run time and modification of function definitions while

1360-553: Is a type constructor , specifically, the function type or arrow type. Similarly, the Cartesian product X × Y {\displaystyle X\times Y} of types is constructed by the product type constructor × {\displaystyle \times } . The type-theoretical approach is expressed in programming languages such as ML and the languages derived from and inspired by it: Caml , Haskell , and F# . The type-theoretical approach provides

1428-524: Is a universal property of an exponential object , and gives rise to an adjunction in cartesian closed categories . That is, there is a natural isomorphism between the morphisms from a binary product f : ( X × Y ) → Z {\displaystyle f\colon (X\times Y)\to Z} and the morphisms to an exponential object g : X → Z Y {\displaystyle g\colon X\to Z^{Y}} . This generalizes to

SECTION 20

#1733085545792

1496-434: Is a function that takes objects from the first set, and returns objects in the second set, and so one writes curry : [ ( X × Y ) → Z ] → ( X → [ Y → Z ] ) . {\displaystyle {\mbox{curry}}:[(X\times Y)\to Z]\to (X\to [Y\to Z]).} This is a somewhat informal example; more precise definitions of what

1564-421: Is adjoint to reduced suspensions ; this is commonly written as where [ A , B ] {\displaystyle [A,B]} is the set of homotopy classes of maps A → B {\displaystyle A\rightarrow B} , and Σ A {\displaystyle \Sigma A} is the suspension of A , and Ω A {\displaystyle \Omega A}

1632-403: Is already on the stack (in this case 3), after which the original function poly2 is invoked. It then uses the top four items on the stack, producing the same result as i.e. In POP-2, it was possible to define new operations (operators in modern terms). The first line declares a new operation +* with precedence (priority) 3. The second line creates a function f(x,y)=x*x+y*y, and assigns it to

1700-474: Is commonly interested in continuous functions between topological spaces . One writes Hom ( X , Y ) {\displaystyle {\text{Hom}}(X,Y)} (the Hom functor ) for the set of all functions from X {\displaystyle X} to Y {\displaystyle Y} , and uses the notation Y X {\displaystyle Y^{X}} to denote

1768-554: Is continuous if and only if its curried form is continuous. Another important result is that the application map , usually called "evaluation" in this context, is continuous (note that eval is a strictly different concept in computer science.) That is, eval : Y X × X → Y ( f , x ) ↦ f ( x ) {\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}

1836-572: Is continuous when Y X {\displaystyle Y^{X}} is compact-open and Y {\displaystyle Y} locally compact Hausdorff. These two results are central for establishing the continuity of homotopy , i.e. when X {\displaystyle X} is the unit interval I {\displaystyle I} , so that Z I × Y ≅ ( Z Y ) I {\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}} can be thought of as either

1904-399: Is equivalent to That is, the parenthesis are not required to disambiguate the order of the application. Curried functions may be used in any programming language that supports closures ; however, uncurried functions are generally preferred for efficiency reasons, since the overhead of partial application and closure creation can then be avoided for most function calls. In type theory ,

1972-451: Is meant by "object" and "function" are given below. These definitions vary from context to context, and take different forms, depending on the theory that one is working in. Currying is related to, but not the same as, partial application . The example above can be used to illustrate partial application; it is quite similar. Partial application is the function apply {\displaystyle {\mbox{apply}}} that takes

2040-591: Is mentioned later in the context of higher-order functions. John C. Reynolds defined "currying" in a 1972 paper, but did not claim to have coined the term. Currying is most easily understood by starting with an informal definition, which can then be molded to fit many different domains. First, there is some notation to be established. The notation X → Y {\displaystyle X\to Y} denotes all functions from X {\displaystyle X} to Y {\displaystyle Y} . If f {\displaystyle f}

2108-437: Is not possible; the most general categories which allow currying are the closed monoidal categories . Some programming languages almost always use curried functions to achieve multiple arguments; notable examples are ML and Haskell , where in both cases all functions have exactly one argument. This property is inherited from lambda calculus , where multi-argument functions are usually represented in curried form. Currying

POP2 - Misplaced Pages Continue

2176-490: Is related to, but not the same as partial application . In practice, the programming technique of closures can be used to perform partial application and a kind of currying, by hiding arguments in an environment that travels with the curried function. The "Curry" in "Currying" is a reference to logician Haskell Curry , who used the concept extensively, but Moses Schönfinkel had the idea six years before Curry. The alternative name "Schönfinkelisation" has been proposed. In

2244-743: Is such a function, we write f : X → Y {\displaystyle f\colon X\to Y} . Let X × Y {\displaystyle X\times Y} denote the ordered pairs of the elements of X {\displaystyle X} and Y {\displaystyle Y} respectively, that is, the Cartesian product of X {\displaystyle X} and Y {\displaystyle Y} . Here, X {\displaystyle X} and Y {\displaystyle Y} may be sets, or they may be types, or they may be other kinds of objects, as explored below. Given

2312-437: Is sufficient for the discussion of classical logic ; the more general setting of closed monoidal categories is suitable for quantum computation . The difference between these two is that the product for cartesian categories (such as the category of sets , complete partial orders or Heyting algebras ) is just the Cartesian product ; it is interpreted as an ordered pair of items (or a list). Simply typed lambda calculus

2380-464: Is the adjoint functor that maps suspensions to loop spaces, and uncurrying is the dual. The duality between the mapping cone and the mapping fiber ( cofibration and fibration ) can be understood as a form of currying, which in turn leads to the duality of the long exact and coexact Puppe sequences . In homological algebra , the relationship between currying and uncurrying is known as tensor-hom adjunction . Here, an interesting twist arises:

2448-497: Is the dual transformation to currying, and can be seen as a form of defunctionalization . It takes a function f {\displaystyle f} whose return value is another function g {\displaystyle g} , and yields a new function f ′ {\displaystyle f'} that takes as parameters the arguments for both f {\displaystyle f} and g {\displaystyle g} , and returns, as

2516-664: Is the loop space of A . In essence, the suspension Σ X {\displaystyle \Sigma X} can be seen as the cartesian product of X {\displaystyle X} with the unit interval, modulo an equivalence relation to turn the interval into a loop. The curried form then maps the space X {\displaystyle X} to the space of functions from loops into Z {\displaystyle Z} , that is, from X {\displaystyle X} into Ω Z {\displaystyle \Omega Z} . Then curry {\displaystyle {\text{curry}}}

2584-442: Is the natural bijection between the set A B × C {\displaystyle A^{B\times C}} of functions from B × C {\displaystyle B\times C} to A {\displaystyle A} , and the set ( A C ) B {\displaystyle (A^{C})^{B}} of functions from B {\displaystyle B} to

2652-445: Is the reverse transformation, and is most easily understood in terms of its right adjoint, the function apply . {\displaystyle \operatorname {apply} .} In set theory , the notation Y X {\displaystyle Y^{X}} is used to denote the set of functions from the set X {\displaystyle X} to the set Y {\displaystyle Y} . Currying

2720-582: The Hom functor and the tensor product functor might not lift to an exact sequence ; this leads to the definition of the Ext functor and the Tor functor . In order theory , that is, the theory of lattices of partially ordered sets , curry {\displaystyle {\text{curry}}} is a continuous function when the lattice is given the Scott topology . Scott-continuous functions were first investigated in

2788-440: The lambda calculus , in which functions only take a single argument. Consider a function f ( x , y ) {\displaystyle f(x,y)} taking two arguments, and having the type ( X × Y ) → Z {\displaystyle (X\times Y)\to Z} , which should be understood to mean that x must have the type X {\displaystyle X} , y must have

POP2 - Misplaced Pages Continue

2856-581: The AI2 (Artificial Intelligence, 2nd year level) class using the EMAS operating system. This implementation was written from scratch in the Edinburgh programming language, IMP . Later versions were implemented for Computer Technology Limited (CTL) Modular One, PDP-10 , ICL 1900 series (running the operating system George ). Julian Davies, in Edinburgh, implemented an extended version of POP-2, which he named POP-10 on

2924-619: The PDP-10 computer running TOPS-10 . This was the first dialect of POP-2 that treated case as significant in identifier names, used lower case for most system identifiers, and supported long identifiers with more than 8 characters. Shortly after that, a new implementation known as WPOP (for WonderPop) was implemented by Robert Rae and Allan Ramsay in Edinburgh, on a research-council funded project. That version introduced caged address spaces, some compile-time syntactic typing (e.g., for integers and reals), and some pattern matching constructs for use with

2992-509: The Scott topology is typically finer , and is not sober . The notion of continuity makes its appearance in homotopy type theory , where, roughly speaking, two computer programs can be considered to be homotopic, i.e. compute the same results, if they can be "continuously" refactored from one to the other. In theoretical computer science , currying provides a way to study functions with multiple arguments in very simple theoretical models, such as

3060-403: The attempt to provide a semantics for lambda calculus (as ordinary set theory is inadequate to do this). More generally, Scott-continuous functions are now studied in domain theory , which encompasses the study of denotational semantics of computer algorithms. Note that the Scott topology is quite different than many common topologies one might encounter in the category of topological spaces ;

3128-548: The category of Heyting algebras is normally written as material implication P → Q {\displaystyle P\to Q} . Distributive Heyting algebras are Boolean algebras , and the exponential object has the explicit form ¬ P ∨ Q {\displaystyle \neg P\lor Q} , thus making it clear that the exponential object really is material implication . The above notions of currying and uncurrying find their most general, abstract statement in category theory . Currying

3196-420: The compiler and all its subroutines at run time made it possible to support far richer language extensions than are possible with Macros, and as a result Pop-11 was used (by Steve Hardy, Chris Mellish and John Gibson) to produce an implementation of Prolog , using the standard syntax of Prolog, and the combined system became known as Poplog , to which Common Lisp and Standard ML were added later. This version

3264-406: The following constructs and are equivalent. An interesting operation on functions is partial application , (sometimes termed currying ). In partial application, some number of the rightmost arguments of the function (which are the last ones placed on the stack before the function is involved) are frozen to given values, to produce a new function of fewer arguments, which is a closure of

3332-470: The functor B ↦ B × C {\displaystyle B\mapsto B\times C} is left adjoint to the functor A ↦ A C {\displaystyle A\mapsto A^{C}} . In the category of sets , the object Y X {\displaystyle Y^{X}} is called the exponential object . In the theory of function spaces , such as in functional analysis or homotopy theory , one

3400-418: The general idea of a type system in computer science is formalized into a specific algebra of types. For example, when writing f : X → Y {\displaystyle f\colon X\to Y} , the intent is that X {\displaystyle X} and Y {\displaystyle Y} are types , while the arrow → {\displaystyle \to }

3468-400: The internal hom functor in the closed monoidal category. For the category of sets , the two are the same. When the product is the cartesian product, then the internal hom B ⇒ C {\displaystyle B\Rightarrow C} becomes the exponential object C B {\displaystyle C^{B}} . Currying can break down in one of two ways. One is if

SECTION 50

#1733085545792

3536-405: The link to point directly to the intended article. Retrieved from " https://en.wikipedia.org/w/index.php?title=POP2&oldid=867522541 " Category : Letter–number combination disambiguation pages Hidden categories: Short description is different from Wikidata All article disambiguation pages All disambiguation pages POP-2 POP-2 (also called POP2 )

3604-477: The mathematical context, the principle can be traced back to work in 1893 by Frege . The originator of the word "currying" is not clear. David Turner says the word was coined by Christopher Strachey in his 1967 lecture notes Fundamental Concepts in Programming Languages , but that source introduces the concept as "a device originated by Schönfinkel", and the term "currying" is not used, while Curry

3672-574: The newly declared operation +*. The original version of POP-2 was implemented on an Elliott 4130 computer in the University of Edinburgh (with only 64 KB RAM, doubled to 128 KB in 1972). POP-2 was ported to the ICT 1900 series on a 1909 at Lancaster University by John Scott in 1968. In the mid-1970s, POP-2 was ported to BESM-6 (POPLAN System). In 1978 Hamish Dewar implemented a version of POP-2 specifically for use by Edinburgh University undergraduates in

3740-416: The original function. For instance, consider a function for computing general second-degree polynomials: This can be bound, for instance as such that the expression applies the closure of poly2 with three arguments frozen, to the argument 3, returning the square of (3 - 1), which is 4. The application of the partially applied function causes the frozen values (in this case 1, -2, 1) to be added to whatever

3808-625: The pair f {\displaystyle f} and x {\displaystyle x} together as arguments, and returns f x . {\displaystyle f_{x}.} Using the same notation as above, partial application has the signature apply : ( [ ( X × Y ) → Z ] × X ) → [ Y → Z ] . {\displaystyle {\mbox{apply}}:([(X\times Y)\to Z]\times X)\to [Y\to Z].} Written this way, application can be seen to be adjoint to currying. The currying of

3876-446: The set of functions Y → Z . {\displaystyle Y\to Z.} Thus, something that maps x {\displaystyle x} to f x {\displaystyle f_{x}} will be of the type X → [ Y → Z ] . {\displaystyle X\to [Y\to Z].} With this notation, curry {\displaystyle {\mbox{curry}}}

3944-411: The set of functions from C {\displaystyle C} to A {\displaystyle A} . In symbols: Indeed, it is this natural bijection that justifies the exponential notation for the set of functions. As is the case in all instances of currying, the formula above describes an adjoint pair of functors : for every fixed set C {\displaystyle C} ,

4012-408: The space Y {\displaystyle Y} is locally compact Hausdorff , then is a homeomorphism . This is also the case when X {\displaystyle X} , Y {\displaystyle Y} and Y X {\displaystyle Y^{X}} are compactly generated , although there are more cases. One useful corollary is that a function

4080-454: The strict notion of currying and uncurrying is in the closed monoidal categories , which underpins a vast generalization of the Curry–Howard correspondence of proofs and programs to a correspondence with many other structures, including quantum mechanics, cobordisms and string theory. The concept of currying was introduced by Gottlob Frege , developed by Moses Schönfinkel , and further developed by Haskell Curry . Uncurrying

4148-409: The subset of continuous functions. Here, curry {\displaystyle {\text{curry}}} is the bijection while uncurrying is the inverse map. If the set Y X {\displaystyle Y^{X}} of continuous functions from X {\displaystyle X} to Y {\displaystyle Y} is given the compact-open topology , and if

SECTION 60

#1733085545792

4216-468: The type Y {\displaystyle Y} , and the function itself returns the type Z {\displaystyle Z} . The curried form of f is defined as where λ {\displaystyle \lambda } is the abstractor of lambda calculus. Since curry takes, as input, functions with the type ( X × Y ) → Z {\displaystyle (X\times Y)\to Z} , one concludes that

4284-482: The type of curry itself is The → operator is often considered right-associative , so the curried function type X → ( Y → Z ) {\displaystyle X\to (Y\to Z)} is often written as X → Y → Z {\displaystyle X\to Y\to Z} . Conversely, function application is considered to be left-associative , so that f ( x , y ) {\displaystyle f(x,y)}

4352-476: The use of close for all loops in POP-2. Pop-11 also introduced a pattern matcher for list structures, making it far easier to teach artificial intelligence (AI) programming. Around 1980, Pop-11 was ported to a VAX-11/780 computer by Steve Hardy and John Gibson, and soon after that it was replaced by a full incremental compiler (producing machine-code instead of an interpreted intermediate code). The existence of

4420-447: The value 3 and leaves it on the stack, and which pops the top value off the stack and assigns it to the variable 'a'. Similarly, the function call can be written as (commas and semicolons being largely interchangeable) or even or Because of the stack-based paradigm, there is no need to distinguish between statements and expressions ; thus, the two constructs and are equivalent (use of close , as endif hadn't become

4488-472: Was implemented in an early dialect of C, using an idiosyncratic compiler made it very hard to maintain and upgrade to new versions of the Mac operating system. Also, AlphaPop was not " 32-bit clean" due to the use of high address bits as tag bits to signify the type of objects, which was incompatible with the use of memory above 8 Mb on later Macintoshes. Currying In the prototypical example, one begins with

4556-532: Was later ported to a variety of machines and operating systems and as a result Pop-11 became the dominant dialect of POP-2, still available in the Poplog system. Around 1986, a new AI company Cognitive Applications Ltd., collaborated with members of Sussex university to produce a variant of Pop-11 named AlphaPop running on Apple Mac computers, with integrated graphics. This was used for many commercial projects, and to teach AI programming in several universities. That it

4624-548: Was written in Unix assembly language , and code was incrementally compiled to an intermediate bytecode which was interpreted. That port was completed around 1976, and as a result, Pop-11 was used in several places for teaching. To support its teaching function, many of the syntactic features of POP-2 were modified, e.g., replacing function ... end with define ... enddefine and adding a wider variety of looping constructs with closing brackets to match their opening brackets instead of

#791208