[Haskell-cafe] generics question, logical variables

[Ralf Lammel]

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 at haskell.org [mailto:haskell-cafe-
> bounces at haskell.org] On Behalf Of Frederik Eaton
> Sent: Sunday, August 28, 2005 9:36 PM
> To: haskell-cafe at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe


-------------- next part --------------
A non-text attachment was scrubbed...
Name: PseudoFmap.hs
Type: application/octet-stream
Size: 4952 bytes
Desc: PseudoFmap.hs
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050829/a5d6367e/PseudoFmap.obj