2017-11-18 73 views
4

我有一個函數正在執行某些特定數據類型的工作。我想知道我能不能把它變成一般人。下面是它的標誌性的通用版本:是用這個簽名寫一個函數的一種方法嗎?

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 
+2

你到目前爲止嘗試過什麼?你有什麼問題?您是否嘗試過在Hoogle上搜索這些功能? –

回答

2

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

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

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

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

4

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

該論點基本上與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) -> APeirce's law,已知這種邏輯中不可證明。

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


相比之下,類型

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

用術語

f2 = \ g h x -> x 

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

相關問題