基本介紹
- 中文名：F*
- 外文名：F*
- 領域：計算機編程
簡介,F#,依賴類型,通用中間語言,JavaScript,
簡介
F*的類型系統較之於F#更加豐富，它允許可被半自動化檢查的功能正確性規範。
F#
F#是由微軟發展的為.NET語言提供運行環境的程式設計語言，是函式程式語言（FP，Functional Programming），函式程式語言最重要的基礎是Lambda Calculus。它是基於OCaml的，而OCaml是基於ML函式程式語言。有時F#和OCaml的程式是可以互動編譯的。
F#已經接近成熟，支持高階函式、柯里化、惰性求值、Continuations、模式匹配、閉包、列表處理和元編程。這是一個用於顯示.NET在不同程式語言間互通的程式設計，可以被.NET中的任意其它代碼編譯和調用。
2002年微軟開始由Don Syme帶領研發F#，從C#，LINQ和Haskell中獲取了經驗，2005年推出第一個版本，2007年7月31日釋出1.9.2.9版。2007年底，微軟宣布F#進入產品化的階段。
F#已被集成在Visual Studio2010中，版本是2.0，含有對.Net Framework的完全支持。
F#現在在Visual Studio2015中，版本是4.0。
F#現在在Visual Studio2017中，版本是4.1。
依賴類型
在計算機科學和邏輯中，依賴類型（或依存類型，dependent type）是指依賴於值的類型，其理論同時包含了數學基礎中的類型論和計算機編程中用以減少程式錯誤的類型系統兩方面。在Per Martin-Löf的直覺類型論中，依賴類型可對應於謂詞邏輯中的全稱量詞和存在量詞；在依賴類型函式式程式語言如ATS、Agda、Dependent ML、Epigram、F*和Idris中，依賴類型系統通過極其豐富的類型表達能力使得程式規範得以藉助類型的形式被檢查，從而有效減少程式錯誤。
依賴類型的兩個常見實例是依賴函式類型（又稱依賴乘積類型、Π-類型）和依賴值對類型（又稱依賴總和類型、Σ-類型）。一個依賴類型函式的返回值類型可以依賴於某個參數的具體值，而非僅僅參數的類型，例如，一個輸入參數為整型值n的函式可能返回一個長度為n的數組；一個依賴類型值對中的第二個值可以依賴於第一個值，例如，依賴類型可表示這樣的類型：它由一對整數組成，其中的第二個數總是大於第一個數。
依賴類型增加了類型系統的複雜度。由於確定兩個依賴於值的類型的等價性需要涉及具體的計算，若允許在依賴類型中使用任意值的話，其類型檢查將會成為不可判定問題；換言之，無法確保程式的類型檢查一定會停機。
由於Curry-Howard同構揭示了程式語言的類型論與證明論的直覺邏輯之間的緊密關聯性，以依賴類型系統為基礎的程式語言大多同時也作為構造證明與可驗證程式的輔助工具而存在，如 Coq 和 Agda（但並非所有證明輔助工具都以類型論為基礎）；近年來，一些以通用和系統編程為目的的程式語言被設計出來，如 Idris。
一些以證明輔助為主要目的的程式語言採用強函式式編程（total functional programming），這消除了停機問題，同時也意味著通過它們自身的核心語言無法實現任意無限遞歸，不是圖靈完全的，如 Coq 和 Agda；另外一些依賴類型程式語言則是圖靈完全的，如 Idris、由ML派生而來的 ATS 和 由F#派生而來的 F*。
通用中間語言
通用中間語言（Common Intermediate Language，簡稱CIL，發音為"sill"或"kill"）是一種屬於通用語言架構和.NET框架的低階（lowest-level）的人類可讀的程式語言。目標為.NET框架的語言被編譯成CIL，然後彙編成位元組碼。CIL類似一個面向對象的組合語言，並且它是完全基於堆疊的。它運行在虛擬機上，其主要的語言有C#、Visual Basic .NET(VB.NET)、C++/CLI以及J#。
在.NET語言的測試版中，CIL原本叫做微軟中間語言，即Microsoft Intermediate Language，簡稱MSIL。由於C#和通用語言架構的標準化，在.Net開發平台下，所有語言（C#、VB.NET、J#、C++/CLI）都會被編譯為MSIL，再由CLR負責運行，位元組碼現在已經官方地成為了CIL。因此MSIL有時仍會與CIL混用，特別是那些.NET語言的老用戶。
JavaScript
JavaScript，一種高級程式語言，通過解釋執行，是一門動態類型，面向對象（基於原型）的解釋型語言。它已經由ECMA（歐洲計算機製造商協會）通過ECMAScript實現語言的標準化。它被世界上的絕大多數網站所使用，也被世界主流瀏覽器（Chrome、IE、Firefox、Safari、Opera）支持。JavaScript是一門基於原型、函式先行的語言，是一門多範式的語言，它支持面向對象編程，命令式編程，以及函式式編程。它提供語法來操控文本、數組、日期以及正則表達式等，不支持I/O，比如網路、存儲和圖形等，但這些都可以由它的宿主環境提供支持。
