タイプシステムとトゥーリン完全

13796 ワード
タイプシステムとトゥーリン完全
シーケンス
タイプシステムはプログラミング言語において極めて重要であり、1つのタイプの寸法を提供したり、コンパイルを容易にしたりするだけでなく、エラーを減らす可能性が高い.タイプシステムがある程度強くなると、いわゆる「リッチタイププログラミング」が可能になります.例えば、Haskellではコンパイラが間違っていない限り、大体プログラムにバグはありません.通常の静的タイプ言語では、C++/java/C#など、新しい標準と新しいバージョンではタイプの自動導出がサポートされていますが、タイプシステムとその導出にはより直接的なサポートが欠けています.
多くの一般的な言語のタイプシステムは、C++、Scala、Haskell、Qi/shen(Lisp方言)のように、C++とScalaがなぜ図霊なのかを完全に理解しており、それらはタイプのパターンマッチングに依存しており、C++では対応特化と偏特化、Scalaはタイプの継承関係などを使用することができる.
非専門的な研究である以上,いくつかのタイプのシステムのTuring Completeを非専門的な手段で論証する.
リード
「プログラムはタイプの証明です」
この言葉がCurry-Howard同構造と結びついて明らかになったものは深い.次の表は、対応関係の一部です.
　logic side　
　program side
　Hilbert-style deduction system
　type system for combinatory logic　
　natural deduction
　type system for lambda calculus　
　hypotheses　
　free variables　
　deduction theorem　
　abstraction elimination　
　．．．　
　．．．　
　Peirce's law　
　cal/cc　
　double-negation translation　
　CPS translation　
注:表の最後から2行目のcall/cc(call with current continuation)((α → β) → α) → αに代表される排中律は、単純なタイプのlambda演算ではタイプが居留しないため、伝説のLisp 7大公理でcall/ccからの別の角度を作ることができない理由でもある.
タイプと推理システムは形式化言語に最も近い場所である.タイプシステムは異なる角度から多くの種類に分けられ,静的/動的,強/弱,サブタイプシステム,Duck Type,Dependent types,Union typesなどである.タイプ導出の観点からSystem F,HMタイプシステムなどがある.Curry Howard同構造の意味では,プログラム言語の言語構造は,System Fが表す2次直感論理など,推理システムの推理規則として同構造化されている.
有名なS結合子:S = λx. λy. λz. xz(yz)を例にとると、そのタイプは(α → β → γ) → (α → β) → α であり、その証明はwikiに移行することができる.
本文
図霊完全といえば、皆さんはきっとよく知られていません.私たちは毎日図霊完全な言語でいろいろなことをしています(すべての言語が図霊完全ではありません.例えばHTML、正則).タイプシステムの図霊完全は、Type CheckerとType Inferenceですべてのことを理論的にできると大雑把に考えることができます(書くのが醜いかどうかにかかわらず!).
Qi/Shen
Qi言語はShen言語の前身であり,Lispに属する方言であり,静的タイプシステムとProlog,Patten Match,カスタム評価ポリシーなどの複数の機能を内蔵したCLisp拡張と見なすことができる.そのタイプシステムの顕著な特徴はDependent Type Systemを採用していることであり,その文字通り一例を見てみよう.
(datatype t
 Name : String;
 Telephone : String;
 ====== 
[Name Telephone] : t;
 )

(注:このうち=====は文法糖で、
(datatype t
 Name : String; 
Telephone : String;
 ---------- 
[Name Telephone] : t; )

と
(datatype t
 Name : String,
 Telephone : String; >> P 
--------- 
[Name Telephone] : t >> P )

の合写.)
Sequent calculusに詳しいなら、上記の書き方はまるで数式に向かって描かれている~しかも上記のタイプ定義のcondition lineではif (element? X [0 1]という書き方もサポートされています.
Sequent calculusはトゥーリンが完全で、Qi/shenのType SystemはSequent calculusに基づいており、もちろんトゥーリンが完全である.
Haskell
Haskellのタイプシステムは有名なHindley–Milner type systemに属し、lambda演算とパラメータ多様性(parametric polymorphism)に基づく古典的なタイプシステムであり、もちろんHaskellの異なるバージョンは上に異なるタイプのシステム拡張がある.以下はこの文章の中で比較的に面白いところで、どのようにSK Combinatorを利用してHaskellタイプのシステムの図霊の完全性を論証します.
Qi/shen言語とは異なり,Haskellのタイプ導出規則は述語(Predicate)に対する演繹解に基づいており,以下の内容はHaskellのType Checkerを用いてSK Combinatorを作成する.対応しない実装の関数宣言を作成するために,undefinedと-fallow-undecidable-instancesのghcオプションを用いた.まず、基本的なSK CombinatorのtermとApplicationを定義します.
data K0 data S0 data App x y data Other a

次に、結果を集計する集計関数のclassとInstanceを宣言します.
 
data Done 
data More
class CombineDone d1 d2 d | d1 d2 -> d 
instance CombineDone Done Done Done 
instance CombineDone Done More More 
instance CombineDone More Done More 
instance CombineDone More More More


もちろん、termを帰約するために本当に使用される帰約関数も宣言しなければなりません.
class Eval1 x y d | x -> y d

次に、Instanceに契約のルールを書き込みます.

instance Eval1 S0        S0         Done 
instance Eval1 K0        K0         Done 
instance Eval1 (Other a) (Other a)  Done  
instance Eval1 x x' d => Eval1 (App K0 x) (App K0 x') d 
instance Eval1 x x' d => Eval1 (App S0 x) (App S0 x') d 
instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , CombineDone d1 d2 d
          ) => Eval1 (App (App S0 x) y) (App (App S0 x') y') d 
instance Eval1 x x' d => Eval1 (App (Other a) x) (App (Other a) x') d
 instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , CombineDone d1 d2 d
          ) => Eval1 (App (App (Other a) x ) y )
                     (App (App (Other a) x') y') d 
instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , Eval1 z z' d3
          , CombineDone d1 d2 d4
          , CombineDone d3 d4 d
          ) => Eval1 (App (App (App (Other a) x ) y ) z )
                     (App (App (App (Other a) x') y') z') d

次は本当のSとKの定義です:S Combinator:
instance Eval1 (App (App (App S0 f) g) x) (App (App f x) (App g x)) More

K Combinator :    λx. λy. λz. xz(yz) 
instance Eval1 (App (App K0 x) y) x More instance Eval1 (App (App (App K0 x) y) z) (App x z) More

これらの特化されたルールだけでは十分ではなく、上記rulesに帰約されないシナリオ処理も含まれています.
instance ( Eval1 (App (App (App p q) x) y) a d )
 => Eval1 (App (App (App (App p q) x) y) z) (App a z) d

補助タイプを追加
class EvalAux x y q1 | x q1 -> y
 instance EvalAux x x Done 
instance (     Eval1   x y q
          ,    EvalAux y z q
          ) => EvalAux x z More  
class Eval x y | x -> y 
instance EvalAux x y More => Eval x y

ここで,X->Y計算を直接表すタイプを得たが,タイプ宣言だけでは走れず,最後にdummy typesとundefinedを補佐したmethodを得た.
data P0 
data Q0 
data R0  
type P = Other P0 
type Q = Other Q0 
type R = Other R0  
eval1 :: Eval1 x y q => x -> y 
eval1 = undefined  
eval :: Eval x y => x -> y 
eval = undefined  
bot :: a bot = undefined

これにより、最も基本的な例を作ることができます.
type K x y   = App (App K0 x) y
type S f g x = App (App (App S0 f) g) x  
testK = eval (bot :: K P Q)   :: P 
testS = eval (bot :: S P Q R) :: App (App P R) (App Q R)

そうですか.高洋のSK Combinatorができて、それはタイプの導きの上ですでに正しい帰約ができて、それから、あなたは全体の世界を作ることができます.
延長
関数式のプログラミングとタイプシステムを研究するのはとても面白いことで、多くのよく使われる言語と違って、いつもいくつかの“王八のお尻--規定”があって、例えばPythonのわけのわからないScoping問題、jsのわけのわからない演算結果など.正真正銘に設計された関数言語の多くの特性は、その設計構想の延長であり、F-algebras、Fix Point、Free Monad、Foldable&Traversableなどは、プログラミング技術だけでなく、別の方向のProgram Pattarnを代表している.
HaskellとOcamlはいずれもHindley-Milnerシステムに基づいているが,タイプシステムにも様々なパッチが適用されており,プログラムの書き方に対するサポートの程度も様々である.
例えば、Haskellは再帰的な定義を処理することができず、例えば λx. λy. x、haskellはサポートされていない.匿名関数タイプ推定では単純なタイプのlambda演算に属し、\x -> x x演算子を追加的に導入しなければ処理できないからである.このように、よく知られているY Combinatorは、
newtype Mu a = Mu (Mu a -> a) 
y :: (a -> a) -> a 
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

(注:詳しくは私のもう一つのブログを参照してください)
Ocamlはこのシナリオにパッチを適用し,asの意味を加えてタイプがμと識別される.
このコードの場合:
data Sum a b = LeftSum a 
                       | RightSum b   
lengthxs list = case list of
                       LeftSum [] -> 0
                       RightSum (x:xs) -> 1 + lengthxs xs

Haskellはコンパイルできません.Ocamlは~
本人ブログアドレス(http://www.cppblog.com/pwq1989/)
以太坊solidity基礎4
static作用