headers
Shachaf Ben-Kiki | 4 Mar 2013 08:43
Picon
Gravatar

new-typeable, new cast?

This came up in #haskell -- rather than just provide coerce, cast (or
a primitive that cast can be built on, as well as other things) can
give a type equality witness of some kind. Some possible signatures
are:

    cast :: (Typeable a, Typeable b) => Maybe (p a -> p b) --
Leibniz-style equality
    cast :: (Typeable a, Typeable b) => p a -> Maybe (p b) -- another form
    cast :: (Typeable a, Typeable b) => Maybe (Is a b) -- GADT-style equality
    cast :: (Typeable a, Typeable b) => MightBe a b -- another form
    -- With
    data Is a b where { Refl :: Is a a } -- standard equality GADT
    data MightBe a b where -- version with built-in Maybe, for more
convenient types
      Is :: MightBe a a
      Isn't :: MightBe a b

Any of these lets you write any of the other ones, of course. But
"cast" doesn't let you write any of them, because it only goes in one
direction.

The GADT form can let you write code like

    foo :: forall a. Typeable a => a -> ...
    foo x
      | Is <- cast :: MightBe a Int = ...x...
      | Is <- cast :: MightBe a Char = ...x...
      | otherwise = ...

Without coming up with a new name for x. It's possible to provide
(Continue reading)

Permalink | Reply |
headers
Shachaf Ben-Kiki | 4 Mar 2013 08:49
Picon
Gravatar

Re: new-typeable, new cast?

On Sun, Mar 3, 2013 at 11:43 PM, Shachaf Ben-Kiki <shachaf <at> gmail.com> wrote
> Any of these lets you write any of the other ones, of course. But
> "cast" doesn't let you write any of them, because it only goes in one
> direction.

Note: It turns out this isn't actually true, since Is can derive Typeable:

λ> data Is :: * -> * -> * where Refl :: Is a a deriving Typeable
λ> let cast' :: forall a b. (Typeable a, Typeable b) => Maybe (Is a
b); cast' = cast (Refl :: Is a a)

It probably still makes sense to provide an equality witness in a less
roundabout way, though.

    Shachaf

_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Permalink | Reply |
headers
Gábor Lehel | 4 Mar 2013 09:28
Picon

Re: new-typeable, new cast?

On Mon, Mar 4, 2013 at 8:43 AM, Shachaf Ben-Kiki <shachaf <at> gmail.com> wrote:
> This came up in #haskell -- rather than just provide coerce, cast (or
> a primitive that cast can be built on, as well as other things) can
> give a type equality witness of some kind. Some possible signatures
> are:
>
>     cast :: (Typeable a, Typeable b) => Maybe (p a -> p b) --
> Leibniz-style equality
>     cast :: (Typeable a, Typeable b) => p a -> Maybe (p b) -- another form
>     cast :: (Typeable a, Typeable b) => Maybe (Is a b) -- GADT-style equality
>     cast :: (Typeable a, Typeable b) => MightBe a b -- another form
>     -- With
>     data Is a b where { Refl :: Is a a } -- standard equality GADT
>     data MightBe a b where -- version with built-in Maybe, for more
> convenient types
>       Is :: MightBe a a
>       Isn't :: MightBe a b
>
> Any of these lets you write any of the other ones, of course. But
> "cast" doesn't let you write any of them, because it only goes in one
> direction.

gcast does, though

>
> The GADT form can let you write code like
>
>     foo :: forall a. Typeable a => a -> ...
>     foo x
>       | Is <- cast :: MightBe a Int = ...x...
(Continue reading)

Permalink | Reply |
headers
Simon Peyton-Jones | 4 Mar 2013 10:07
Picon
Favicon
Gravatar

RE: new-typeable, new cast?

Shachaf's idea (below) makes sense to me, though I'd present it slightly differently.

* Currently, cast :: (Typeable a, Typeable b) => a -> Maybe b
  provides a function to convert a value of type 'a' to 'b'.
  But it does not provide a way to convert a [a] to [b], or
  a->Int to b->Int.

* Of course these things can be done with 'map', but that's a pain,
  and the type involved might not be an instance of Functor

* So the Right Thing is provide a witness for a~b, wrapped as usual
  in a GADT. Then it will "lift" automatically to any type, such as
  those above.

* The type GHC.TypeLits.(:~:) is the current library version of a 
  GADT-wrapped equality
  So we need 
    newCast :: (Typeable a, Typeable b) => Maybe (a :~: b)

As usual this relies absolutely on the veracity of Typeable, but now we only derive it mechanically that
should be assured.

Iavor/Pedro, what do you think?

Simon



| -----Original Message-----
| From: libraries-bounces <at> haskell.org [mailto:libraries-
(Continue reading)

Permalink | Reply |
headers
Shachaf Ben-Kiki | 4 Mar 2013 11:17
Picon
Gravatar

Re: new-typeable, new cast?

On Mon, Mar 4, 2013 at 1:07 AM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> Shachaf's idea (below) makes sense to me, though I'd present it slightly differently.
>
> * Currently, cast :: (Typeable a, Typeable b) => a -> Maybe b
>   provides a function to convert a value of type 'a' to 'b'.
>   But it does not provide a way to convert a [a] to [b], or
>   a->Int to b->Int.
>
> * Of course these things can be done with 'map', but that's a pain,
>   and the type involved might not be an instance of Functor
>
> * So the Right Thing is provide a witness for a~b, wrapped as usual
>   in a GADT. Then it will "lift" automatically to any type, such as
>   those above.
>
> * The type GHC.TypeLits.(:~:) is the current library version of a
>   GADT-wrapped equality
>   So we need
>     newCast :: (Typeable a, Typeable b) => Maybe (a :~: b)
>
> As usual this relies absolutely on the veracity of Typeable, but now we only derive it mechanically that
should be assured.
>
> Iavor/Pedro, what do you think?
>
> Simon
>

I sent this message to the wrong address before:
(Continue reading)

Permalink | Reply |
headers
Simon Peyton-Jones | 4 Mar 2013 13:24
Picon
Favicon
Gravatar

RE: new-typeable, new cast?

|     λ> data a :~: b where Refl :: a :~: a
|     λ> :t gcast Refl
|     gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe ((:~:) *
| a b)

That is a ferociously-unintuitive use of 'gcast'!  It too me dome while to convince myself that it was right.  
Though it does indeed work.  I'd see (gcast Refl) as the primitive, with 'gcast' itself as a simple derived function.

I'm not sure what name to give the new cast function
	?? :: Typeable a, Typeable b) => Maybe (a :~: b)


Do we need gcast1 and gcast2 any more, in our new polykinded world?  Can they be depreceated?

Simon

| -----Original Message-----
| From: Shachaf Ben-Kiki [mailto:shachaf <at> gmail.com]
| Sent: 04 March 2013 10:18
| To: Simon Peyton-Jones
| Cc: libraries <at> haskell.org; Stephanie Weirich; Richard Eisenberg
| (eir <at> cis.upenn.edu); Dimitrios Vytiniotis; Iavor Diatchki; Conor
| McBride; Pedro Magalhães
| Subject: Re: new-typeable, new cast?
| 
| On Mon, Mar 4, 2013 at 1:07 AM, Simon Peyton-Jones
| <simonpj <at> microsoft.com> wrote:
| > Shachaf's idea (below) makes sense to me, though I'd present it
| slightly differently.
| >
(Continue reading)

Permalink | Reply |
headers
Shachaf Ben-Kiki | 4 Mar 2013 14:46
Picon
Gravatar

Re: new-typeable, new cast?

On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> |     λ> data a :~: b where Refl :: a :~: a
> |     λ> :t gcast Refl
> |     gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe ((:~:) *
> | a b)
>
> That is a ferociously-unintuitive use of 'gcast'!  It too me dome while to convince myself that it was
right.   Though it does indeed work.  I'd see (gcast Refl) as the primitive, with 'gcast' itself as a simple
derived function.
>
> I'm not sure what name to give the new cast function
>         ?? :: Typeable a, Typeable b) => Maybe (a :~: b)
>
>
> Do we need gcast1 and gcast2 any more, in our new polykinded world?  Can they be depreceated?
>
> Simon
>

A couple of people have suggested "same". (I wonder if this would also
subsume eqSingNat/eqSingSym?).

By the way -- since (:~:) seems to be in HEAD now, but not yet
released, is there a chance of renaming it? ":~:" is pretty awkward to
type, given all the new TypeOperators options these days; how about
"=="?

    Shachaf
(Continue reading)

Permalink | Reply |

Gmane