是用這個簽名寫一個函數的一種方法嗎？

Question

我有一個函數正在執行某些特定數據類型的工作。我想知道我能不能把它變成一般人。下面是它的標誌性的通用版本：

f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d 

如果以上不能寫，或許更受限制的版本可以？

f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b 

Answer 1

出現問題。知道c不會告訴你哪個a s會被傳遞給(a -> b)。你要麼需要能夠列舉的a S中的宇宙或能夠與一些檢查所提供的a參數，像

(forall f. Functor f => ((a -> f b) -> c -> f d) 

在這種情況下，變得幾乎微不足道的實施F。

一般而言，您應該嘗試概括您的功能，如((a -> b) -> c -> d)，以查看是否可以用鏡頭，遍歷或類似方法替換它們。

Answer 2

不，這是不可能的，至少沒有非終止或不安全的操作。

該論點基本上與this one類似：我們利用f來居住一種我們知道不能居住的類型。

假設存在

f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d 

專營c ~()

f :: Monad m => ((a -> b) ->() -> d) -> (a -> m b) -> m() -> m d 

因此

(\g h -> f (\x _ -> g x) h (return())) 
    :: Monad m => ((a -> b) -> d) -> (a -> m b) -> m d 

Speciazlize d ~ a。

(\g h -> f (\x _ -> g x) h (return())) 
    :: Monad m => ((a -> b) -> a) -> (a -> m b) -> m a 

Speclialize m ~ Cont t

(\g h -> runCont $ f (\x _ -> g x) (cont . h) (return())) 
    :: ((a1 -> b) -> a) -> (a1 -> (b -> r) -> r) -> (a -> r) -> r 

採取h = const

(\g -> runCont $ f (\x _ -> g x) (cont . const) (return())) 
    :: ((r -> b) -> a) -> (a -> r) -> r 

因此

(\g -> runCont (f (\x _ -> g x) (cont . const) (return())) id) 
    :: ((r -> b) -> r) -> r 

所以，類型((r -> b) -> r) -> r有人居住，H通過庫裏霍華德同構主義，它對應於命題直覺主義邏輯的一個定理。然而，公式((A -> B) -> A) -> A是Peirce's law，已知這種邏輯中不可證明。

我們得到一個矛盾，因此沒有這樣的f。

---

相比之下，類型

f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b 

用術語

f2 = \ g h x -> x 

居住，但我懷疑這是不是你真正想要的。