Применение FP и теории типов на практике

Поручение ДУРАКА: давайте создадим настоящий язык FP с нуля (на Haskell)

Часть 1: Введение — почему; ранняя архитектура компилятора; Nat, Bool, суммирование, равенство; Введение в «Машину основных списков»

Это первая статья из серии, описывающей создание FOOL3: функциональный объектно-ориентированный язык низкого уровня — язык функционального программирования с мощной системой типов (настолько близкой к Исчислению конструкций, насколько мы можем получить, не делая наших кружится голова), который компилируется в .Net и JavaScript в качестве исходных целей. Серия предполагает некоторое знакомство с Haskell, лямбда-исчислением и знакомством с теорией типов. Полный исходный код для этого шага доступен здесь: https://github.com/superstringsoftware/fool3/tree/tutorial01

Почему другой язык?

Поскольку мы любим Haskell, благодаря этой любви мы полюбили теорию типов, и мы действительно верим, что индустрия может извлечь выгоду из (возможно, глупого) подхода проектирование из первых принципов для создания чего-то надежного и красивого, что все современные Нас могут научить исследования ФП и теории типов, а также опыт использования и разработки Haskell. В то же время нам нужно что-то с надеюсь, менее крутой кривой обучения, что построено на основе стандартных отраслевых технологий (отсюда .Net и JavaScript в качестве целей компиляции) и что использует некоторые замечательные принципы, такие как « написать один раз, запустить где угодно и DRY на следующий уровень».

В конце концов, мы хотим иметь возможность написать что-то вроде:

// COMMON:
type Post = { title, body : String }
type User = { name:String, age:Int, role:String}
authorship:Relation = One2Many (User,Post)

// SERVER:
db = buildDatabase([Post,User], [authorship], DBTypes.Mongo)

currentUser : Entity(User) = loggedIn(db.User)
newPost : Post = Post {"Hi", "Hello world"}

tr = [
  enp:Entity(Post) = db.Post.add(newPost),
  db.setRelation(authorship, currentUser, enp}]

db.executeTransaction(tr)

// CLIENT:

posts = GVM.subscribe(Post, srvData)

newPostForm = buildForm(Post, 
    Button("Create Post", onClick = posts.add(fromForm(newPostForm))), 
    visualOptions)

… и пусть Система типов и компилятор позаботятся о доказательстве правильности, о метапрограммировании отношений между сущностями, операциях CRUD с различными базами данных, об автоматическом создании форм пользовательского интерфейса как в .Net, так и в Интернете ( а также другие цели компиляции в конечном итоге), синхронизации данных между вычислительными узлами и т. д., чтобы получить полнофункциональное и математически правильное (:)) приложение для ведения блога менее чем в 100 строк кода. Для этого нам нужна система типов, намного более мощная, чем даже та, что предоставляет Haskell, но мы определенно будем повторно использовать множество идей, которые уже были опробованы в других местах.

Звучит безумно и слишком хорошо, чтобы быть правдой? Ну, может быть, а может и нет — давайте начнем и посмотрим, к чему это нас приведет, не так ли? :) Во всяком случае, следуя этой серии статей, вы можете узнать кое-что новое о Haskell и поэкспериментировать вместе с нами.

1. Язык первой итерации

В первой итерации, код которой можно скачать здесь: https://github.com/superstringsoftware/fool3/tree/tutorial01, наш язык представлен следующей библиотекой (см. base.fool), который определяет два типа — Bool и Nat — и три функции, которые работают с ними (фактически вы можете определять новые типы и функции используя приведенный ниже пример не требующего пояснений синтаксиса — как насчет определения собственной функции умножения для типа Nat или добавления типов Maybe и List и функции на них? Теперь все они должны работать из коробки!)

type Nat = {
  Z,
  Succ (n:Nat)
};

type Bool = { True, False };

function eq(x:Nat,y:Nat):Bool = {
  {Z,Z} -> True,
  {Z,n} -> False,
  {n,Z} -> False,
  {Succ(m),Succ(n)} -> eq(m,n)
};

function plus (x:Nat,y:Nat):Nat = {
  {Z, n} -> n, 
  {Succ(n), m} -> Succ (plus(n, m)) 
};

function not (b:Bool) : Bool = {
    {True}  -> False,
    {False} -> True
};

Это минимальное определение, обманчиво простое, требует от нас создания полного «MVP» для среды компилятора и интерпретатора, начиная с синтаксического анализатора, внутреннего представления поверхностного языка, основного языка, проходов преобразования и т. д. Единственное, чего не хватает от этой начальной итерации идет проверка типов — поскольку это самая сложная часть, мы отложим ее введение на более поздний момент. Этот MVP послужит основой для нашего компилятора/интерпретатора, который мы будем дорабатывать, улучшать и оптимизировать в ходе разработки серии. Мы следуем философии «выпускайте ранние выпуски чаще» или «внедряйте инновации и повторяйте», как мы говорили на Veeam.com. Это означает, что код ни в коем случае не является аккуратным, красивым и оптимизированным, как вы, возможно, ожидаете от него. хорошо поддерживаемые библиотеки Haskell. Здесь мы будем экспериментировать, проверять гипотезы, пробовать разные подходы по мере создания ДУРАКА в наших глупых усилиях, поэтому качество кода будет сильно различаться и оставлять много места для оптимизации и рефакторинга по мере укрепления архитектуры.

Как вы можете догадаться из приведенного выше кода, наша основная библиотека FOOL3 в настоящее время поддерживает обычные типы Product и Sum, например. определение Nat более или менее соответствует следующему коду на Haskell: data Nat = Z | Succ Nat . Определения функций поддерживают сопоставление с образцом, что было наиболее сложной частью для реализации в текущей версии.

Как только вы загрузите код, соберете его с помощью stack build и запустите среду, вы сможете делать такие вещи, как:

λfool3. one = Succ(Z)
Received expressions: 
Binding (Var {name = "one", typ = UNDEFINED, val = App (Id "Succ") [Id "Z"]})
CLM:
CLMBIND "one" (CLMCON (ConsTag "Succ" 1) [CLMCON (ConsTag "Z" 0) []])
Added binding one = Succ(Z)
λfool3. three = Succ(Succ(Succ(Z)))
...
λfool3. plus(one,three)
trying interactive expression
CLM:
plus (one, three)
Final result:
Succ {Succ {Succ {Succ {Z {}}}}}
λfool3. eq(one,three)
trying interactive expression
CLM:
eq (one, three)
Final result:
False {}

При желании вы можете включить трассировку, выполнив команду :s trace on, и вы получите гораздо больше отзывов обо всех шагах, которые в данный момент выполняет интерпретатор. Конечно, если вы добавите свои собственные типы и функции в файл base.fool, вы также сможете поиграть с ними.

2. Архитектура компилятора

На высоком уровне наша архитектура строится следующим образом:

  • Мы используем отличную терминальную библиотеку Haskeline в Main.hs в качестве текущего интерфейса.
  • Синтаксический анализатор определяется в Lexer.hs и Parser.hs с использованием Parsec. Мы не будем тратить много времени на анализ синтаксического анализатора, так как есть несколько отличных материалов для чтения. Например, совершенно выдающийся Что бы я хотел знать, изучая Haskell Стивена Диля, парсер которого мы взяли за основу для нашего; В книге Realworld Haskell есть глава о Parsec.
  • Синтаксический анализатор анализирует наш язык в соответствии с определениями языка Surface, указанными в файле Core.hs (имя является исторической ошибкой и будет соответствующим образом исправлено в будущем) в Expr. тип данных. Он довольно обширный, несколько уродливый (например, GADT могут добавить некоторую дополнительную безопасность типов, что мы, возможно, сделаем в будущем), но позволяет нам представить все, что нам нужно, на основе для захвата классов типов/семейств типов, примитивных типов, Pi -types и т. д. в следующих итерациях. Модуль также содержит некоторые вспомогательные функции, обход дерева Expr, красивую печать и т. д.
  • Конвейер компилятора определен в Pipeline.hs и включает в себя несколько проходов: 1) первоначальная очистка парсинга и создание монадической среды (подробнее об этом ниже) , где мы храним все привязки для Типов, Конструкторов и Функций 2) разбор и оптимизация case-операторов внутри определений функций — огромная и уродливая функция с несколькими уровнями рекурсии, для которой понадобится совсем немного работы по рефакторингу в будущем, но пока это работает :) 3) преобразование в CLM — основную машину списков — язык, вдохновленный GHC STG на Haskell (описанный более подробно в наш предыдущий пост о компиляции Haskell в .Net) и имеет свой собственный раздел ниже в этом посте 4) в конце концов, проверка типов, множество проходов оптимизации и, наконец, компиляция в разные цели . Этот последний пункт оставлен для будущих постов — в следующем мы перейдем к компиляции и некоторой базовой проверке типов, а затем будем постепенно улучшаться по мере добавления языковых функций.
  • State.hs определяет нашу монаду верхнего уровня, в которой мы работаем и которая содержит состояние нашего загруженного модуля, интерпретатора, журналов и т. д.:
-- structure keeping our current environment

data Environment = Environment {
    -- Map that keeps all our TypeReps in the current environment
    types        :: NameMap Expr,
    constructors :: NameMap (Lambda, Int), 
    -- constructors are stored with their number inside the sum type
    topLambdas   :: NameMap Lambda,
    topBindings  :: NameMap Var,
    clmLambdas   :: NameMap CLMLam,
    clmBindings  :: NameMap CLMVar,
    outProgram   :: NameMap String
} deriving Show

data InterpreterState = InterpreterState {
    currentFlags :: CurrentFlags,
    -- this is being filled by the parser as we go, so last line in the file will be first here!
    parsedModule :: LTProgram,
    currentSource :: Text,
    currentEnvironment :: Environment
} deriving Show

type IntState = StateT InterpreterState LambdaLoggerMonad
  • ^^^ это преобразователь состояния поверх другой служебной монады — LambdaLoggerMonad — которая находится поверх IO и предоставляет дополнительные возможности ведения журнала и т. д., вы можете покопаться в ней в папке Util, но это не обязательно для того, что мы пытаемся сделать здесь. Если вы не разбираетесь в монадах — рекомендую прочитать мою книгу Волшебный Haskell, в которой бережно выстроена иерархия классов типов Haskell из первых принципов простым языком, но эта серия, наверное, для вас слишком ранняя :)
  • Interpreter.hs – очень простой интерпретатор для основного языка CLM, обеспечивающий некоторую интерактивность внутри среды с опциональным отслеживанием шагов интерпретации. Мы также не будем тратить на это много времени, поскольку нашей конечной целью является компиляция, к которой мы приступим в следующей итерации как для платформ .Net, так и для платформ javascript.
  • CLM.hs предварительно расшифровывается как Core List Machine и является определением нашего Core Language, где все в конечном итоге компилируется для проверки типов и оптимизации, и из которого все компилируется в различные цели, . Net и JavaScript изначально. На него сильно повлияла GHC Spineless-Tagless-G-machine и наша работа по компиляции Haskell в .Net для проприетарных нужд, но в нем используется несколько иной подход, чем в основном лямбда-исчислении. Ниже приведено краткое введение в CLM:

3. Введение в Core List Machine

Название может измениться в будущем, но «Список» отражает главное отличие от основного подхода каррирования лямбда-исчисления: мы работаем с кортежами явно по всем направлениям, как для строго типизированных значений, так и для определений типов, для классов и семейств типов. в конце концов, для вызовов функций, для правильных (!) записей и т. д. Вот текущее определение типа данных CLMExpr, который фиксирует CLM:

data CLMExpr = 
    CLMEMPTY
  | CLMERR String
  | CLMID Name
  | CLMLAM CLMLam
  | CLMBIND Name CLMExpr
  | CLMAPP CLMExpr [CLMExpr] -- saturated application first expr to the tuple of exprs
  | CLMPAP CLMExpr [CLMExpr] -- partial application (When we know the types!)
  | CLMCON ConsTag [CLMExpr] -- saturated constructor application, value in a sense
  | CLMFieldAccess (Name, Int) CLMExpr -- accessing a field of an expr by name or number
  | CLMCASE [CLMConsTagCheck] CLMExpr -- list of constructor checks that must all fold to True bound to an expr
  | CLMPROG [CLMExpr] -- list of expressions, for now used for Actions but needs to change
  | CLMTYPED CLMExpr CLMExpr -- in case we want to give a type to an expression
  | CLMPRIMCALL -- body of the function that is a primitive call
    deriving (Show, Eq)

Если вы знакомы с STG, вы сразу заметите некоторые сходства, а также ключевое различие: где STG определяет приложение ex ex1 ex2как своего рода «дерево» — App ex (App ex1 ex2)) — это классический подход к каррированию на основе лямбда-исчисления, мы используем кортеж явно — CLMAPP ex [ex1,ex2,...,exn] — что означает, что выражение ex применяется к кортежу [ex1,...,exn] . Мы можем по-прежнему так же легко выражать частичное приложение, каррирование, функции как первоклассные граждане и т. д., используя этот подход, при этом используя манипуляции со списками вместо обхода деревьев для множества общих операций и оптимизаций. Возможно, манипулирование списками более интуитивно понятно людям, чем деревья, и упрощает чтение и понимание.

Разные конструкторы представляют разные выражения в нашем языке, которые объясняются в комментариях выше. Заметные вещи, которых сейчас не хватает, — это примитивные типы и литеральные значения, но их очень легко добавить, и мы сделаем это в следующей итерации.

Пара моментов, на которые стоит обратить внимание как в CLM, так и в дизайне нашего поверхностного языка, которые сильно отличаются от Haskell:

  • Взаимодействие с библиотеками .Net/JavaScript и «реальным миром» в целом. Зная из первых рук, насколько «ужасной» концепцией Monad является препятствием для императивных программистов и новичков в целом, мы хотим сделать работу с изменчивостью и «реальным миром» максимально безболезненной. Это может означать использование некоторых сокращений, которые на данный момент охватываются очень простой (хотя и не строго математически определенной) концепцией Действия как отдельного типа Функции, где Функция *должна * быть чистым, в то время как Action может изменяться и взаимодействовать с «реальным миром». Единственное правило на данный момент: вы можете вызывать как действия, так и функции из действий, но вы можете вызывать функции только из других функций. Такого рода захватывает весь смысл «вы не можете избежать монады», при этом пугая людей гораздо меньше. У нас все равно будут монады, заметьте! :)
  • Поскольку мы планируем использовать более или менее исчисление конструкций в качестве нашей системы типов, нет никакой разницы в терминах выражений между «уровнем типа» и «уровнем значения», что делает вещи гораздо более кратким с точки зрения определения типов данных для компилятора, но, конечно, гораздо более сложным с точки зрения вывода/проверки типов, поэтому необходимо сделать некоторые компромиссы
  • Мощная система типов позволяет нам писать типобезопасные определения для многих понятий, которые мы действительно хотели бы иметь возможность выразить в Haskell, но не можем. А также потенциально обеспечить очень элегантное метапрограммирование решения вполне практических вопросов (таких как упомянутая выше абстракция базы данных), а не просто «скучные» зависимые векторы размера n. Это будет нашим основным направлением в будущем — практические проблемы, элегантно решаемые с помощью мощной системы типов. Так же, как очень быстрый пример первого — типобезопасная функция доступа к полю кортежа очень проста с зависимыми типами и может быть представлена ​​примерно так:
proj : PI (i:Nat, tup:(t1, ..., tn)) -> ti
proj (i, (a1:t1, ..., an:tn)) = ai:ti
  • ^^^ это означает, что манипулирование кортежами может стать первоклассным гражданином в нашем языке, который решает ооочень много проблем с повторениями, которые мы наблюдаем сейчас в некоторых очень хороших библиотеках Haskell, но это всего лишь один простой пример. Базы данных (и постоянство в целом), а также графический интерфейс — это другое, гораздо большее, более глубокое, более практичное и более захватывающее, и мы попытаемся решить его в будущем.

Заключение

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

В будущих постах мы потратим гораздо больше времени на объяснение и разработку концепций поверхностного языка, имея в виду практические вопросы, и будем следить за развитием компилятора по пути.

Спасибо за ваше время, ваша команда Superstring Solutions! :)