Применение 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! :)