[Haskell-cafe] TypeApplications and Proxy
johannes.waldmann at htwk-leipzig.de
Mon Sep 14 15:50:31 UTC 2020
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.
More information about the Haskell-Cafe