Re: [Haskell-cafe] generics question, logical variables
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
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 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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 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:[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 ::
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/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] generics question, logical variables
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 PseudoFmap2.hs Description: PseudoFmap2.hs ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] generics question, logical variables
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 gener
RE: [Haskell-cafe] generics question, logical variables
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
