Computer Science – Programming Languages
Scientific paper
2010-03-31
Computer Science
Programming Languages
This paper is obsolete and has been superceded by {\it Multi-Level Programs are Generalized Arrows} available here: http://a
Scientific paper
The lambda calculus, subject to typing restrictions, provides a syntax for the internal language of cartesian closed categories. This paper establishes a parallel result: staging annotations, subject to named level restrictions, provide a syntax for the internal language of Freyd categories, which are known to be in bijective correspondence with Arrows. The connection is made by interpreting multi-stage type systems as indexed functors from polynomial categories to their reindexings. This result applies only to multi-stage languages which are (1) homogeneous, (2) allow cross-stage persistence and (3) place no restrictions on the use of structural rules in typing derivations. Removing these restrictions and repeating the construction yields generalized arrows, of which Arrows are a particular case. A translation from well-typed multi-stage programs to single-stage GArrow terms is provided. The translation is defined by induction on the structure of the proof that the multi-stage program is well-typed, relying on information encoded in the proof's use of structural rules. Metalanguage designers can now factor out the syntactic machinery of metaprogramming by providing a single translation from staging syntax into expressions of generalized arrow type. Object language providers need only implement the functions of the generalized arrow type class in point-free style. Object language users may write metaprograms over these object languages in a point-ful style, using the same binding, scoping, abstraction, and application mechanisms in both the object language and metalanguage. This paper's principal contributions are the GArrow definition of Figures 2 and 3, the translation in Figure 5 and the category-theoretic semantics of Definition 16. An accompanying Coq proof formalizes the type system, translation procedure, and key theorems.
No associations
LandOfFree
Multi-Stage Programs are Generalized Arrows does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Multi-Stage Programs are Generalized Arrows, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Multi-Stage Programs are Generalized Arrows will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-579376