newtypeable, new cast?
Simon PeytonJones
simonpj at microsoft.com
Tue Jul 23 03:31:03 CEST 2013
Harump. There is *still* an infinite family going on here, isn't there?
gcast :: forall a b c. (Typeable a, Typeable b) => c a > Maybe (c b)
but what about this
gcast_2 :: forall a b c d e. (Typeable a, Typeable b, Typeable d, Typeable e)
=> c a b > c d e
Then, as you point out, we have gcast1 and 2 (etc). And there are more. What about
gcast1' :: forall c t a a'. (Typeable a, Typeable a')
=> c (t a) > Maybe (c (t a'))
One could imagine all sorts of combinations of bits that stay the same (and hence do not need to be Typeable) and bits that change (and hence do need to be Typable).
As Edward says, all these functions can be polykinded, which makes them more useful, but there still seem too many of them.
I wonder if we could instead make a combinatory library that lets us build these functions easily. It think we are going to offer a function that computes an equality witness:
mkEqWit :: (Typable a, Typeable b) => Maybe (EQ a b)
Now we need to be able to compose witnesses:
appEqWit :: Eq a b > Eq c d > Eq (a c) (b d)
reflEqWit :: Eq a a
Now, I think you can make all those other casts.
Would that do the job better?
Simon
 Original Message
 From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
 Sent: 22 July 2013 10:20
 To: José Pedro Magalhães
 Cc: Dimitrios Vytiniotis; Simon PeytonJones; Stephanie Weirich;
 josepedromagalhaes at gmail.com; libraries at haskell.org; Conor McBride
 Subject: Re: newtypeable, new cast?

 There seems to be a small tangle. The proposal includes deprecating
 gcast1 and gcast2 in favor of the polykinded gcast. But, there is a
 small discrepancy between these. Here are the type signatures:

 > gcast :: forall a b c. (Typeable a, Typeable b) => c a > Maybe (c b)
 > gcast1 :: forall c t t' a. (Typeable (t :: * > *), Typeable t')
 > => c (t a) > Maybe (c (t' a))

 The difference is that gcast1 does *not* require the variable `a` to be
 Typeable, whereas defining gcast1 = gcast does require this. Not
 requiring `a` to be Typeable seems correct to me, as the type signature
 of gcast1 requires both uses of `a` to be the same. But, gcast isn't
 smart enough to know that. Here are some ideas of how to proceed:

  Keep gcast1 and gcast2 undeprecated.
  Require clients to add more Typeable constraints (for example, in
 Data.Data) to get their code to compile with gcast.
  Come up with some other workaround, but none is striking me at the
 moment.

 Thoughts?

 Richard

 On 20130722 09:44, Richard Eisenberg wrote:
 > I was waiting to respond to Shachaf's email saying "pushed", but
 > instead, I have to say "currently validating".
 >
 > Expect this by the end of the day. Sorry it's taken so long!
 >
 > Richard
 >
 > On 20130722 09:23, José Pedro Magalhães wrote:
 >> Thanks for bringing this up again. This was started in my dataproxy
 >> branch of base [1],
 >> but never really finished. We definitely want to have this in 7.8, and
 >> I think there's
 >> only some minor finishing work to do (check if we have all the
 >> instances we want,
 >> document, etc.). Perhaps you can look through what's there already,
 >> and what you
 >> think is missing? I'm more than happy to accept contributing patches
 >> too :)
 >>
 >> Thanks,
 >> Pedro
 >>
 >> On Sun, Jul 21, 2013 at 3:09 AM, Shachaf BenKiki <shachaf at gmail.com>
 >> wrote:
 >>
 >>> On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães
 >>> <jpm at cs.uu.nl> wrote:
 >>>> Hi,
 >>>>
 >>>> On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg
 >>> <eir at cis.upenn.edu> wrote:
 >>>>>
 >>>>> Unless I'm missing something, this all looks very
 >>> straightforward. The
 >>>>> implementation is there, already, in the guise of (gcast Refl).
 >>> We would
 >>>>> just shuffle the definitions around a bit. Am I indeed missing
 >>> something?
 >>>>
 >>>>
 >>>> I think that is the case indeed. Though I agree that it would be
 >>> a nice
 >>>> addition to Data.Typeable.
 >>>>
 >>>>
 >>>
 >>> This thread is a few months old now, but it looks like people were
 >>> generally in favor of adding (gcast Refl) to Data.Typeable. I've
 >>> used
 >>> it in real code in at least one place since then (where I just
 >>> defined
 >>> it locally). It doesn't look like it's actually been added, though
 >>> 
 >>> is it planned to go into HEAD eventually?
 >>>
 >>> Shachaf
 >>
 >>
 >>
 >> Links:
 >> 
 >> [1] https://github.com/ghc/packagesbase/tree/dataproxy
 >
 > _______________________________________________
 > Libraries mailing list
 > Libraries at haskell.org
 > http://www.haskell.org/mailman/listinfo/libraries
More information about the Libraries
mailing list