[Haskell-cafe] Re: Monad explanation

[Benjamin L.Russell]

On Wed, 4 Feb 2009 21:43:04 -0800, Max Rabkin <max.rabkin at gmail.com>
wrote:

>On Wed, Feb 4, 2009 at 9:38 PM, Benjamin L. Russell
><DekuDekuplex at yahoo.com> 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^