この署名付きの関数を書く方法はありますか？

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が(a -> b)に渡される情報はありません。あなたのいずれかがa秒の宇宙を列挙したり、それをfを実装することはほとんど自明となった場合には

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

のようなものを提供a引数を検査することができることができるようにする必要があります。

一般的に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 

したがって、タイプ((r -> b) -> r) -> rが生息している

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

したがってh = const

(\g -> runCont $ f (\x _ -> g x) (cont . const) (return())) 
    :: ((r -> b) -> a) -> (a -> 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 

が住んでいるが、私は、これはあなたが本当に欲しいものではありません疑います。