Hey Daniel, On Wed, Dec 17, 2008 at 00:58, Daniel Drienyovszky 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:data...), 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