Введение
F* – это новый язык с зависимыми типами, разработанный в недрах Microsoft Research для построения доказательств свойств программ. F* компилируется в байткод .Net и прозрачно интегрируется с другими языками, включая F#, на основе которого он и построен. Вы можете попробовать F* в браузере или скачать альфа-версию компилятора и сопутствующих примеров тут. Формализация F* в системе Coq доступна для всех желающих.
Итак, основные фичи нового языка:
- Self-certification: тайпчекер F* верифицирован с использованием F*. Подробнее об этом можно почитать тут.
- В настоящее время javascript де-факто стал основным языком для построения фронтэнда веб-приложений. Многие современные языки умеют компилироваться в Javascript. Инженеры Microsoft Research создали компилятор, который имеет компилировать достаточно большое подмножество F* в Javascript. Это означает, что программист может развернуть свою программу на F* на веб-страницах и получить гарантию того, что его код работает доказуемо правильно. Подробности можно почитать тут.
- Существует диалект «monadic F*», в котором реализована новая методология верификации с помощью монады Дейкстры.
Тех читателей, кто не знает что такое зависимые типы и для чего они нужны, я отсылаю к соответствующей статье в википедии. Теория типов в языках программирования – это довольно обширная область знаний, обзор которой займет не одну сотню страниц. Краткая суть такова: Хенк Барендрегт предложил наглядную модель для описания восьми различных систем типизированного по Чёрчу лямбда-исчисления. Так называемый лямбда-куб представляет собой трехмерный куб, в вершинах которого находятся различные системы типизации, а направленные ребра указывают направление включения.
Таким образом, более примитивная система типизации является частным случаем более продвинутой. В базовой вершине располагается обычное типизированное лямбда-исчисление, термы которого зависят от термов, а типы в зависимостях не участвуют. Более подробно познакомиться с лямбда-исчислением можно прочитав монографию Барендрегта «Ламбда-исчисление его синтаксис и семантика».
Различные языки функционального программирования поддерживают различные системы типов, представленных в лямбда-кубе. Λ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. Остальные заинтересовавшиеся читатели могут ознакомиться с примерами на официальном сайте проекта или подождать следующих постов.
