RE: Post making contest
11-18-2016, 04:52 AM
Programming Language Fan Fiction (extended abstract)
Stefan Muller, Carnegie Mellon University
Programming language theory and design is an area of research in which authors frequently make design
decisions. For example, authors might choose between call-by-name and call-by value; simply typed, dependently
typed and untyped; intensional and extensional; predicative and impredicative; C-style syntax and
ML-style syntax; statically and dynamically typed; garbage-collected and useless, etc. Inevitably, readers
of these papers wonder what would happen if one of these design decisions were made differently. This is
not a feature unique to programming languages; fan fiction is a popular process in which devotees of a work
of fiction reimagine the work in their own way. It thus seems that programming languages and fan fiction
could be combined to form a large body of new ideas, and it is the author’s opinion that SIGBOVIK is a
fine venue for such ideas.
Here, we present a number of avenues for development of programming language fan fiction. Some of
these areas appear novel; in others, some work has already been done which can now be drawn under the
umbrella of programming language fan fiction.
• Alternate notions of type membership. Type theories typically define the canonical forms of a
particular type, but occasionally variations on this canon are possible. For example, in a strict language,
canonical forms of pair type are (v1, v2) where v1 and v2 are themselves irreducible. Proponents
of laziness might instead consider values of pair type to be (e1, e2) where e1 and e2 are arbitrary
expressions. Expressions of a type which are considered by fans of a type theory, but not by the
original presentation, to be irreducible are known as headcanonical forms or, if accepted by a large
fanbase, fanonical forms.
1
• Hacking new features into old languages. A common source of complaints about programming
languages comes from the fact that a particular feature isn’t present in a particular language. This
complaint generally takes the form “I’d consider using language if only it had feature!” Examples
include:
– Statically-typed Python2
– Garbage-collected C [1]
– Concurrent ML [2]
– LaTeX with types
– LaTeX with decent syntax
– LaTeX with any features at all
Some of the above are considered conservative extensions. Often, however, adding a particular feature
to a particular language breaks a desired soundness property, makes type checking undecidable or
causes various other havoc. This is generally not considered a problem in fan fiction, so have at it.
• Meta-properties of fan fiction. One interesting area of future research is the application of programming
language techniques to the study of fan fiction. For example, fan fiction can be “Kripked” (a
reference to author Eric Kripke) if it is validated by new canon. However, this assumes that the development
of canon is linear. Often in computer science research, however, new developments will build
1Note that this terminology is itself subject to debate. Confusingly, some authors of type theory fan fiction believe that the
latter forms should be known as headcanonical forms and the former should be weak headcanonical forms. 2https://github.com/illume/static checking python
off of older ones in a nonlinear, branching fashion. This leads to the question of whether programming
language fan fiction can be “Kripked” (a reference to logician Saul Kripke) in a way consistent with
nonlinear reachability graphs.
• Fan fiction of type theory itself. Fans can make fan fiction not just of particular programming
languages or type theories, but of the subject of type theory itself. In important prior work in this
area, languages have been developed which are clearly based upon fan fiction-style manipulations of
type theory itself3.
References
[1] HansJ. Boehm and Paul F. Dubois. Dynamic memory allocation and garbage collection. Computers in
Physics, 9(3):297–303, 1995.
[2] John H. Reppy. CML: A higher-order concurrent language. In Proceedings of the SIGPLAN 1991
Conference on Programming Language Design and Implementation, pages 293–305, New York, NY, June
1991. ACM.
Stefan Muller, Carnegie Mellon University
Programming language theory and design is an area of research in which authors frequently make design
decisions. For example, authors might choose between call-by-name and call-by value; simply typed, dependently
typed and untyped; intensional and extensional; predicative and impredicative; C-style syntax and
ML-style syntax; statically and dynamically typed; garbage-collected and useless, etc. Inevitably, readers
of these papers wonder what would happen if one of these design decisions were made differently. This is
not a feature unique to programming languages; fan fiction is a popular process in which devotees of a work
of fiction reimagine the work in their own way. It thus seems that programming languages and fan fiction
could be combined to form a large body of new ideas, and it is the author’s opinion that SIGBOVIK is a
fine venue for such ideas.
Here, we present a number of avenues for development of programming language fan fiction. Some of
these areas appear novel; in others, some work has already been done which can now be drawn under the
umbrella of programming language fan fiction.
• Alternate notions of type membership. Type theories typically define the canonical forms of a
particular type, but occasionally variations on this canon are possible. For example, in a strict language,
canonical forms of pair type are (v1, v2) where v1 and v2 are themselves irreducible. Proponents
of laziness might instead consider values of pair type to be (e1, e2) where e1 and e2 are arbitrary
expressions. Expressions of a type which are considered by fans of a type theory, but not by the
original presentation, to be irreducible are known as headcanonical forms or, if accepted by a large
fanbase, fanonical forms.
1
• Hacking new features into old languages. A common source of complaints about programming
languages comes from the fact that a particular feature isn’t present in a particular language. This
complaint generally takes the form “I’d consider using language if only it had feature!” Examples
include:
– Statically-typed Python2
– Garbage-collected C [1]
– Concurrent ML [2]
– LaTeX with types
– LaTeX with decent syntax
– LaTeX with any features at all
Some of the above are considered conservative extensions. Often, however, adding a particular feature
to a particular language breaks a desired soundness property, makes type checking undecidable or
causes various other havoc. This is generally not considered a problem in fan fiction, so have at it.
• Meta-properties of fan fiction. One interesting area of future research is the application of programming
language techniques to the study of fan fiction. For example, fan fiction can be “Kripked” (a
reference to author Eric Kripke) if it is validated by new canon. However, this assumes that the development
of canon is linear. Often in computer science research, however, new developments will build
1Note that this terminology is itself subject to debate. Confusingly, some authors of type theory fan fiction believe that the
latter forms should be known as headcanonical forms and the former should be weak headcanonical forms. 2https://github.com/illume/static checking python
off of older ones in a nonlinear, branching fashion. This leads to the question of whether programming
language fan fiction can be “Kripked” (a reference to logician Saul Kripke) in a way consistent with
nonlinear reachability graphs.
• Fan fiction of type theory itself. Fans can make fan fiction not just of particular programming
languages or type theories, but of the subject of type theory itself. In important prior work in this
area, languages have been developed which are clearly based upon fan fiction-style manipulations of
type theory itself3.
References
[1] HansJ. Boehm and Paul F. Dubois. Dynamic memory allocation and garbage collection. Computers in
Physics, 9(3):297–303, 1995.
[2] John H. Reppy. CML: A higher-order concurrent language. In Proceedings of the SIGPLAN 1991
Conference on Programming Language Design and Implementation, pages 293–305, New York, NY, June
1991. ACM.