[Haskell-cafe] Fast times at Inferable-but-not-Checkable High.

[Peter Verswyvelen]

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 <jfredett at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091007/bb93b856/attachment.html