Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Generalized Arrows

Adam Megacz Joseph

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2014-130
May 28, 2014

http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.pdf

Multi-level languages and arrows both facilitate metaprogramming, the act of writing a program which generates a program. The {\tt arr} function required of all arrows turns arbitrary metalanguage expressions into object language expressions; because of this, arrows may be used for metaprogramming only when the object language is a superset of the metalanguage. This thesis introduces {\it generalized arrows}, which are less restrictive than arrows in that they impose no containment relationship between the object language and metalanguage; this allows generalized arrows to be used for {\it heterogeneous} metaprogramming. This thesis also establishes a correspondence between two-level programs and one-level programs which take a generalized arrow instance as a distinguished parameter. A translation across this correspondence is possible, and is called a {\it flattening transformation}. The flattening translation is not specific to any particular object language; this means that it needs to be implemented only once for a given metalanguage compiler. Support for various object languages can then be added by implementing instances of the generalized arrow type class; this does not require knowledge of compiler internals. Because of the flattening transformation the users of these object languages are able to program using convenient multi-level types and syntax; the conversion to one-level terms manipulating generalized arrow instances is handled by the flattening transformation. A modified version of the Glasgow Haskell Compiler (GHC) with multi-level types and expressions has been produced as a proof of concept. The Haskell extraction of the Coq formalization in this thesis have been compiled into this modified GHC as a new flattening pass.

Advisor: John Wawrzynek


BibTeX citation:

@phdthesis{Joseph:EECS-2014-130,
    Author = {Joseph, Adam Megacz},
    Title = {Generalized Arrows},
    School = {EECS Department, University of California, Berkeley},
    Year = {2014},
    Month = {May},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.html},
    Number = {UCB/EECS-2014-130},
    Abstract = {Multi-level languages and arrows both facilitate metaprogramming, the
act of writing a program which generates a program.  The {\tt arr}
function required of all arrows turns arbitrary metalanguage
expressions into object language expressions; because of this, arrows 
may be used for metaprogramming only when the object language is a
superset of the metalanguage.

This thesis introduces {\it generalized arrows}, which are less
restrictive than arrows in that they impose no containment
relationship between the object language and metalanguage; this allows
generalized arrows to be used for {\it heterogeneous} metaprogramming.
This thesis also establishes a correspondence between two-level
programs and one-level programs which take a generalized arrow
instance as a distinguished parameter.  A translation across this
correspondence is possible, and is called a {\it flattening
transformation}.

The flattening translation is not specific to any particular object
language; this means that it needs to be implemented only once for a
given metalanguage compiler.  Support for various object languages can
then be added by implementing instances of the generalized arrow type
class; this does not require knowledge of compiler internals.  Because
of the flattening transformation the users of these object languages
are able to program using convenient multi-level types and syntax; the
conversion to one-level terms manipulating generalized arrow instances
is handled by the flattening transformation.

A modified version of the Glasgow Haskell Compiler (GHC) with
multi-level types and expressions has been produced as a proof of
concept.  The Haskell extraction of the Coq formalization in this
thesis have been compiled into this modified GHC as a new flattening
pass.}
}

EndNote citation:

%0 Thesis
%A Joseph, Adam Megacz
%T Generalized Arrows
%I EECS Department, University of California, Berkeley
%D 2014
%8 May 28
%@ UCB/EECS-2014-130
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.html
%F Joseph:EECS-2014-130