F * - new language with dependent types for .Net

Introduction

F * is a new language with dependent types, developed in the depths of Microsoft Research to build evidence of program properties. F * compiles to .Net bytecode and seamlessly integrates 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 of F * in the Coq system is available to everyone.


So, the main features of the new language:

• Self-certification: the F * type check checker was verified using F *. Read more about it here .
• Currently, de facto javascript has become the main language for building frontend of web applications. Many modern languages ​​can compile to Javascript. Microsoft Research engineers created a compiler that has compiled a fairly large subset of F * into Javascript. This means that a programmer can deploy his program on F * on web pages and get a guarantee that his code works provably correctly. Details can be read here .
• There is a monadic F * dialect in which a new verification methodology has been implemented using the Dijkstra monad.

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



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

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

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

Galloping across europe

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

 HelloWorld module
 let _ = print "Hello world!"

The constructor of the form let _ = e at the end of the module sets its main function.

Types in F * are used to describe program properties. For example, the expression 0 can match the type int. The Prims module (analogous to 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, F * programming is very similar to Coq - a programmer can give an inductive type definition and define functions on 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, explicit parallels are traced with Coq and its Notations for the introduction of syntactic sugar.

As well as types describe properties of expressions, F * uses sorts to describe properties of types. In most programming languages, varieties are implicitly defined. As a rule, there is only one type of type - * (pronounced "star"). Basic data types, such as int or string, are of the * grade. In F *, sorts of types are more obvious - you need to have more than one base variety. Therefore, the Prim module determines whether the base types belong to the S grade.

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

If a grade is not specified explicitly and it cannot be inferred by the type taker in the context of use, this type automatically receives grade S.

More explicitly, the list type can be set like this:

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

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

Preliminary result

So, F * programming should not cause difficulties for programmers who are familiar with ML family languages. The remaining interested readers can familiarize themselves with examples on the official website of the project or wait for the following posts.