F*

**F***是一个由微软研究院开发的基于F♯的依赖类型函数式程序语言。它可被编译到.NET的CIL或JavaScript。

简介**F***是一个由微软研究院开发的基于F♯的依赖类型函数式程序语言。它可被编译到.NET的CIL或JavaScript。

F*的类型系统较之于F#更加丰富，它允许可被半自动化检查的功能正确性规范。1

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。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*。1

通用中间语言通用中间语言（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语言的老用户。2

JavaScriptJavaScript，一种高级编程语言，通过解释执行，是一门动态类型，面向对象（基于原型）的解释型语言。它已经由ECMA（欧洲计算机制造商协会）通过ECMAScript实现语言的标准化。它被世界上的绝大多数网站所使用，也被世界主流浏览器（Chrome、IE、Firefox、Safari、Opera）支持。JavaScript是一门基于原型、函数先行的语言，是一门多范式的语言，它支持面向对象编程，命令式编程，以及函数式编程。它提供语法来操控文本、数组、日期以及正则表达式等，不支持I/O，比如网络、存储和图形等，但这些都可以由它的宿主环境提供支持。

虽然JavaScript与Java这门语言不管是在名字上，或是在语法上都有很多相似性，但这两门编程语言从设计之初就有很大的不同，JavaScript的语言设计主要受到了Self（一种基于原型的编程语言）和Scheme（一门函数式编程语言）的影响。在语法结构上它又与C语言有很多相似（例如if条件语句、while循环、switch语句、do-while循环等）。

在客户端，JavaScript在传统意义上被实现为一种解释语言，但在最近，它已经可以被即时编译（JIT）执行。随着最新的HTML5和CSS3语言标准的推行它还可用于游戏、桌面和移动应用程序的开发和在服务器端网络环境运行，如Node.js。3

本词条内容贡献者为:

王慧维 - 副研究员 - 西南大学