TypeApplications and Proxy

14 Sep 2020

      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.

Johannes Waldmann