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
