Fast times at Inferable-but-not-Checkable High.

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Fast times at Inferable-but-not-Checkable High.

jfredett
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fast times at Inferable-but-not-Checkable High.

Peter Verswyvelen-2
I don't have an answer to your question, but I asked a similar one a while ago:

Ryan Ingram gave an answer:

Maybe this helps.

On Wed, Oct 7, 2009 at 7:10 AM, Joe Fredette <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe