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

Введение


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. Остальные заинтересовавшиеся читатели могут ознакомиться с примерами на официальном сайте проекта или подождать следующих постов.
Поделиться публикацией
AdBlock похитил этот баннер, но баннеры не зубы — отрастут

Подробнее
Реклама
Комментарии 11
  • +7
    Из статьи абсолютно непонятно, что такое «зависимые типы», какие задачи они решают и зачем понадобилось делать целый язык для валидации.

    Если я правильно понимаю, зависимый тип — это, например, "int в диапазоне от 0 до 10", или «некий объект, обладающий методом DoStuff()». С помощью таких ограничений можно статически анализировать динамически типизируемые языки, как например JS, и обнаруживать ошибки еще на этапе компиляции.

    Если я не прав, поправьте пожалуйста.
    • +3
      Существует структурная эквивалентность между программами и математическими доказательствами, которая формализуется в виде изоморфизма между типизированным исчислением и логическими системами (изоморфизм Карри-Говарда). Фактически можно построить тип, выражающий сложные математические свойства.

      Логика высказываний соответствует простому типизированному лямбда-исчислению, исчисление предикатов — лямбда-исчислению с зависимыми типами и т.п.

      Более подробно о теории типов можно почитать в великолепном учебнике «Типы в языках программирования» за авторством Б. Пирса.
      • +6
        Вы скопировали это из Википедии, или правда так выражаетесь? :)
      • +3
        Ваш первый пример зависимого типа правильный, а второй — нет (второй пример ближе к структурным типам, как, например, интерфейсы в Go).

        На самом деле, зависимые типы на самом верхнем уровне достаточно простая концепция. Пусть у вас есть тип List<T>. В таком случае тип List можно рассматривать как функцию над типами (вы даёте List тип, например, String, и получаете обратно тоже тип, List<String>). Это типы, параметризованные типами — система \lambda \omega.

        Теперь представьте, что вы параметризуете тип не другим типом, а каким-либо значением — числом 10, строкой "string", каким-нибудь объектом. Например, если Vector<N> обозначает список чего-то длиной N, где N — натуральное число: Vector<10>, то тип Vector является зависимым типом. Система типов для лямбда-исчисления, которая позволяет такое делать, и есть \lambda P.
        • +3
          Для справки, третий вариант — значения, зависящие от типов — это просто полиморфизм. Лучше всего это продемонстрировать на языке типа хаскеля. Например, значение (вернее, не значение, а терм) 10 в зависимости от своего типа может быть разным. Например, 10 :: Int даёт целое число 10, 10 :: Double даёт число с плавающей точкой 10.0, 10 :: Complex Double может дать комплексное число 10 + 0i, 10 :: YourType может дать некоторое значение типа YourType, если для этого типа реализован класс типов Num. То есть, в зависимости от того, какой тип мы приписываем литералу (или другому терму, переменной, например), у него будет cвоё значение.
        • +2
          Я не пиарюсь, но вот статья на хабре. Может прояснится.
          Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
          Но вообще штука очень даже интересная.
          Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.
          • 0
            Видел вашу статью. Некоторое время назад, когда я начинал изучать зависимые типы и теорем-пруверы, выбирал между Agda и Coq. В итоге выбрал второе: есть как минимум два отличных учебника, плюс Coq более популярен, плюс написан на OCaml и умеет экстрактится в него.
            • 0
              Не, ну это холивар :-D
              Agda лучше интегрируется с Haskell, чем Coq с OCaml.
              Но плюс Coq'а действительно в учебниках и намного большей истории.
              А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.
              • 0
                Дружище, а не перечислите ли названия этих учебников по Coq? Я пока что читаю Пирса, но не отказался бы от обзора альтернативных источников.
                • +1
                  О, я тоже на этот топик только сейчас наткнулся — искал, что пишут на Хабре про Coq… Так вот, у автора этой записи ymn есть небольшой вводный тьюториал по Coq из нескольких записей. В конце первой есть ссылки на 2 книги: «Software Foundations» и «Certified Programming with Dependent Types» — я думаю, это и есть вышеупомянутые «два отличных учебника».
                  • 0
                    Забавно, я тут по этой же причине :)

          Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.