Frederik, Thanks for the challenge. I didn't get some of the bits about your application scenario though. (What did you mean by the type Pred? Why a list in the result of solve? How did you model typed logical variables? With GADTs, phantoms? ... Perhaps send more code, if you want to discuss this topic more.) So I hope that the attached make sense to you. I do believe so. I have coded a function that converts a term "t Maybe a" to a term "t Id a", where I assume that: - "t" is the Haskell type that may involve Maybe/Id "spots". - Maybe/Id spots for variables are wrapped in a dedicated datatype Spot, - "a" is the type of the term with regard to some custom type system. - The custom type system is model as a class Term. Here is the conversion function: force :: ( Data (t Maybe a) , Data (t Id a) , Term t Maybe a , Term t Id a ) => t Maybe a -> t Id a force = fromJust . tree2data . data2tree This example assumes that all Maybe spots are actually Just values. Clearly, you can do some error handling in case this cannot be assumed. You could also make the Maybe-to-Id conversion part of the traversal that resolves "holes". This is not the challenge, the challenge was indeed to traverse over a term and to "get the types right" when replacing subterms of type Maybe x by subterms of type Id x. The actual type conversion relies on going through the universal Tree datatype. We use "Tree Constr" as the type of an intermediate value. (We could also use "Tree String" but this would be more inefficient. BTW, we take here dependency on the invariant that constructors in Constr are polymorphic. So SYB's reflection is nicely generic; compare this with Java.) When encountering spots during trealization, they are converted from Maybies to Ids. Then, a subsequent de-trealization can do its work without any ado. The deep trealization solves the problem of exposing these type changes to the type of gfoldl. (Amazingly, one might say that the type of gfoldl is just not general enough!) I guess I should admit that: - We temporally defeat strong typing. - We make the assumption that all occurrences of Spot are to be converted. - That is, we don't quite track the type parameter for Maybe vs. Id. - This is a bit inefficient because of going through Tree Constr. So I am willing to summarize that this is potentially a sort of a (cool) hack. Code attached. Ralf P.S.: The extension you propose seems to be a major one. Perhaps you could look into the TH code for SYB3 (ICFP 2005) to see whether this can be automated. This sort of discussion calls for kind polymorphism once again.
-----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] On Behalf Of Frederik Eaton Sent: Sunday, August 28, 2005 9:36 PM To: haskell-cafe@haskell.org Subject: [Haskell-cafe] generics question, logical variables
Hi all,
I'm trying to write something like a generic fmap, or a generic natural transformation. The application is this. I have a typed logical variable library which produces arbitrary terms with values of type "Var a", which are references to a value of type "Maybe a", and I want to write a "solve" function which replaces these values with instantiated versions of type "Id a" where
newtype Id a = Id a
. Furthermore I want this to be reflected in the type of the generic term:
solve :: Pred (t Var) -> [t Id]
so if I have a type like
data Entry k = Entry (k String) (k Int)
then I can write some constraint equation with values of type "Entry Var", and get back values of type "Entry Id" - in other words, objects where the unknowns are statically guaranteed to have been filled in.
I looked at the generics library. I may be mistaken, but it seems that it doesn't have what I need to do this. The problem isn't the mapping, it's creating a new type which is parameterized by another type. The only options for creating new types are variations on
fromConstr :: Data a => Constr -> a
but what is needed is something like
fromConstr1 :: Data1 a => Constr1 -> a b
With something like that it should be possible to define:
gmapT1 :: (forall b . Data1 b => b l -> b m) -> a l -> a m
Does this make sense? Here I would be treating all instances of Data as possibly degenerate instances of Data1 (which just might not depend on the type variable).
If it seems like a good idea, I would be interested in helping out with the implementation.
Frederik
-- http://ofb.net/~frederik/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe