RE: [Haskell-cafe] generics question, logical variables

[Simon Peyton-Jones]

Ralf,

I'm a bit snowed under at the moment with the POPL PC meeting, but I'm
quite open to changing GHC's deriving behaviour.  It's not hard to
change.  The hard thing is figuring out just what the specification
should be.

So if you and others are able to evolve a better design, I'd be happy to
implement it.  (And of course think about it too.)

I'm afraid that full-blown kind polymorphism is probably a bit of a
stretch, though it comes up every now and again.  So the best
monomorphic compromise would be good.

There's also the question of whether we should make any changes in GHC's
libraries to take SYB3 (using classes) into account...

Simon


| -Original Message-
| From: Ralf Lammel
| Sent: 19 September 2005 04:34
| To: [EMAIL PROTECTED]
| Cc: haskell-cafe@haskell.org; Simon Peyton-Jones
| Subject: RE: [Haskell-cafe] generics question, logical variables
| 
| 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 n0 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] generics question, logical variables

[Yitzchak Gale]

Ralf Lammel wrote:

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

Here are two possible simple examples.

The first is from real life: I once needed a
polymorphic function replace that replaces an
element of an n-dimensional list given its
coordinates and a replacement value:

replace :: Int - a - [a] - [a]
replace :: Int - Int - a - [[a]] - [[a]]
etc.

Also, trivially, in dimension zero:

replace :: a - a - a

So we have:

dim 0: replace = const

dim 1: replace i x (y:ys)
| i == 0= replace x y : ys
| otherwise = y : replace (i-1) x ys
   replace _ _ _ = []

dim 2: replace i j x (y:ys)
| i == 0= replace j x y : ys
| otherwise = y : replace (i-1) j x ys
   replace _ _ _ _ = []

etc.

Intuitively, this ought to be simple. But I leave
it as an exercise for the reader to implement it
using the current type system. What a mess!

Second example:

It seems intuitive that the State monad should
be isomorphic to the lazy ST monad with STRef, in
the sense that it should be possible to implement
each monad in terms of the other.

(For the purpose of this discussion, let us ignore
differences in strictness due to the execution
strategies of any given compiler, though that also
may be an interesting topic.)

Well, in one direction that is trivial - it is easy
to implement State using lazy ST and STRef.

As for the other direction - yuck! Again, I leave
it as an exercise for the reader.

Regards,
Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [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 n0 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:[EMAIL PROTECTED]
 Sent: Sunday, September 18, 2005 7:50 PM
 To: Ralf Lammel
 Cc: haskell-cafe@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

RE: [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: [EMAIL PROTECTED] [mailto:haskell-cafe-
 [EMAIL PROTECTED] 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




PseudoFmap.hs
Description: PseudoFmap.hs
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] generics question, logical variables

[Frederik Eaton]

 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: [EMAIL PROTECTED] [mailto:haskell-cafe-
  [EMAIL PROTECTED] 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
 
 



-- 
http://ofb.net/~frederik/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] generics question, logical variables

[Frederik Eaton]

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