[Haskell-cafe] generics question, logical variables

[Frederik Eaton]

Hi Ralf,

I'm revisiting this project and just have another question. The story
seems to be that GHC cannot derive Typeable1, or Typeable when
Typeable1 is available - so anyone who wants to use ext1Q must define
special instances for all of the datatypes they use, is this correct? 
Will this change soon?

Aside from that, your 'idify' in PseudoFmap2 certainly seems to have
the correct type for this application. However, the absence of
automatic derivation is somewhat of an impediment.

Thanks for your help.

Frederik

On Tue, Aug 30, 2005 at 02:25:08PM -0700, Ralf Lammel wrote:
> 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
> 



-- 
http://ofb.net/~frederik/