[Haskell-cafe] generics question, logical variables

[Ralf Lammel]

Hi Frederik,

[I call this "the dreadful lack of kind polymorphism strikes back" :-)]

I put SPJ on cc; perhaps he can suggest a way to improve in this area.
Based on input, I could try to work on this issue in the not so remote
future.

Let me briefly recapitulate. My recollection is that deriving works for
Typeable, Tyepable1, ..., if all type parameters are of type kind "*".
Whenever you can derive a Typeablen instance with n > 0, you can instead
ask for Typeable to be derived. The reason why you cannot get both a
Typeable and say a Typeable42 instance is that there are generic
instances for getting an "n-1 instance" from the "n instance". However,
this is also precisely the reason why you don't want them both. That is,
you get everything you can ask for, if you have the "n instance" for the
actual arity of the type constructor in question. (Getting a smaller n
or no n just means that you limit polymorphic type case.) Recall that
you *may* need a n>0 instance if you want to do polymorphic type case
according to the SYB2 paper. As long as you are fine with monomorphic
generic function extension, the plain Typeable instance should be fine.

However, the real limitation is here, *indeed*, as said, that GHC does
not derive Typeable[1|2|...] for parameter kinds other than "*". This
was the reason that I had to hand-code some Typeable instances in your
original example.

Let us also be honest about another limitation of the current deriving
code. "deriving Data" gives you Data instances that do *not* support
polymorphic type case. That is the following code prints 0, 1, 0 whereas
you may expect  0, 1, 2.

newtype Foo x = Foo x deriving (Typeable, Data)

f :: Data a => a -> Int
f = const 0
    `ext1Q` (\(_::Maybe x) -> 1)
    `ext1Q` (\(_::Foo y)   -> 2)

main = do
          print $ f True
          print $ f (Just True)
          print $ f (Foo (Just True))


This is the reason that I had to handcode some Data instances in your
original example, which wasn't hard BTW. We thought that these two
limitations were Ok since we didn't expect people to write many
polymorphic datatype constructors on which SYB should work. Sounds like
a feature request.

Now I wonder how much work it is to improve the situation. We need to
make the GHC deriving code a bit more kind-aware. I guess we are still
not at the point where we want to add kind polymorphism to Haskell?
Would be a nice topic for future work on SYB. Clearly, the GH folks have
done splendid work in this area. Getting full-blown kind polymorphism in
normal Haskell though seems to be less of a topic, simply because we do
not have many scenarios around that would *really* require it.

Does anyone want to speak up and mention scenarios that would benefit
from kind polymorphism? (In Haskell, we are likely to see kind
polymorphism, if at all, in the form of type classes whose type
parameters can be of different, perhaps of all kinds.)

Frederik, for the time being I propose to look into TH code for deriving
Tyepable/Data instances and to make it fit for your purposes. There are
several versions of Ulf Norell's code around. You may also use SYB3 with
the TH code that readily comes with it.

Thanks for bringing this up.

Regards,
Ralf

> -----Original Message-----
> From: Frederik Eaton [mailto:frederik at a5.repetae.net]
> Sent: Sunday, September 18, 2005 7:50 PM
> To: Ralf Lammel
> Cc: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] generics question, logical variables
> 
> 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/