[Haskell-cafe] generics question, logical variables

[Frederik Eaton]

Ralf,

> Thanks for the challenge.

Wow, thanks for taking an interest. I'm sorry for my slow response,
I've been sick.

Ah, I haven't seen your SYB3 yet, I will have to take some time to
read it.

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?

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

It seems to result in a lot of bookkeeping, e.g.:

data Pair tx ty ax ay ( h :: * -> * ) a = Pair (tx h ax) (ty h ay)
instance (Term tx v ax, Term ty v ay) => Term (Pair tx ty ax ay) v (ax,ay)

The whole purpose of my project is to get something which resembles
logical variables in Haskell with minimal syntactic overhead.

> 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.)

What I am trying to do is an extension of a paper by Koen Claessen and
Peter Ljunglof:

http://citeseer.ist.psu.edu/claessen00typed.html

Here is the code I have written:

http://ofb.net/~frederik/GenLogVar.hs

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.

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.

I won't have time to work on this much more, but one motivation I had
was that if I can get this working, then a possible next step would be
to map the logical variable syntax onto SQL database queries, rather
than interpreting it directly in Haskell. The mapping would be a bit
higher-level than HaskellDB. Haskell algebraic data types themselves
would turn into sets of SQL tables. Each constructor would correspond
to a table. A value of a type would be a pair (table, index) where
"table" tells you the constructor and "index" is the primary key into
the table. In addition other indices would be specified to exist for
querying, and range queries could be done by extending the logical
variable semantics, substituting a Range datatype for Maybe in
variables. It's probably a lot more complicated than this but I think
it would be fun to try.

Frederik



> 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
> 
> 



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