- PVSM.RU - https://www.pvsm.ru -
F* – это новый язык [1] с зависимыми типами, разработанный в недрах Microsoft Research для построения доказательств свойств программ. F* компилируется в байткод .Net и прозрачно интегрируется с другими языками, включая F#, на основе которого он и построен. Вы можете попробовать [2] F* в браузере или скачать [3] альфа-версию компилятора и сопутствующих примеров тут. Формализация F* в системе Coq доступна [4] для всех желающих.
Итак, основные фичи нового языка:
Тех читателей, кто не знает что такое зависимые типы и для чего они нужны, я отсылаю к соответствующей статье [8] в википедии. Теория типов в языках программирования – это довольно обширная область знаний, обзор которой займет не одну сотню страниц. Краткая суть такова: Хенк Барендрегт предложил наглядную модель для описания восьми различных систем типизированного по Чёрчу лямбда-исчисления. Так называемый лямбда-куб представляет собой трехмерный куб, в вершинах которого находятся различные системы типизации, а направленные ребра указывают направление включения.
Таким образом, более примитивная система типизации является частным случаем более продвинутой. В базовой вершине располагается обычное типизированное лямбда-исчисление, термы которого зависят от термов, а типы в зависимостях не участвуют. Более подробно познакомиться с лямбда-исчислением можно прочитав монографию Барендрегта «Ламбда-исчисление его синтаксис и семантика».
Различные языки функционального программирования поддерживают различные системы типов, представленных в лямбда-кубе. Λ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. Остальные заинтересовавшиеся читатели могут ознакомиться с примерами на официальном сайте проекта или подождать следующих постов.
Автор: ymn
Источник [9]
Сайт-источник PVSM.RU: https://www.pvsm.ru
Путь до страницы источника: https://www.pvsm.ru/microsoft-research/35962
Ссылки в тексте:
[1] новый язык: http://research.microsoft.com/en-us/projects/fstar/
[2] попробовать: http://rise4fun.com/FStar
[3] скачать: http://research.microsoft.com/en-us/downloads/e9089b8e-8871-46a8-987b-75effdcf70e6/default.aspx
[4] доступна: http://research.microsoft.com/en-us/um/people/juanchen/fstar.tgz
[5] тут: http://research.microsoft.com/en-us/um/people/nswamy/papers/popl2012-paper211.pdf
[6] тут: http://research.microsoft.com/apps/pubs/?id=176601
[7] «monadic F*»: http://research.microsoft.com/en-us/um/people/nswamy/supp/dijkstra-js.html
[8] статье: https://en.wikipedia.org/wiki/Dependent_type
[9] Источник: http://habrahabr.ru/post/182340/
Нажмите здесь для печати.