Pull to refresh

F* – новый язык с зависимыми типами для .Net

Reading time 3 min
Views 5.1K

Введение


F* – это новый язык с зависимыми типами, разработанный в недрах Microsoft Research для построения доказательств свойств программ. F* компилируется в байткод .Net и прозрачно интегрируется с другими языками, включая F#, на основе которого он и построен. Вы можете попробовать F* в браузере или скачать альфа-версию компилятора и сопутствующих примеров тут. Формализация F* в системе Coq доступна для всех желающих.


Итак, основные фичи нового языка:

  • Self-certification: тайпчекер F* верифицирован с использованием F*. Подробнее об этом можно почитать тут.
  • В настоящее время javascript де-факто стал основным языком для построения фронтэнда веб-приложений. Многие современные языки умеют компилироваться в Javascript. Инженеры Microsoft Research создали компилятор, который имеет компилировать достаточно большое подмножество F* в Javascript. Это означает, что программист может развернуть свою программу на F* на веб-страницах и получить гарантию того, что его код работает доказуемо правильно. Подробности можно почитать тут.
  • Существует диалект «monadic F*», в котором реализована новая методология верификации с помощью монады Дейкстры.


Тех читателей, кто не знает что такое зависимые типы и для чего они нужны, я отсылаю к соответствующей статье в википедии. Теория типов в языках программирования – это довольно обширная область знаний, обзор которой займет не одну сотню страниц. Краткая суть такова: Хенк Барендрегт предложил наглядную модель для описания восьми различных систем типизированного по Чёрчу лямбда-исчисления. Так называемый лямбда-куб представляет собой трехмерный куб, в вершинах которого находятся различные системы типизации, а направленные ребра указывают направление включения.

image

Таким образом, более примитивная система типизации является частным случаем более продвинутой. В базовой вершине располагается обычное типизированное лямбда-исчисление, термы которого зависят от термов, а типы в зависимостях не участвуют. Более подробно познакомиться с лямбда-исчислением можно прочитав монографию Барендрегта «Ламбда-исчисление его синтаксис и семантика».

Различные языки функционального программирования поддерживают различные системы типов, представленных в лямбда-кубе. Λpѡ – наиболее прокачанная система типизации, которую поддерживают языки Coq и Agda.

Но вернемся к нашим баранам и попробуем дать краткое описание языка F*.

Галопом по европам


Программы на F* состоят из модулей. Каждый модуль объявляется с использованием ключевого слова module, задающего имя модуля. Пример:

module HelloWorld
let _ = print "Hello world!"

Конструктор вида let _ = e в конце модуля задает его функцию main.

Типы в F* служат для описания свойств программы. Например, выражению 0 можно сопоставить тип int. Модуль Prims (аналог хаскелльной Prelude) определяет несколько базовых типов, таких как unit, int, string и т. п. В следующем примере показано несколько способов задания типа выражения:

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

В модуле Prims определены некоторые полезные типы данных, такие как полиморфные списки:

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

В целом программирование на F* во многом похоже на Coq – программист может дать индуктивное определение типа и задать функции над этими типами. Попробуем написать что-нибудь полезное:

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

Опять же прослеживаются явные параллели с Coq и его Notations для введения синтаксического сахара.

Также как типы описывают свойства выражений, F* использует сорты для описания свойств типов. В большинстве языков программирования сорты задаются неявно. Как правило есть только один сорт типов – * (произносится как «star»). Основные типы данных, такие как int или string, относятся к сорту *. В F* сорты типов более очевидны – необходимо иметь более одного базового сорта. Поэтому модуль Prim определяет принадлежность базовых типов к сорту S.

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

Если сорт не задан явно и он не может быть выведен тайпчекером по контексту использования, такой тип автоматически получает сорт S.

Более явно тип list может быть задан так:

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

Здесь мы определяем новый тип list с двумя конструкторами. Конструктор Nil принимает единственный аргумент – тип 'a сорта S.

Предварительный итог


Итак, программирование на F* не должно вызвать трудности и программистов, знакомых с языками семейства ML. Остальные заинтересовавшиеся читатели могут ознакомиться с примерами на официальном сайте проекта или подождать следующих постов.
Tags:
Hubs:
+14
Comments 11
Comments Comments 11

Articles