TypeApplications and Proxy

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

TypeApplications and Proxy

Johannes Waldmann-2
Dear Cafe,

since GHC has TypeApplication, we don't need Proxy that much?


`natVal (Proxy :: Proxy w)`  can be written as  `natVal @w Proxy`
but then, the argument  `Proxy`  looks unnecessary. I can define

nat :: forall (n::Nat) . KnownNat n => Int
nat = fromIntegral $ natVal @n Proxy

and then use `nat @w`. (with -XAllowAmbiguousTypes.)
I just wonder if that's already in some library.


But then, what about the other direction (from value to type)?
Is there a shorter way to write, e.g.,

reifyNat (read e) $ \ (_ :: Proxy w) -> run @w ...

I see that Data.Reflection  suggests `reifyNat (read 3) run`
but then `run` needs the Proxy argument.


Thanks, J.W.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Henning Thielemann

On Mon, 14 Sep 2020, Johannes Waldmann wrote:

> since GHC has TypeApplication, we don't need Proxy that much?

Is it as reliable as Proxy? I remember TypeApplication depends on the
order in which type variables are introduced. I am afraid type
applications may easily break during refactoring. But I have no
experience.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Johannes Waldmann-2

> TypeApplication depends on the
> order in which type variables are introduced.

https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#ordering-of-specified-variables

The easy fix is to declare all type variables.
Then the first clause of 9.19.2 is enough?

- J.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Richard Eisenberg-5
I would say that TypeApplications is stable enough, and that the ordering of type variables is reliable enough.

But, sadly, we can't quite get rid of Proxy yet. Here's a very contrived example:

type family F a
hr :: (forall a. F a -> ()) -> ()
hr _ = ()

x = hr (\ _ -> ())

In the body of the lambda there, it is impossible to bind the type variable `a` with any Haskell construct. The workaround is to use Proxy in the type of hr. I don't know another way to do it.

So I'm all for removing other uses of Proxy, but I don't think we should quite drop it from base, yet.

Proposal #155 (https://github.com/ghc-proposals/ghc-proposals/pull/155) is in this area, but it's not yet implemented.

Richard

> On Sep 14, 2020, at 3:34 PM, Johannes Waldmann <[hidden email]> wrote:
>
>
>> TypeApplication depends on the
>> order in which type variables are introduced.
>
> https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#ordering-of-specified-variables
>
> The easy fix is to declare all type variables.
> Then the first clause of 9.19.2 is enough?
>
> - J.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Henning Thielemann
In reply to this post by Johannes Waldmann-2

On Mon, 14 Sep 2020, Johannes Waldmann wrote:

>> TypeApplication depends on the
>> order in which type variables are introduced.
>
> https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#ordering-of-specified-variables
>
> The easy fix is to declare all type variables.

It still means, that libraries have to maintain order of type variables in
order to avoid surprises in client code. Re-ordering introduction of type
variables becomes a breaking change - But only if the client code chooses
to use TypeApplication.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Compl Yue
In reply to this post by Johannes Waldmann-2

> I just wonder if that's already in some library.

I happen to be learning `named`, and read here:


data Name (name :: Symbol) = Name

instance name ~ name' => IsLabel name' (Name name) where
#if MIN_VERSION_base(4,10,0)
  fromLabel = Name
#else
  fromLabel _ = Name
#endif
  {-# INLINE fromLabel #-}

Does this mean [IsLabel](http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-OverloadedLabels.html#t:IsLabel) class has dropped Proxy since GHC 8.2?



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: TypeApplications and Proxy

Adam Gundry-2
On 15/09/2020 06:19, Compl Yue wrote:
>
> Does this mean
> [IsLabel](http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-OverloadedLabels.html#t:IsLabel)
> class has dropped Proxy since GHC 8.2?

Yes. The original implementation of IsLabel had a Proxy argument, but it
was removed as unnecessary in the presence of TypeApplications [1].

As others have observed, there are certainly uses for Proxy that remain,
notably to make it clear when a type variable needs to be supplied
explicitly by the caller, or to allow type variables to be bound in
patterns. Both of these may be alleviated by future GHC extensions, but
we're not there yet.

Adam

[1]
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0023-overloaded-record-fields.rst#changes-to-overloadedlabels-extension


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
118 Wymering Mansions, Wymering Road, London W9 2NF, England
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.