Hey Daniel,

On Wed, Dec 17, 2008 at 00:58, Daniel Drienyovszky <drienyovszky@gmail.com> wrote:
Hi, 

I'm trying to write a generic nominal abstract syntax library, and I
ran into a problem using ext1T. I asked around at #haskell but no one
was able to help me, I hope this is not too off topic here.

It's definitely on-topic :-)
 



substAbs works just fine by itself, but when I try to combine it with
something using ext1T, it stops working. I can't figure out what's the
problem with this, am I doing something wrong?

*Main> substAbs $ a :\\: a



Name "a" (Just 1) :\\: Name "a" (Just 1)
*Main> id `ext1T` substAbs $ a :\\: a
Name "a" Nothing :\\: Name "a" Nothing

Here is my code:

>{-# LANGUAGE DeriveDataTypeable #-}


>
>import Data.Generics
>
>data Name = Name String (Maybe Int) 
>            deriving (Eq, Show, Data, Typeable)
>
>refresh (Name s Nothing) = Name s (Just 1)
>refresh (Name s (Just i)) = Name s (Just $ i+1)


>
>data Abs a = Name :\\: a deriving (Eq, Show, Data, Typeable)
>
>swapName (a,b) x = if a == x then b else
>                       if b == x then a else x
>
>swap (a,b) = everywhere (mkT $ swapName (a,b))


>
>substAbs (n :\\: x) = (m :\\: (x'))
>    where m = refresh n
>          x' = swap (n,m) x
>
>a = Name "a" Nothing
>b = Name "b" Nothing

First, some naming. (I prefer to use undefined instead of id so that we get an error immediately when it's applied, but it works the same with id)

y, z :: Name
y = Name "y" Nothing
z = Name "z" Nothing

t0, t1, t2 :: Abs Name
t0 = y :\\: y
t1 = substAbs $ y :\\: y
t2 = undefined `ext1T` substAbs $ y :\\: y


Now let's expand t2 to see what's happening:

newtype T x = T { unT :: x -> x } -- defined in Data.Generics.Aliases, not exported
-- ext1T def ext = unT ((T def) `ext1` (T ext))
t3 :: Abs Name -> Abs Name
t3 = unT (ext1 undefined (T substAbs))

ext1 :: (Data a, Typeable1 t) -- defined in Data.Generics.Aliases, not exported
     => c a
     -> (forall d. Data d => c (t d))
     -> c a
ext1 def ext = maybe def id (dataCast1 ext)

t4 :: Abs Name -> Abs Name
t4 = unT (maybe undefined id (dataCast1 (T substAbs)))


Now, according to the documentation of dataCast1 (http://haskell.org/ghc/docs/latest/html/libraries/base/Data-Data.html#v:dataCast1), it should be defined as gcast1:

t5 :: Abs Name -> Abs Name
t5 = unT (maybe undefined id (gcast1 (T substAbs)))


And then it all works:
 
t6 :: Abs Name
t6 = t5 t0


t6 is the same as t1. The problem is that dataCast1 is apparently not defined as such, but instead keeps the default definition of const Nothing. This is obviously not what is wanted here, and so you get the behavior of t2.

This can been seen if we dump the generated Data instances. For some common datatypes:

{-# OPTIONS -ddump-deriv          #-}
{-# LANGUAGE DeriveDataTypeable   #-}

module Test where

import Data.Generics

data List a = Nil | Cons a (List a) deriving (Data, Typeable)

data Pair a b = Pair a b deriving (Data, Typeable)

We can see that the generated instances for these datatypes do not define (respectively) dataCast1 and dataCast2, but they should.

So Daniel, a solution is to give your own instance of Data Abs:

instance (Data a) => Data (Abs a) where
  gfoldl f z (x :\\: y) = z (:\\:) `f` x `f` y
  gunfold k z c = k (k (z (:\\:)))
  dataCast1 f = gcast1 f

And now t1 behaves as t2. However, I believe the deriving mechanism should have derived the correct instance for you...


Thanks,
Pedro