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