From oleg-at-okmij.org Mon Aug 14 17:00:35 2006
Date: 14 Aug 2006 16:00:35 -0000
Message-ID: <20060814160035.17319.qmail@eeoth.pair.com>
To: haskell-cafe
In-Reply-To: <a49071280608091556ma04860ct6fd9bb6e4984ad0c@mail.gmail.com>
Subject: Local functional dependencies: solving show . read and 
  XML generation problems
Status: OR


Sorry for a late reply, I'm out of town.

As I understand it, the problem is as follows: we'd like to construct
different realizations of XML documents from data of different
types. We wish to write
       p (p "foo")
and specify the desired type of the XML document, like
       (p (p "foo")) :: XMLTree
or
       (p (p "foo")) :: IO ()  -- for writing out the XML document
etc. 

The function 'p' obviously has to be overloaded with the 
type |p :: a -> xml|.  However, |p (p "foo")| exhibits the `show . read'
problem. What should be the result type of the internal `p'?
Functional dependencies help resolve the ambiguity; alas, we can't
assert any dependency here. We should be able to use Strings
with XML documents of different types, so we can't assert the argument
of 'p' determines the result. Also, XML documents of the same type can
be created from children of different types. We indeed have the
`show . read' problem.

Fortunately, there is a solution that does not involve proxies or
type annotations. We use a `syntactic hint' to tell the typechecker
which intermediate type we want. To be more precise, we assert local
functional dependencies. Thus we can write:

     p c = build "p" [embed c]

     test1 :: XML
     test1 = p [[p [[p "foo"]]]]

Our syntactic crutch is the list notation: [[x]]. We could have used a
single pair of brackets, but we'd like to avoid overlapping
instances (as is done in the following self-contained code).

> {-# OPTIONS_GHC -fglasgow-exts #-}
> {-# OPTIONS_GHC -fallow-undecidable-instances #-}
> module GenXML where
> 
> data XML = Element String [XML] | CDATA String deriving Show
> 
> class Build child xml | xml -> child where
>     build :: String -> [child] -> xml
> 
> instance Build XML XML where
>     build = Element
> 
> -- This type class has no functional dependency
> 
> class Embed a child where
>     embed :: a -> child
> 
> instance Embed String XML where
>     embed = CDATA
> 
> -- This instance exhibits the functional dependency child -> a
> instance TypeCast a XML => Embed [[a]] XML where
>     embed [[x]] = typeCast x
> 
> 
> p c = build "p" [embed c]
> 
> test1 :: XML
> test1 = p [[p [[p "foo"]]]]
> 
> -- Our silver bullet
> 
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x