Should coercion binders (arguments or binders in patterns) be TyVars?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Should coercion binders (arguments or binders in patterns) be TyVars?

Ömer Sinan Ağacan
Hi,

I just realized that coercion binders are currently Ids and not TyVars (unlike
other type arguments). This means that we don't drop coercion binders in
CoreToStg. Example:

    {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
       TypeApplications, MagicHash #-}

    module UnsafeCoerce where

    import Data.Type.Equality ((:~:)(..))
    import GHC.Prim
    import GHC.Types

    unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
    unsafeEqualityProof = error "unsafeEqualityProof evaluated"

    unsafeCoerce :: forall a b . a -> b
    unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x

If I build this with -ddump-stg this is what I get for `unsafeCoerce`:

    UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
    [GblId, Arity=1, Unf=OtherCon []] =
        [] \r [x_s2jn]
            case UnsafeCoerce.unsafeEqualityProof of {
              Data.Type.Equality.Refl co_a2fd -> x_s2jn;
            };

See the binder in `Refl` pattern.

Unarise drops this binder because it's a "void" argument (doesn't have a runtime
representation), but still it's a bit weird that we drop types but not coercions
in CoreToStg.

Is this intentional?

Ömer
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Should coercion binders (arguments or binders in patterns) be TyVars?

Sebastian Graf
Hi Ömer,

I'm not sure if there's a case in GHC (yet, because newtype coercions are zero-cost), but coercions in general (as introduced for example in Types and Programming Languages) can carry computational content and thus can't be erased.

Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a floating point register) at run-time, so you can't erase it. The fact that we can for newtypes is because `coerce` is basically just the `id` function at runtime.

Cheers,
Sebastian

Am So., 6. Okt. 2019 um 10:28 Uhr schrieb Ömer Sinan Ağacan <[hidden email]>:
Hi,

I just realized that coercion binders are currently Ids and not TyVars (unlike
other type arguments). This means that we don't drop coercion binders in
CoreToStg. Example:

    {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
       TypeApplications, MagicHash #-}

    module UnsafeCoerce where

    import Data.Type.Equality ((:~:)(..))
    import GHC.Prim
    import GHC.Types

    unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
    unsafeEqualityProof = error "unsafeEqualityProof evaluated"

    unsafeCoerce :: forall a b . a -> b
    unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x

If I build this with -ddump-stg this is what I get for `unsafeCoerce`:

    UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
    [GblId, Arity=1, Unf=OtherCon []] =
        [] \r [x_s2jn]
            case UnsafeCoerce.unsafeEqualityProof of {
              Data.Type.Equality.Refl co_a2fd -> x_s2jn;
            };

See the binder in `Refl` pattern.

Unarise drops this binder because it's a "void" argument (doesn't have a runtime
representation), but still it's a bit weird that we drop types but not coercions
in CoreToStg.

Is this intentional?

Ömer
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Should coercion binders (arguments or binders in patterns) be TyVars?

Ömer Sinan Ağacan
> I'm not sure if there's a case in GHC (yet, because newtype coercions are
> zero-cost), but coercions in general (as introduced for example in Types and
> Programming Languages) can carry computational content and thus can't be
> erased.

But they're already erased! They don't have a runtime representation and the
unarise pass eliminates coercion values and binders. See the last paragraph in
my original email.

> Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion
> as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a
> floating point register) at run-time, so you can't erase it. The fact that we
> can for newtypes is because `coerce` is basically just the `id` function at
> runtime.

Do we even support such coercions? I think a `co :: Int ~ Double` can only be an
unsafe coercion, which are basically no-op in runtime, so again they can be
erased.

Let me know if I'm mistaken.

Ömer

Sebastian Graf <[hidden email]>, 6 Eki 2019 Paz, 12:50 tarihinde
şunu yazdı:

>
> Hi Ömer,
>
> I'm not sure if there's a case in GHC (yet, because newtype coercions are zero-cost), but coercions in general (as introduced for example in Types and Programming Languages) can carry computational content and thus can't be erased.
>
> Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a floating point register) at run-time, so you can't erase it. The fact that we can for newtypes is because `coerce` is basically just the `id` function at runtime.
>
> Cheers,
> Sebastian
>
> Am So., 6. Okt. 2019 um 10:28 Uhr schrieb Ömer Sinan Ağacan <[hidden email]>:
>>
>> Hi,
>>
>> I just realized that coercion binders are currently Ids and not TyVars (unlike
>> other type arguments). This means that we don't drop coercion binders in
>> CoreToStg. Example:
>>
>>     {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
>>        TypeApplications, MagicHash #-}
>>
>>     module UnsafeCoerce where
>>
>>     import Data.Type.Equality ((:~:)(..))
>>     import GHC.Prim
>>     import GHC.Types
>>
>>     unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
>>     unsafeEqualityProof = error "unsafeEqualityProof evaluated"
>>
>>     unsafeCoerce :: forall a b . a -> b
>>     unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x
>>
>> If I build this with -ddump-stg this is what I get for `unsafeCoerce`:
>>
>>     UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
>>     [GblId, Arity=1, Unf=OtherCon []] =
>>         [] \r [x_s2jn]
>>             case UnsafeCoerce.unsafeEqualityProof of {
>>               Data.Type.Equality.Refl co_a2fd -> x_s2jn;
>>             };
>>
>> See the binder in `Refl` pattern.
>>
>> Unarise drops this binder because it's a "void" argument (doesn't have a runtime
>> representation), but still it's a bit weird that we drop types but not coercions
>> in CoreToStg.
>>
>> Is this intentional?
>>
>> Ömer
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Should coercion binders (arguments or binders in patterns) be TyVars?

Ömer Sinan Ağacan
> > Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion
> > as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a
> > floating point register) at run-time, so you can't erase it. The fact that we
> > can for newtypes is because `coerce` is basically just the `id` function at
> > runtime.
>
> Do we even support such coercions? I think a `co :: Int ~ Double` can only be an
> unsafe coercion, which are basically no-op in runtime, so again they can be
> erased.

To elaborate, for coercions that have a meaning in runtime I think we use
primops, type coercions are not used for this purpose. E.g. for Int to Double
coercion, if you really mean boxed Ints and Doubles then you can simply treat
Int as Double in runtime (and enjoy the segfaults or worse), if you mean Int# to
Double# then you use a primop like int2Double# which does `fild` if necessary.

Ömer

Ömer Sinan Ağacan <[hidden email]>, 6 Eki 2019 Paz, 12:55
tarihinde şunu yazdı:

>
> > I'm not sure if there's a case in GHC (yet, because newtype coercions are
> > zero-cost), but coercions in general (as introduced for example in Types and
> > Programming Languages) can carry computational content and thus can't be
> > erased.
>
> But they're already erased! They don't have a runtime representation and the
> unarise pass eliminates coercion values and binders. See the last paragraph in
> my original email.
>
> > Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion
> > as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a
> > floating point register) at run-time, so you can't erase it. The fact that we
> > can for newtypes is because `coerce` is basically just the `id` function at
> > runtime.
>
> Do we even support such coercions? I think a `co :: Int ~ Double` can only be an
> unsafe coercion, which are basically no-op in runtime, so again they can be
> erased.
>
> Let me know if I'm mistaken.
>
> Ömer
>
> Sebastian Graf <[hidden email]>, 6 Eki 2019 Paz, 12:50 tarihinde
> şunu yazdı:
> >
> > Hi Ömer,
> >
> > I'm not sure if there's a case in GHC (yet, because newtype coercions are zero-cost), but coercions in general (as introduced for example in Types and Programming Languages) can carry computational content and thus can't be erased.
> >
> > Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a floating point register) at run-time, so you can't erase it. The fact that we can for newtypes is because `coerce` is basically just the `id` function at runtime.
> >
> > Cheers,
> > Sebastian
> >
> > Am So., 6. Okt. 2019 um 10:28 Uhr schrieb Ömer Sinan Ağacan <[hidden email]>:
> >>
> >> Hi,
> >>
> >> I just realized that coercion binders are currently Ids and not TyVars (unlike
> >> other type arguments). This means that we don't drop coercion binders in
> >> CoreToStg. Example:
> >>
> >>     {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
> >>        TypeApplications, MagicHash #-}
> >>
> >>     module UnsafeCoerce where
> >>
> >>     import Data.Type.Equality ((:~:)(..))
> >>     import GHC.Prim
> >>     import GHC.Types
> >>
> >>     unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
> >>     unsafeEqualityProof = error "unsafeEqualityProof evaluated"
> >>
> >>     unsafeCoerce :: forall a b . a -> b
> >>     unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x
> >>
> >> If I build this with -ddump-stg this is what I get for `unsafeCoerce`:
> >>
> >>     UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
> >>     [GblId, Arity=1, Unf=OtherCon []] =
> >>         [] \r [x_s2jn]
> >>             case UnsafeCoerce.unsafeEqualityProof of {
> >>               Data.Type.Equality.Refl co_a2fd -> x_s2jn;
> >>             };
> >>
> >> See the binder in `Refl` pattern.
> >>
> >> Unarise drops this binder because it's a "void" argument (doesn't have a runtime
> >> representation), but still it's a bit weird that we drop types but not coercions
> >> in CoreToStg.
> >>
> >> Is this intentional?
> >>
> >> Ömer
> >> _______________________________________________
> >> ghc-devs mailing list
> >> [hidden email]
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Should coercion binders (arguments or binders in patterns) be TyVars?

GHC - devs mailing list
In reply to this post by Ömer Sinan Ağacan
| Is this intentional?

Yes, it's absolutely intentional.

Consider this Core defn
   f :: forall a b. (a ~# b) -> Int
   f = /\a b. \(g :: a ~# b). error "urk"

Now is `seq f True` equal to True, or to (error "urk").  Definitely the former.

So we cannot and must not discard coercion lambda.  However, a coercion is represented by a zero-bit value, and takes no space.  

Simon

| -----Original Message-----
| From: ghc-devs <[hidden email]> On Behalf Of Ömer Sinan
| Agacan
| Sent: 06 October 2019 10:28
| To: ghc-devs <[hidden email]>
| Subject: Should coercion binders (arguments or binders in patterns) be
| TyVars?
|
| Hi,
|
| I just realized that coercion binders are currently Ids and not TyVars
| (unlike other type arguments). This means that we don't drop coercion
| binders in CoreToStg. Example:
|
|     {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
|        TypeApplications, MagicHash #-}
|
|     module UnsafeCoerce where
|
|     import Data.Type.Equality ((:~:)(..))
|     import GHC.Prim
|     import GHC.Types
|
|     unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
|     unsafeEqualityProof = error "unsafeEqualityProof evaluated"
|
|     unsafeCoerce :: forall a b . a -> b
|     unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x
|
| If I build this with -ddump-stg this is what I get for `unsafeCoerce`:
|
|     UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
|     [GblId, Arity=1, Unf=OtherCon []] =
|         [] \r [x_s2jn]
|             case UnsafeCoerce.unsafeEqualityProof of {
|               Data.Type.Equality.Refl co_a2fd -> x_s2jn;
|             };
|
| See the binder in `Refl` pattern.
|
| Unarise drops this binder because it's a "void" argument (doesn't have a
| runtime representation), but still it's a bit weird that we drop types
| but not coercions in CoreToStg.
|
| Is this intentional?
|
| Ömer
| _______________________________________________
| ghc-devs mailing list
| [hidden email]
| https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.has
| kell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
| devs&amp;data=02%7C01%7Csimonpj%40microsoft.com%7Cf7f3feaf26b4452c1e8e08d
| 74a3f92f6%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637059509215789548
| &amp;sdata=T9iolaftOD1ncWw1JICW1UJU1X8pyCivNyB7enTS4X8%3D&amp;reserved=0
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Should coercion binders (arguments or binders in patterns) be TyVars?

Richard Eisenberg-5
And just to close the loop: the more general coercions that Sebastian has talked about would have computational content, but these are well beyond what GHC supports at the moment (and there are no plans to move in that direction).

Richard

> On Oct 6, 2019, at 10:38 PM, Simon Peyton Jones via ghc-devs <[hidden email]> wrote:
>
> | Is this intentional?
>
> Yes, it's absolutely intentional.
>
> Consider this Core defn
>   f :: forall a b. (a ~# b) -> Int
>   f = /\a b. \(g :: a ~# b). error "urk"
>
> Now is `seq f True` equal to True, or to (error "urk").  Definitely the former.
>
> So we cannot and must not discard coercion lambda.  However, a coercion is represented by a zero-bit value, and takes no space.  
>
> Simon
>
> | -----Original Message-----
> | From: ghc-devs <[hidden email]> On Behalf Of Ömer Sinan
> | Agacan
> | Sent: 06 October 2019 10:28
> | To: ghc-devs <[hidden email]>
> | Subject: Should coercion binders (arguments or binders in patterns) be
> | TyVars?
> |
> | Hi,
> |
> | I just realized that coercion binders are currently Ids and not TyVars
> | (unlike other type arguments). This means that we don't drop coercion
> | binders in CoreToStg. Example:
> |
> |     {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
> |        TypeApplications, MagicHash #-}
> |
> |     module UnsafeCoerce where
> |
> |     import Data.Type.Equality ((:~:)(..))
> |     import GHC.Prim
> |     import GHC.Types
> |
> |     unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b
> |     unsafeEqualityProof = error "unsafeEqualityProof evaluated"
> |
> |     unsafeCoerce :: forall a b . a -> b
> |     unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x
> |
> | If I build this with -ddump-stg this is what I get for `unsafeCoerce`:
> |
> |     UnsafeCoerce.unsafeCoerce :: forall a b. a -> b
> |     [GblId, Arity=1, Unf=OtherCon []] =
> |         [] \r [x_s2jn]
> |             case UnsafeCoerce.unsafeEqualityProof of {
> |               Data.Type.Equality.Refl co_a2fd -> x_s2jn;
> |             };
> |
> | See the binder in `Refl` pattern.
> |
> | Unarise drops this binder because it's a "void" argument (doesn't have a
> | runtime representation), but still it's a bit weird that we drop types
> | but not coercions in CoreToStg.
> |
> | Is this intentional?
> |
> | Ömer
> | _______________________________________________
> | ghc-devs mailing list
> | [hidden email]
> | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.has
> | kell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
> | devs&amp;data=02%7C01%7Csimonpj%40microsoft.com%7Cf7f3feaf26b4452c1e8e08d
> | 74a3f92f6%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637059509215789548
> | &amp;sdata=T9iolaftOD1ncWw1JICW1UJU1X8pyCivNyB7enTS4X8%3D&amp;reserved=0
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs