[Haskell-cafe] Re: Monad explanation

On Wed, 4 Feb 2009 21:43:04 -0800, Max Rabkin wrote:

On Wed, Feb 4, 2009 at 9:38 PM, Benjamin L. Russell wrote:

...

Is it possible to write a self-referential function in Haskell that modifies itself?

Is it possible to write *any* kind of function in Haskell that modifies *anything*?

While trying to research this issue, I came across a relevant archived thread in Haskell-Cafe, entitled "[Haskell-cafe] haskell and reflection," started by Greg Meredith, dated "Tue, 11 Sep 2007 07:09:22 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29882.html), which at first had me worried. Specifically, Greg wrote as follows:

Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

- there is no runtime representation of type available for programmatic representation - there is no runtime representation of the type-inferencing or checking machinery - there is no runtime representation of the evaluation machinery - there is no runtime representation of the lexical or parsing machinery

However, I was somewhat relieved to find that Haskell apparently does support, in at least one GHC extension to Haskell, a limited form of reflection. In the same thread, Reinier Lamers, in his response, dated "Tue, 11 Sep 2007 13:08:38 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29898.html), wrote as follows:

Op 11-sep-2007, om 18:43 heeft Greg Meredith het volgende geschreven:

[...]

Template Haskell [1] is a system that lets you write programs that get executed at *compile time*, and that produce parts of the Haskell program to be compiled by manipulating a representation of the program as structured data. It's a form of reflection restricted to compile time, if you'd ask me.

[...]

[1] http://www.haskell.org/haskellwiki/Template_Haskell

According to the site referenced by the above-mentioned link,

Template Haskell is an extension to Haskell 98 that allows you to do type-safe compile-time meta-programming, with Haskell both as the manipulating language and the language being manipulated.

This site is even referenced on the site for "The Meta-Programming Project" (see http://www.infosun.fim.uni-passau.de/cl/metaprog/index.php3), as follows:

Languages which we are using for meta-programming

* Template Haskell, permits analysis of object programs

Additionally, Don Stewart, in an earlier post in the same thread, dated "Thu, 13 Sep 2007 11:36:11 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg30009.html), wrote as follows:

lgreg.meredith:

...

Haskellians,

Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

* there is no runtime representation of type available for programmatic representation

...

* there is no runtime representation of the type-inferencing or checking machinery

...

* there is no runtime representation of the evaluation machinery

...

* there is no runtime representation of the lexical or parsing machinery

So there is library support for all of this, in various forms:

* lexer, parser, type checker, evaluator: ghc-api hs-plugins

* lexer, parser, pretty printer many parser libs (Language.Haskell, Template Haskell)

* runtime type representation Data.Typeable

* reflecting code to data: Data.Generics

As a sidenote, I discovered an interesting post and associated paper by Lauri Alanko, who in a post in the same thread, dated "Tue, 11 Sep 2007 10:12:09 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29895.html), responded that while both structural and procedural reflection are possible in Haskell, because of static typing, type safety is nevertheless an issue:

On Tue, Sep 11, 2007 at 07:33:54AM -0700, Greg Meredith wrote:

...

Our analysis suggested the following breakdown

- Structural reflection -- all data used in the evaluation of programs has a programmatic representation - Procedural reflection -- all execution machinery used in the evaluation of programs has a programmatic representation

[...]

As for Haskell, there are various tools for both (at least Data.Typeable and hs-plugins), but neither are truly type-safe: it is possible to write code that uses these libraries and type-checks, yet crashes. Static typing makes reflection very difficult to support safely.

You might be interested in my MS thesis, where I explored these issues in some more length: http://www.cs.helsinki.fi/u/lealanko/alanko04types.pdf

This thesis is entitled "Types and Reflection" (see the above-mentioned URL), and summarizes the problem as follows (see p. 1):

This thesis is about reflection in typed programming languages. The central idea of this work, the thesis proper, can be summarized in three points: . Typed reflection is a good thing. . It has not yet been done properly. . It is nevertheless possible.

The basic problem with reflection in a statically typed language seems to be that "reflection wreaks havoc to the basic assumptions that type systems are based on" (see p. 11). Specifically, he explains as follows (see p. 38):

[A] type system verifies or infers universal properties about all possible executions of a program by making a context-sensitive syntactic analysis of the program’s structure. Usually this is possible because the computational rules for executing the program are simple, tractable and most importantly syntax-directed: the evaluation of each expression proceeds in a predictable fashion that is determined mostly by its syntactic form and only to a limited extent by run-time state. For each expression there are certain invariants that always hold for its evaluation, and these invariants can be expressed in the expression’s type.

In practice this means that we can prove the soundness of a type system with structural induction over the terms, using the dynamic semantics of the language to show that the evaluation of each expression will yield a well-typed result.

In the presence of reflective operations this mode of reasoning no longer works. The reason is that the effects of all primitive expressions on computational structures are no longer simple and tractable: an absorption operation turns an arbitrary run-time value into a computational structure, and there are therefore no simple invariants about the operation’s behavior.

This is of course an inherent property of reflection. Its idea, after all, is to allow the program more freedom at run-time instead of completely predefining its behavior when the program is written. Yet it is still a rarely used feature and it seems unreasonable that it should make static typing completely unattainable. Thankfully, this proves not to be the case.

In Greg Meredith's solution, he writes as follows (see p. 42):

[T]here is a tradeoff to be made between static safety and dynamic flexibility. It turns out that it is possible to do quite sophisticated run-time code manipulation while still retaining fully static safety guarantees both of the original code and the generated code.

In Section 8.3: "Dynamics in Haskell," Meredith elucidates as follows (see p. 62):

The language Haskell [H98] has a powerful type system, but the standard version of the language has no support for run-time type operations. However, there is a dynamics library that has for a long time been included in many implementations [LPJ03, Section 8]. The library provides a datatype Dynamic and some machinery for injecting values of different types into it and for extracting them out from it. Unfortunately, the user of the library is required to obey certain programming conventions, and if they are not followed, it is very easy to write code that breaks type safety. Moreover, the library provides only limited support for dynamics. For instance, it is not possible to inject polymorphic functions into a Dynamic.

More recently, Cheney and Hinze [CH02a] and Baars and Swierstra [BS02] have developed more flexible and type-safe frameworks for representing type information at runtime in Haskell. In fact, dynamic values are only one of the possible applications of the frameworks.

Cheney and Hinze's system is then described in more detail. Meredith then concludes as follows (see p. 63):

The above system is quite remarkable. The type Rep [tau]  bridges the gap between static and dynamic type information while remaining completely type-safe even internally. Indeed, the type representations are very much like reified types. They can be synthesized and analyzed, and the isomorphisms allow a kind of absorption: conversion from run-time to compile-time type information.

Some problems relating to the need for programmer cooperation, the treatment of new named datatypes, and lack of full reflexivity are then described. Nevertheless, Meredith summarizes as follows (see p. 64):

Nevertheless, these "lightweight dynamics" are surprisingly powerful, considering that they can be implemented in a statically typed language without extending the type system. For example, Baars and Swierstra demonstrate how to write a type-safe eval function for a simple language so that all type checking is done before the code is evaluated. Although this is not full reflection due to the simplicity of the object language, the result is still encouraging. For one thing, at least now a type can be pretty-printed even without the presence of a value of that type.

Apparently, there is hope for reflection in Haskell with such libraries. What would be especially interesting would be a specific example of a type-safe Haskell program that could modify itself at runtime. If anyone has any examples to cite, I would be very interested in reading about them in this thread. -- Benjamin L. Russell -- Benjamin L. Russell / DekuDekuplex at Yahoo dot com http://dekudekuplex.wordpress.com/ Translator/Interpreter / Mobile: +011 81 80-3603-6725 "Furuike ya, kawazu tobikomu mizu no oto." -- Matsuo Basho^