F * is a new language with dependent types for .Net

Introduction

F * is a new language with dependent types developed in the bowels of Microsoft Research to build evidence of program properties. F * compiles into .Net bytecode and integrates transparently with other languages, including F #, on the basis of which it is built. You can try F * in the browser or download the alpha version of the compiler and related examples here. Formalization F * in the Coq system is available to everyone.


So, the main features of the new language:

• Self-certification: F * tymphekher verified using F *. You can read more about this here .
• Currently, javascript has become the de facto main language for building front-end web applications. Many modern languages ​​can compile in Javascript. Microsoft Research engineers created a compiler that compiles a fairly large subset of F * in Javascript. This means that the programmer can deploy his program in F * on web pages and get a guarantee that his code works provably correctly. Details can be read here .
• There is a dialect “monadic F *” , which implements a new verification methodology using the monk Dijkstra.

Those readers who do not know what the dependent types are and why they are needed, I refer to the corresponding Wikipedia article . Type theory in programming languages ​​is a fairly extensive area of ​​knowledge, a review of which will take more than one hundred pages. The brief point is: Henk Barendregt proposed a visual model for describing eight different Church-typed lambda calculus systems. The so-called lambda cube is a three-dimensional cube, at the vertices of which there are various typing systems, and directed edges indicate the direction of inclusion.



Thus, a more primitive typing system is a special case of a more advanced one. At the base vertex is the usual typed lambda calculus, the terms of which depend on terms, and types do not participate in dependencies. You can get acquainted with the lambda calculus in more detail by reading Barendregt's monograph “Lambda calculus, its syntax and semantics”.

Different functional programming languages ​​support different type systems represented in a lambda cube. Λpѡ is the most advanced typing system supported by Coq and Agda.

But back to our sheep and try to give a brief description of the language F *.

Gallop across Europe

Programs on F * consist of modules. Each module is declared using the module keyword, which specifies the name of the module. Example:

module HelloWorld
let _ = print "Hello world!"

A constructor of the form let _ = e at the end of the module defines its main function.

Types in F * are used to describe program properties. For example, an expression of type 0 can match an int. The Prims module (an analogue of the Haskell Prelude) defines several basic types, such as unit, int, string, etc. The following example shows several ways to specify the type of expression:

let u = (() <: unit)
let z = (0 <: int)
let z ': int = 1 - 1 
let z '' = (1 - 1 <: int)
let hello: string = "hello"

The Prims module defines some useful data types, such as polymorphic lists:

type list 'a =
  | Nil: list 'a
  | Cons: 'a -> list' a -> list 'a

In general, programming in F * is much like Coq - a programmer can give an inductive definition of a type and define functions over these types. Let's try to write something useful:

let empty_list = Nil
let empty_list_sugar = []
let cons = Cons 1 Nil
let cons_sugar = 1 :: []
let list_3 = Cons 0 (Cons 1 (Cons 2 Nil))
let list_3_sugar = [0; 1; 2]
let rec length = function 
  | [] -> 0
  | _ :: tl -> 1 + (length tl)
let rec nth n = function 
  | [] -> fail "Not enough elements"
  | hd :: tl -> if n = 0 then hd else nth (n - 1) tl

Again, there are clear parallels with Coq and its Notations for introducing syntactic sugar.

Just as types describe the properties of expressions, F * uses sorts to describe the properties of types. In most programming languages, sorts are implicitly specified. Typically, there is only one kind of type - * (pronounced "star"). Basic data types, such as int or string, are sort *. In F *, type varieties are more obvious - you must have more than one base variety. Therefore, the Prim module determines the belonging of the basic types to the variety S.

type unit: S
type int: S
type string: S

If the sort is not specified explicitly and cannot be displayed by the tipper in the context of use, this type will automatically receive the variety S.

More explicitly, the list type can be specified as follows:

type list: S => S =
   | Nil: 'a: S -> list' a
   | Cons: 'a: S ->' a -> list 'a -> list' a

Here we define a new list type with two constructors. The Nil constructor takes a single argument - type 'a of type S.

Preliminary result

So, programming in F * should not cause difficulties for programmers familiar with the languages ​​of the ML family. Other interested readers can familiarize themselves with examples on the official website of the project or wait for the next posts.