如何编写带有签名“(Proxy a -> s) -> Proxy (Maybe a) -> Maybe s”的函数

Question

根据标题，我希望编写一个具有以下签名的函数。

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

对于我的用例来说，f是symbolVal. 我可以symbolVal在平原上运行KnownSymbol a => a，但我无法让它工作KnownSymbol a => Maybe a。

Answer 1

在同构之前，一种类型Proxy T等于()——实际上两种类型都只有一个可能的值。

另外，就同构而言，函数() -> T等于T——毕竟函数只能用一个值来调用。

然后可以简化（直到同构）您的类型，如下所示：

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

因此，你的问题相当于“我们如何实现s -> Maybe s，我们只有两种方法可以做到这一点：

f x = Just x
f x = Nothing

翻译回你的g我们得到两个解决方案

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

我认为这两个都不有趣，但没有其他（终止）选择。