Home > Net >  How do I write a function with the signature `(Proxy a -> s) -> Proxy (Maybe a) -> Maybe s`
How do I write a function with the signature `(Proxy a -> s) -> Proxy (Maybe a) -> Maybe s`

Time:07-20

As per the title, I'm looking to write a function with the following signature.

g :: (Proxy a -> s) -> Proxy (Maybe a) -> Maybe s
g f x = ...

For my use case, f is symbolVal. I can run symbolVal on a plain KnownSymbol a => a, but I can't get this to work on KnownSymbol a => Maybe a.

CodePudding user response:

Up to isomorphism, a type Proxy T is equal to () -- indeed both types only have one possible values.

Also, up to isomorphism, a function () -> T is equal to T -- after all the function can only be called with one value.

One can then simplify (up to isomorphism) your type as follows:

(Proxy a -> s) -> Proxy (Maybe a) -> Maybe s
~=
(() -> s) -> () -> Maybe s
~=
s -> Maybe s

Hence, your question is equivalent to "how can we implement s -> Maybe s and we only have two ways t do that:

f x = Just x
f x = Nothing

Translating back to your g we obtain the two solutions

g h _ = Just (h Proxy)
g h _ = Nothing

I don't think either of these is interesting, but there are no other (terminating) choices.

CodePudding user response:

I think this is an XY question: you're asking about a different problem from what you really should be solving.

See, proxies were always just a hack to make up for the fact that Haskell isn't really designed to pass around type information like you can pass around values. (By contrast, dependently typed languages are designed up-front for doing this.) But actually, for quite a while now Haskell has included a feature that allows explicitly passing types: -XTypeApplications. So at this point proxies are basically just a legacy alternative, but in your own code I would suggest not worrying about how you can manipulate proxies or proxy-functions. Instead you should just pass around the type information explicitly, and if you need to fulfill the Proxy whvr -> argument of some library function then simply give it Proxy @whvr right there and then.

If you don't understand how to do that, give a bit more example code of the use-case in which you really have this need.

  • Related