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.

{-# 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, 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.

> ghc -F -pgmF adt_view FILENAME.hs 

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

> ghci -F -pgmF adt_view FILENAME.hs 

How to build

1. Download tar file: 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.

$(fold ''[]) = fold 
        where fold fB = $(fromT ''[]) >>>> right (second (fold fB)) >>>> fB

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.