[Haskell-cafe] Fast times at Inferable-but-not-Checkable High.
bugfact at gmail.com
Wed Oct 7 02:52:15 EDT 2009
I don't have an answer to your question, but I asked a similar one a while
Ingram gave an answer:
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
> 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`
> 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
> 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 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
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe