[Haskell-cafe] generics question, logical variables

[Ralf Lammel]

Frederik,

> As for your code example, it looks very interesting, but are you
> saying that this could turn into an extension of the Data.Generics
> library, or that this is something I could be implementing in terms of
> what's already there?

The posted code works with GHC 6.4 (SYB2) intentionally and actually. I
have attached another attempt (again GHC 6.4, based on SYB2) which might
be more useful for your purposes, and it may be useful in general, in
fact.

What I defined this time is a "certainty-improving" function:

idify :: (Typeable1 f, Monad m, Data (a f), Data (a Id))
      => (forall a. f a -> m a) -> a f -> m (a Id)

That is, the function "idify get" takes a value whose type is
parameterized in a type constructor f (such as Maybe or IORef), and the
function attempts to establish Id instead of f on the basis of the
function argument "get".

> What is the 'a' parameter for in "force"?
> 
> force :: ( Data (t Maybe a)
>          , Data (t Id a)
>          , Term t Maybe a
>          , Term t Id a
>          ) => t Maybe a -> t Id a

The previous attempt was a more parameterized blow than required in your
case. (I was guessing about what "typed logical variables" could mean.
I was assuming that you would need some extra layer of embedding types
on top of the Haskell term types. Looking at your code, this was not the
case.)
 
> For the part which I asked for help with, to get around my trouble
> with generics, I defined a class GenFunctor and an example instance.
> The intent is that generics should be able to provide this
> functionality automatically later on, but you can see what the
> functionality is.

Let's look at the type of your GenFunctor:

class GenFunctor f where
    gfmapM :: (Monad m, FunctorM b) => (forall x . a x -> m (b x)) -> f
a -> m (f b)

This type can be seen as a more relaxed version of the idify operation
above. That is, idify fixes GenFunctor's b to Id. The particular
encoding of idify (attached) takes advantage of this restriction. I
wonder whether I should bother. (Exercise for reader :-))

> However, I am stuck on something else, the program doesn't typecheck
> because of use of another function I defined, 'cast1'. Maybe you can
> take a look. I had thought that I would be able to write a generic
> 'unify' but I get the error:
> 
> GenLogVar.hs:82:19:
>     Ambiguous type variable `a' in the constraint:
>       `Data a' arising from use of `cast1' at GenLogVar.hs:82:19-23
>     Probable fix: add a type signature that fixes these type
variable(s)
> 
> This is because I need to do something special when I encounter a
> "Var" variable in unification, but the compiler seems to not like the
> fact that the type argument of the Var data type is not known.

Please try to avoid new cast operations at all costs. :-)
Your code can be arranged as follows:

(i) Use extQ1 to dispatch to a special case for "Var x" for the first
argument. (ii) In this special case, use again ext1Q to dispatch to a
special case for "Var y" for the second argument. (iii) At this point,
*cast* the variable value of *one* variable to the type of the other.

So the problem with your code, as it stands, is that the target type of
cast is ambiguous because you cast *both* arguments. The insight is to
make the cast asymmetric. Then, not even polymorphism is in our way.

Interesting stuff!

Ralf

-------------- next part --------------
A non-text attachment was scrubbed...
Name: PseudoFmap2.hs
Type: application/octet-stream
Size: 4723 bytes
Desc: PseudoFmap2.hs
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050830/feece8fa/PseudoFmap2.obj