I don't have an answer to your question, but I asked a similar one a while ago:http://www.mail-archive.com/haskell-cafe@haskell.org/msg53872.html
<http://www.mail-archive.com/haskell-cafe@haskell.org/msg53872.html>Ryan Ingram gave an answer: http://www.mail-archive.com/haskell-cafe@haskell.org/msg53941.html Maybe this helps. On Wed, Oct 7, 2009 at 7:10 AM, Joe Fredette <jfred...@gmail.com> wrote: > So, I've been fiddling with an utterly random idea. What if I had a class: > > class Hom a b where > data Rep a b > hm :: Rep a b -> b > im :: a -> Rep a b > > That is, all types that have some conversion between them (an isomorphism > originally, then I thought homomorphism, now I'm not sure what the hell I'm > talking about, so I've just stuck with Hom...) which preserves some sense of > "structure" and "content", for instance > > > data CouldBe a = Only a | Nada > > is _obviously_ the same type as `Maybe`. However, it can't be used > transparently where `Maybe` can be used. That is, shouldn't I be able to > define a 1-1, onto function `phi :: CouldBe a -> Maybe a` and as such > another `pho :: Maybe a -> CouldBe a` such that > > phi . pho = pho . phi = phum ... errr. `id`? > > Hom a b represents one end of that (specifically `hm . im = phi`, and `hm . > im` for the instance `Hom b a` would `pho`), then I could, instead of > writing a type which expects maybe, simply expects anything _equivalent_ to > a maybe, eg > > safeHead :: Hom (Maybe a) b => [c] -> Rep a (Maybe c) > safeHead [] = im Nothing > safeHead (x:_) = im (Just x) > > Though- I think this is a little bit off in terms of how it should work, > perhaps this is my problem, but the idea is that instead of returning a > Maybe, it returns something which can be converted _from_ a maybe. That is, > a "generic" type like: > > data X1 a = X a | Y > > which is the "form" of any "maybe-like" type. > > In one sense, I'm almost trying to be polymorphic over the constructors of > a given type, kindof, sortof, if you squint your eyes just right and try not > to think too much. > > My problem comes when I try to do this: > > hom = hm . im > eq x y = hom x == hom y > > Which, I reason, ought to satisfy the type: > > eq :: (Hom a b, Eq b) => a -> a -> Bool > > this assumes that hom defines a equality-preserving conversion. However, > the type it infers is: > > eq :: (Hom a b, Hom a1 b, Eq b) => a -> a1 -> Bool > > Now, this makes sense, all my signature is is a special case of this type. > Interesting consequence, this eq could compare a `Maybe a` and `CouldBe a` > in a sensical way. Which is a nice benefit. However, here's where it gets > weird, If I try to _provide_ this signature (the second, more general one, > or the first, specific one, it doesn't matter), GHC gives me the following > error: > > Iso.hs:29:10: > Could not deduce (Hom a b) from the context (Hom a b1, Eq b1) > arising from a use of `hom' at Iso.hs:29:10-14 > Possible fix: > add (Hom a b) to the context of the type signature for `eq' > In the first argument of `(==)', namely `(hom x)' > In the expression: (hom x) == (hom y) > In the definition of `eq': eq x y = (hom x) == (hom y) > Failed, modules loaded: none. > > for the latter and a similar one (but for each of the `Hom a b`, `Hom a1 b` > cases. > > Punchline is this, I'm trying to write a generic equality that works for > any two types with the same constructor-structure, when I try to write said > function, GHC can infer but not Check (it seems, I'm not sure if that's the > correct lingo) the type... > > My question is twofold. > > 1. Is this whole idea even possible? I mean- is there some limitation I'm > going to run into, I have run into problems when trying to do: > > instance (Hom a b, Eq b) => Eq a where > blah > > wrt UndecideableInstances. But it seems so _obvious_ what that means, I > don't think I fully understand what's going on -- that is, whether I'm > misunderstanding how class contexts work here, and why this (seemingly > obvious) signature is undecidable, or whether I'm just mistaken in my type > signature all together. (My goal is to say that anything which can be > converted freely to and from something that is an instance of the Eq class, > must preserve the equality relationships. > > 2. Why is GHC unable to check the types, but infer them. I always > understood inferring to be the "hard" part of the problem, and checking to > be the "easy" part. Is my intuition wrong? > > I've posted the code here[1] for your perusal. It's not particularly > important that I get this solved, it's just a random idea I wanted to > explore and thought the notion might appeal to some other Haskeller's around > there who like to have self-documenting datatypes, but hate having to > rewrite lots of simple utility functions as penance for our documentarian > sins. > > /Joe > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
