[Haskell-cafe] generics question, logical variables
ralfla at microsoft.com
Tue Aug 30 17:25:08 EDT 2005
> 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
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
> 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:
> 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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 4723 bytes
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050830/feece8fa/PseudoFmap2.obj
More information about the Haskell-Cafe