ハスケル型に唯一の関数が存在することをどのように示しますか？

Question

this answerでは、idがforall a. a -> aの唯一の住人であることを示す方法を示しています。これを行うには、形式がYoneda lemmaを使用して()と同形であり、()に値が1つしかないことを示しているので、タイプはidでなければなりません。

米田は言う：まとめ、彼の証明は、このようなものですa =()とf = Identity場合

Functor f => (forall b . (a -> b) -> f b) ~ f a 

、これは次のようになります。

(forall b. (() -> b) -> b) ~() 

そして自明() -> b ~ b以来、LHSは基本的にタイプですidです。

これは、idでうまくいく「マジックトリック」のような感じです。私はより複雑な関数型のために同じことをしようとしています：

(b -> a) -> (a -> b -> c) -> b -> c 

しかし、どこから始めたらいいのか分かりません。 \f g x = g (f x) xが住んでいることを知っています。醜い⊥/undefinedのものを無視すると、このタイプの他の機能はありません。

私はガブリエルのトリックはすぐに私は種類を選ぶ方法を適用するとは思わない。このタイプと同型の同型性を示すことができる他のアプローチ（これは正式な形式です）は()ですか？

Answer 1

sequent calculusを適用できます。

ショートの例では、タイプa -> aで、我々は次のように用語を構築することができます：\x -> (\y -> y) xが、それはまだidある\x -> xに正規化します。後の計算では、システムは "還元可能な"プルーフを構築することを禁じます。

f: b -> a 
g: a -> b -> c 
x: b 
-------------- 
Goal: c 

して続行するには多くの方法がありません：

あなたのタイプは非公式に、(b -> a) -> (a -> b -> c) -> b -> cあるので、最終的には

apply g 

f: b -> a 
g: a -> b -> c 
x: b 
--------------- 
Subgoal0: a 
Subgoal1: b 


apply f 

f: b -> a 
g: a -> b -> c 
x: b 
--------------- 
Subgoal0': b 
Subgoal1: b 


-- For both 
apply x 

は、g (f x) xは、そのタイプの唯一の住人であると思われます。

---

米田の補題のアプローチ、実際forall xを持って注意する必要があります！最後に

(b -> a) -> (a -> b -> c) -> b -> c 
forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c 

レッツ濃縮物：

(a -> b -> c) -> c ~ ((a,b) -> c) -> c 

(a, b)と同型であるので、全体の形は取る

(b -> a) -> b -> (a, b) 

に減少しf = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b) 

そして、それはHP a = (a,a)ファンクタを取ることによって、ユニークです：

b -> (b,b) ~ (() -> b) -> HP b ~ HP() ~() 

---

EDIT最初のアプローチは、もう少し手波状を感じ、何とかもっと直接的に感じている：どのように証明、ルールの制限された集合が与えられます構築することができる校正証明書はいくつありますか？