[Haskell-cafe] TypeApplications and Proxy

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Mon Sep 14 15:50:31 UTC 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.

More information about the Haskell-Cafe mailing list