Haskellでの自己申告機能の作成方法を教えてください。

Question

次のコードを試しましたが、タイプエラーが発生しました。

sa f = f f 

• Occurs check: cannot construct the infinite type: t ~ t -> t1 
• In the first argument of ‘f’, namely ‘f’ 
    In the expression: f f 
    In an equation for ‘sa’: sa f = f f 
• Relevant bindings include 
    f :: t -> t1 
     (bound at fp-through-lambda-calculus-michaelson.hs:9:4) 
    sa :: (t -> t1) -> t1 
     (bound at fp-through-lambda-calculus-michaelson.hs:9:1) 

Answer 1

私は、Haskellのすべての用語で機能する単一の自己申請機能はないと思います。自己申請は、型付きラムダ計算において独特のものであり、しばしば型定義を回避する。これは、自己申告では、論理システムと見なされるときに型システムに矛盾を導入する固定小数点結合子を表すことができるという事実に関連している（Curry-Howard対応参照）。

id機能に適用するように尋ねました。自己申告id idでは、2つのidは異なるタイプを持っています。明示的には(id :: (A -> A) -> (A -> A)) (id :: A -> A)（任意のタイプはA）です。うまく動作しますが、むしろ、そのタイプによって制限され

sa :: (forall a. a -> a) -> b -> b 
sa f = f f 

ghci> :t sa id 
sa id :: b -> b 

：我々は、具体的id機能のために設計された自己のアプリケーションを作ることができます。あなたは、このような自己アプリケーション機能の家庭を作ることができますが、あなたは（sa tがt t場合に限っよく型付けされるような一般的な自己アプリケーション機能がよく型付けされていることを確認できるようにするつもりはないRankNTypesを使用して

GHCの核計算が基づいているシステムFω（「F-omega」）には少なくとも含まれていません。

の理由は、あなたが正式に（おそらく）それを作業する場合、我々は何の正規形を持っていないsa saを、得ることができるということである、と（私たちはもちろんのfixを追加するまで）Fωを正規化することが知られています。

Answer 2

無限の種類を構築するためのnewtypeを使用します。 GHCで

newtype Eventually a = NotYet (Eventually a -> a) 

sa :: Eventually a -> a 
sa eventually@(NotYet f) = f eventually 

、eventuallyとfは、メモリ内の同じオブジェクトになります。

Answer 3

これは、型指定されていないラムダ計算が何らかの形で、さらにがHaskellより強力なためです。あるいは、別の言い方をすると、型なしラムダ計算には型システムがありません。したがって、サウンドタイプのシステムはありません。ハスケルはそれを持っているのに対し、

これは、自己申告で表示されるだけでなく、無限の種類が関係するすべてのケースで表示されます。例えば、これを試してみてください：型システムは、一見無害expresion s i iが音型システムで許されるべきではないということを知りどのようにそれは驚くべきことである

i x = x 
s f g x = f x (g x) 
s i i 

。 がの場合、自己申告が可能です。