
 `adt_view`: A Haskell Preprocessor for Gradual Refinement Support for Abstract Data Types
======================================================



 What is this?
---------------

This is an implementation of the paper "Gradual Refinement: Blending Pattern Matching with Data Abstraction" written by Meng Wang et al.

With this system, in Haskell, you can pattern-match on ADTs 
via its abstraction.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.haskell}
{-# OPTIONS -XTemplateHaskell -XMultiParamTypeClasses #-}
import UpdatableViewStub 

spec Q a = None 
         | More a (Q a) deriving (Show, Eq) where 
    isEmpty :: Q a -> Bool 
    isEmpty None = True 
    
    emptyQ :: Q a 
    emptyQ = None

    enQ :: a -> Q a -> Q a 
    enQ a None = More a None 
    enQ a (More b x) = More b (enQ a x)

    deQ :: Q a -> Q a
    deQ (More a x) = x

    first :: Q a -> a  
    first (More a x) = a 
impl Qi a = Qi [a] [a] deriving (Show, Eq) where
    enQ :: a -> Qi a -> Qi a 
    enQ a (Qi x y) = Qi x (a:y)

    deQ :: Qi a -> Qi a
    deQ (Qi (a:x) y) = Qi x y
    deQ (Qi [] y)    = deQ (Qi (reverse y) [])

    first :: Qi a -> a 
    first (Qi (a:x) y) = a 
    first (Qi [] y)    = first (Qi (reverse y) [])
abstractedBy
    view = $(foldT ''Qi) ( (idB <**> reverseB) >>>> appendB) >>>> l2l 
          where l2l = $(foldT ''[]) ( $(toC 'None) <||> $(toC 'More) )

mapQ f None       = None 
mapQ f (More a x) = More (f a) (mapQ f x)

play1 0     q = first q 
play1 (n+1) q = do hd 
                   play1 n (enQ hd tl)
   where hd = first q 
         tl = deQ   q 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Since the views are defined by bidirectional language [`rinv`](#rinv-right-inverse-language),
you can access the original data by both decomposing and composing the views.


Using this system is quite easy; just use it as a preprocessor for [GHC].
If you want to compile "FILENAME.hs" including viewdata, just type as follows.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.shell}
> ghc -F -pgmF adt_view FILENAME.hs 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Of course, you can use the system through `ghci` interpreter.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.shell}
> ghci -F -pgmF adt_view FILENAME.hs 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

[GHC]: http://www.haskell.org/ghc/


 How to build
--------------

  1. Download tar file: [adt_view.tar.gz](./adt_view.tar.gz)
  2. Unpack the tar file: `tar zxvf adt_view.tar.gz`
  3. `make`
     - In case of trouble, please edit make file to fix the problem.
     - `adt_view` (or, `adt_view.exe` in Windows) is the name of the preprocessor.
     - Directory `examples` contains some examples.
     - Directory `lib` contains Haskell source files 
       for view data.

Since the module name of the libraries for updatable views are still tentative, 
we do not install them automatically.
Please put the files under `lib` directory to your favorite place and 
include them by `-iDIRECTORY` in compilation.


 `rinv`: Right-Inverse Language
---------------------------------
In our framework, views are defined by bidirectional transformations described by
`rinv` language.
Thanks to the properties guaranteed by the `rinv` language, 
we can avoid the situations that view updating result is counter-intuitive for users.

As the above example, `rinv` is pointfree combinator-based language.
You can use the following primitives in the language.


`f >>>> g`
:    Sequential composition of two transformations.

`f <**> g`
:    Application of "f" and "g" to each element of pairs.

`f <&&> g`
:    It tuples the result of application of "f" and "g" to input.

`f <||> g`
:    It applies "f" if the input is `Left x`, and
     applies "g" if the input is `Right x`.

`f <++> g`
:    Similar to above but it keeps tags (`Left`/`Right`).

`$(toC C')`
:    This applies the constructor `C` to the input.

`idB`
:    It just returns input as is.


`$(fold ''T)`
:    The function is "fold" on datatype `T`.
     For example, "fold" on `[a]` is defined as follows.     
     <pre><code class="haskell">$(fold ''[]) = fold 
            where fold fB = $(fromT ''[]) >>>> right (second (fold fB)) >>>> fB</code></pre>
     Currently, it only works only if T is  very simple type, i.e., polynomial.
     It does not work for mutually recursive types.
     

Users also can use predefined combinators as `reverseB` and `appendB`.


One would think why do we use Arrows.
However, because of bidirectionality, this language does not follow Arrow laws. 
For example, `arr id >>>> f = f` does not hold because `arr id` does not know anything about inverse direction.


 Code Translation Example
---------------------------

Our system is defined as preprocessor for GHC.
Since we hope that some people interested in how the above "viewdata" codes are translated to Haskell code, 
we put here some of translation examples.


<table summary="code conversion result">
<thead>
 <tr><th>Short Description</th><th>Code with `viewdata`</th><th>Preprocessed Result</th></tr>
</thead>
<tbody>
 <tr>
   <th>Queue/List</th>
   <td>[queue.hs](examples/queue.hs)</td>
   <td>[queue.hspp](examples/queue.hspp)</td>
 </tr>
 <tr>
	<th>SizedTree</th>
	<td>[sizedtree.hs](examples/sizedtree.hs)</td>
	<td>[sizedtree.hspp](examples/sizedtree.hspp)</td>
 </tr>
 <tr>
	<th>Binary Number</th>
	<td>[msblsb.hs](examples/msblsb.hs)</td>
	<td>[msblsb.hspp](examples/msblsb.hspp)</td>
 </tr>
</tbody>

</table>





<div class="footer">

----------------------


<address>Kazutaka Matsuda: <kztk@kb.ecei.tohoku.ac.jp>.</address>

The first version of this page was published in 2011-01-10.

</div>
