Compare commits
17 Commits
7623787b1c
...
localizati
| Author | SHA1 | Date | |
|---|---|---|---|
| 0b5748cc5a | |||
| cd574b43fd | |||
| 8466a5601e | |||
| 845d1ae7d8 | |||
| 988bf72786 | |||
| 8557dc4399 | |||
| 7d1fcdb0c5 | |||
| bda78fed78 | |||
| b0e501f086 | |||
| 385ae59133 | |||
| 49469bdf12 | |||
| 020417e971 | |||
| eff0de5330 | |||
| b219f6855e | |||
| 068d0218b0 | |||
| 65215ccdd6 | |||
| 3e9f6a14f2 |
11
config.toml
11
config.toml
@@ -1,9 +1,8 @@
|
|||||||
baseURL = "https://danilafe.com"
|
languageCode = "en"
|
||||||
languageCode = "en-us"
|
|
||||||
title = "Daniel's Blog"
|
title = "Daniel's Blog"
|
||||||
theme = "vanilla"
|
theme = "vanilla"
|
||||||
pygmentsCodeFences = true
|
pygmentsCodeFences = true
|
||||||
pygmentsStyle = "github"
|
pygmentsUseClasses = true
|
||||||
summaryLength = 20
|
summaryLength = 20
|
||||||
|
|
||||||
[markup]
|
[markup]
|
||||||
@@ -11,3 +10,9 @@ summaryLength = 20
|
|||||||
endLevel = 4
|
endLevel = 4
|
||||||
ordered = false
|
ordered = false
|
||||||
startLevel = 3
|
startLevel = 3
|
||||||
|
|
||||||
|
[languages]
|
||||||
|
[languages.en]
|
||||||
|
baseURL = "https://danilafe.com"
|
||||||
|
[languages.ru]
|
||||||
|
baseURL = "https://ru.danilafe.com"
|
||||||
|
|||||||
8
content/_index.ru.md
Normal file
8
content/_index.ru.md
Normal file
@@ -0,0 +1,8 @@
|
|||||||
|
---
|
||||||
|
title: Daniel's Blog
|
||||||
|
description: Персональный блог Данилы Федорина о функциональном программировании, дизайне компиляторов, и многом другом!
|
||||||
|
---
|
||||||
|
## Привет!
|
||||||
|
Добро пожаловать на мой сайт. Здесь, я пишу на многие темы, включая фунциональное программирование, дизайн компилляторов, теорию языков программирования, и иногда компьютерные игры. Я надеюсь, что здесь вы найдете что-нибуть интересное!
|
||||||
|
|
||||||
|
Вы читаете русскою версию моего сайта. Я только недавно занялся его переводом, и до этого времени редко писал на русском. Я заранеее извиняюсь за присутствие орфографических или грамматических ошибок.
|
||||||
97
content/blog/00_compiler_intro.ru.md
Normal file
97
content/blog/00_compiler_intro.ru.md
Normal file
@@ -0,0 +1,97 @@
|
|||||||
|
---
|
||||||
|
title: Пишем Компилятор Для Функционального Языка на С++, Часть 0 - Вступление
|
||||||
|
date: 2019-08-03T01:02:30-07:00
|
||||||
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
description: "todo"
|
||||||
|
---
|
||||||
|
Год назад, я был записан на курс по компиляторам. Я ждал этого момента почти два учебных года: еще со времени школы меня интересовало создание языков программирования. Однако я был разочарован - заданный нам финальный проект полностью состоял из склеивания вместе написанных профессором кусочков кода. Склеив себе такой грустный компилятор, я не почувствовал бы никакой гордости. А я хотел бы гордиться всеми своими проектами.
|
||||||
|
|
||||||
|
Вместо стандартного задания, я решил -- с разрешением профессора -- написать компилятор для ленивого функционального языка, используя отличную книгу Саймона Пейтона Джоунса, _Implementing functional languages: a tutorial_. На курсе мы пользовались С++, и мой проект не был исключением. Получился прикольный маленький язык, и теперь я хочу рассказать вам, как вы тоже можете создать ваш собственный функциональный язык.
|
||||||
|
|
||||||
|
### Примечание к Русской Версии
|
||||||
|
Вы читаете русскою версию этой статьи. Оригинал ее был написан год назад, и с тех пор объем всей серии немного изменился. Я планировал описать только те части компилятора, которые я успел закончить и сдать профессору: лексический анализ, синтаксический разбор, мономорфную проверку типов, и компиляцию простых выражений с помощью LLVM. Закончив и описав все эти части, я решил продолжать разрабатывать компилятор, и описал сборку мусора, полиморфную проверку типов, полиморфные структуры данных, а также компиляцию более сложных выражений. Вместо того чтобы писать наивный перевод английской версии -- притворяясь что я не знаю о перемене моих планов -- я буду вносить в эту версию изменения соответствующие сегодняшнему состоянию компилятора. Части статей не затронутые этими изменениями я тоже не буду переводить слово в слово, иначе они будут звучать ненатурально. Тем не менее техническое содержание каждой статьи будет аналогично содержанию ее английской версии, и код будет тот же самый.
|
||||||
|
|
||||||
|
### Мотивация
|
||||||
|
Начать эту серию меня подтолкнули две причины.
|
||||||
|
|
||||||
|
Во-первых, почти все учебники и вступления к созданию компиляторов, с которыми я сталкивался, были написаны об императивных языках, часто похожих на C, C++, Python, или JavaScript. Я считаю, что в компиляции функциональных языков -- особенно ленивых -- есть много чего интересного, и все это относительно редко упоминается.
|
||||||
|
|
||||||
|
Во-вторых, меня вдохновили книги, как Software Foundations. Все содержание Software Foundations, например, написано в форме комментариев языка Coq. Таким образом, можно не только читать саму книгу, но и сразу же запускать находящийся рядом с комментариями код. Когда описываемый код под рукой, легче экспериментировать и интереснее читать. Принимая это во внимание, я выкладываю вместе с каждой статьей соответствующую версию компилятора; в самой статье описывается код именно из этой версии. Все части написанной мною программы полностью доступны.
|
||||||
|
|
||||||
|
### Обзор
|
||||||
|
Прежде чем начинать наш проект, давайте обсудим, чего мы будем добиваться, и какими способами.
|
||||||
|
|
||||||
|
#### “Классические” Стадии Компилятора
|
||||||
|
Части большинства компиляторов достаточно независимы друг от друга (по крайней мере в теории). Мы можем разделить их на следующие шаги:
|
||||||
|
|
||||||
|
* Лексический анализ
|
||||||
|
* Синтаксический разбор
|
||||||
|
* Анализ и оптимизация
|
||||||
|
* Генерация кода
|
||||||
|
|
||||||
|
Не все вышеописанные шаги встречаются в каждом компиляторе. Например, компилятор в моих статьях совсем не оптимизирует код. Также, в некоторых компиляторах присутствуют шаги не упомянутые в этом списке. Язык Idris -- как и многие другие функциональные языки -- переводится сначала в упрощённый язык “TT”, и только после этого проходит через анализ. Иногда, с целью ускорить компиляцию, несколько шагов производятся одновременно. В целом, все эти стадии помогут нам сориентироваться, но никаким образом нас не ограничат.
|
||||||
|
|
||||||
|
#### Темы, Которые Мы Рассмотрим
|
||||||
|
Мы начнем с нуля, и пошагово построим компилятор состоящий из следующих частей:
|
||||||
|
|
||||||
|
* Лексического анализа с помощью программы Flex.
|
||||||
|
* Синтаксического разбора с помощью программы Bison.
|
||||||
|
* Сначала мономорфной, а позже полиморфной проверки типов.
|
||||||
|
* Вычисления программ используя абстрактную машину G-machine.
|
||||||
|
* Компиляции абстрактных инструкций G-machine используя LLVM.
|
||||||
|
* Простого сбора мусора.
|
||||||
|
|
||||||
|
Наша цель - создать ленивый, функциональный язык.
|
||||||
|
|
||||||
|
#### Темы, Которые Мы Не Рассмотрим
|
||||||
|
Для того, чтобы создать любую нетривиальную программу, нужно иметь значительный объем опыта и знаний; одному человеку было бы сложно научить всему этому. У меня буквально не хватило бы на это времени, да и исход такой попытки был бы неблагоприятным: опытным читателям было бы труднее извлечь из статей новую информацию, а неопытным читателям все равно было бы недостаточно подробно. Вместо того, чтобы портить таким образом свои статьи, я буду полагаться на то, что вы достаточно комфортно себя чувствуете с некоторыми темами. В число этих тем входят:
|
||||||
|
|
||||||
|
* [Теория алгоритмов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D0%BE%D0%B2),
|
||||||
|
более конкретно [теория автоматов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2).
|
||||||
|
Детерминированные и недетерминированные автоматы кратко упоминаются в первой статье во время лексического анализа, a синтаксический разбор мы выполним используя контекстно-свободную грамматику.
|
||||||
|
* [Функциональное программирование](https://ru.wikipedia.org/wiki/%D0%A4%D1%83%D0%BD%D0%BA%D1%86%D0%B8%D0%BE%D0%BD%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D0%B5), с легкой примесью [лямбда-исчисления](https://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5).
|
||||||
|
Мы будем пользоваться лямбда-функциями, каррированием, и системой типов Хиндли-Мильнер, которая часто встречается в языках семейства ML.
|
||||||
|
* С++. Я стараюсь писать код правильно и по последним стандартам, но я не эксперт. Я не буду объяснять синтаксис или правила С++, но разумеется буду описывать что именно делает мой код с точки зрения компиляторов.
|
||||||
|
|
||||||
|
#### Синтаксис Нашего Языка
|
||||||
|
Саймон Пейтон Джоунс, в одном из своих [~~двух~~ многочисленных](https://www.reddit.com/r/ProgrammingLanguages/comments/dsu115/compiling_a_functional_language_using_c/f6t52mh?utm_source=share&utm_medium=web2x&context=3) трудов на тему функциональных языков, отметил что большинство из этих языков по сути очень похожи друг на друга; часто, главная разница состоит именно в их синтаксисе. На данный момент, выбор синтаксиса - наша главная степень свободы. Нам точно нужно предоставить доступ к следующим вещам:
|
||||||
|
|
||||||
|
* Декларациям функций
|
||||||
|
* Вызову функций
|
||||||
|
* Арифметике
|
||||||
|
* Aлгебраическим типам данных
|
||||||
|
* Сопоставлению с образцом
|
||||||
|
|
||||||
|
Позже, мы добавим к этому списку выражения let/in и лямбда-функции. С арифметикой разобраться не сложно - числа будут писаться просто как `3`, значения выражений как `1+2*3` будут высчитываться по обычным математическим правилам. Вызов функций ненамного сложнее. Выражение `f x` будет значить “вызов функции `f` с параметром `x`”, а `f x + g y` - “сумма значений `f x` и `g y`”. Заметьте, что вызов функций имеет приоритет выше приоритета арифметических операций.
|
||||||
|
|
||||||
|
Теперь давайте придумаем синтаксис для деклараций функций. Я предлогаю следующий вариант:
|
||||||
|
|
||||||
|
```
|
||||||
|
defn f x = { x + x }
|
||||||
|
```
|
||||||
|
|
||||||
|
А для типов данных:
|
||||||
|
|
||||||
|
```
|
||||||
|
data List = { Nil, Cons Int List }
|
||||||
|
```
|
||||||
|
|
||||||
|
Заметьте, что мы пока пользуемся мономорфными декларациями типов данных. Позже, в одиннадцатой части, мы добавим синтаксис для полиморфных деклараций.
|
||||||
|
|
||||||
|
В последнюю очередь, давайте определимся с синтаксисом сопоставления с образцом:
|
||||||
|
|
||||||
|
```
|
||||||
|
case l of {
|
||||||
|
Nil -> { 0 }
|
||||||
|
Cons x xs -> { x }
|
||||||
|
}
|
||||||
|
```
|
||||||
|
|
||||||
|
Представленная выше распечатка читается как: “если лист `l` сопоставим с `Nil`, то все выражение возвращает значение `0`; иначе, если лист сопоставим с `Cons x xs` (что, опираясь на декларацию `List`, означает, что лист состоит из значений `x`, с типом `Int`, и `xs`, с типом `List`), то выражение возвращает `x`”.
|
||||||
|
|
||||||
|
Вот и конец нашего обзора! В следующей статье, мы начнем с лексического анализа, что является первым шагом в процессе трансформации программного текста в исполняемые файлы.
|
||||||
|
|
||||||
|
### Список Статей
|
||||||
|
* Ой! Тут как-то пусто.
|
||||||
|
* Вы, наверно, читаете черновик.
|
||||||
|
* Если нет, то пожалуйста напишите мне об этом!
|
||||||
@@ -361,7 +361,7 @@ I think this is a good approach. Should we want to add more types to our languag
|
|||||||
lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
|
lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
|
||||||
proofs, and keep the `typecheck` method the same. Had we not used this approach,
|
proofs, and keep the `typecheck` method the same. Had we not used this approach,
|
||||||
and instead decided to pattern match on types inside of `typecheck`, we would've quickly
|
and instead decided to pattern match on types inside of `typecheck`, we would've quickly
|
||||||
found that this only works for types with finitely many values. When we add polymorphic tuples
|
found that this only works for languages with finitely many types. When we add polymorphic tuples
|
||||||
and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
|
and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
|
||||||
so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
|
so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
|
||||||
solution. I think that this leads us back to `decEq`.
|
solution. I think that this leads us back to `decEq`.
|
||||||
|
|||||||
216
content/blog/typesafe_interpreter_tuples.md
Normal file
216
content/blog/typesafe_interpreter_tuples.md
Normal file
@@ -0,0 +1,216 @@
|
|||||||
|
---
|
||||||
|
title: Meaningfully Typechecking a Language in Idris, With Tuples
|
||||||
|
date: 2020-08-12T15:48:04-07:00
|
||||||
|
tags: ["Idris"]
|
||||||
|
---
|
||||||
|
|
||||||
|
Some time ago, I wrote a post titled
|
||||||
|
[Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}).
|
||||||
|
I then followed it up with
|
||||||
|
[Meaningfully Typechecking a Language in Idris, Revisited]({{< relref "typesafe_interpreter_revisited.md" >}}).
|
||||||
|
In these posts, I described a hypothetical
|
||||||
|
way of 'typechecking' an expression data type `Expr` into a typesafe form `SafeExpr`.
|
||||||
|
A `SafeExpr` can be evaluated without any code to handle type errors,
|
||||||
|
since it's by definition impossible to construct ill-typed expressions using
|
||||||
|
it. In the first post, we implemented the method only for simple arithmetic
|
||||||
|
expressions; in my latter post, we extended this to support `if`-expressions.
|
||||||
|
Near the end of the post, I made the following comment:
|
||||||
|
|
||||||
|
> When we add polymorphic tuples and lists, we start being able to construct an
|
||||||
|
arbitrary number of types: `[a]`. `[[a]]`, and so on. Then, we cease to be able t
|
||||||
|
enumerate all possible pairs of types, and require a recursive solution. I think
|
||||||
|
that this leads us back to [our method].
|
||||||
|
|
||||||
|
Recently, I thought about this some more, and decided that it's rather simple
|
||||||
|
to add tuples into our little language. The addition of tuples mean that our
|
||||||
|
language will have an infinite number of possible types. We would have
|
||||||
|
`Int`, `(Int, Int)`, `((Int, Int), Int)`, and so on. This would make it
|
||||||
|
impossible to manually test every possible case in our typechecker,
|
||||||
|
but our approach of returning `Dec (a = b)` will work just fine.
|
||||||
|
|
||||||
|
### Extending The Syntax
|
||||||
|
First, let's extend our existing language with expressions for
|
||||||
|
tuples. For simplicity, let's use pairs `(a,b)` instead of general
|
||||||
|
`n`-element tuples. This would make typechecking less cumbersome while still
|
||||||
|
having the interesting effect of making the number of types in our language
|
||||||
|
infinite. We can always represent the 3-element tuple `(a,b,c)` as `((a,b), c)`,
|
||||||
|
after all. To be able to extract values from our pairs, we'll add the `fst` and
|
||||||
|
`snd` functions into our language, which accept a tuple and return its
|
||||||
|
first or second element, respectively.
|
||||||
|
|
||||||
|
Our `Expr` data type, which allows ill-typed expressions, ends up as follows:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 31 39 "hl_lines=7 8 9" >}}
|
||||||
|
|
||||||
|
I've highlighted the new lines. The additions consist of the `Pair` constructor, which
|
||||||
|
represents the tuple expression `(a, b)`, and the `Fst` and `Snd` constructors,
|
||||||
|
which represent the `fst e` and `snd e` expressions, respectively. In
|
||||||
|
a similar manner, we extend our `SafeExpr` GADT:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 41 49 "hl_lines=7 8 9" >}}
|
||||||
|
|
||||||
|
Finally, to provide the `PairType` constructor, we extend the `ExprType` and `repr` functions:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 1 11 "hl_lines=5 11" >}}
|
||||||
|
|
||||||
|
### Implementing Equality
|
||||||
|
An important part of this change is the extension of the `decEq` function,
|
||||||
|
which compares two types for equality. The kind folks over at `#idris` previously
|
||||||
|
recommended the use of the `Dec` data type for this purpose. A value of
|
||||||
|
type `Dec P`
|
||||||
|
{{< sidenote "right" "decideable-note" "is either a proof that \(P\) is true, or a proof that \(P\) is false." >}}
|
||||||
|
It's possible that a proposition \(P\) is not provable, and neither is \(\lnot P\).
|
||||||
|
It is therefore not possible to construct a value of type <code>Dec P</code> for
|
||||||
|
any proposition <code>P</code>. Having a value of type <code>Dec P</code>, then,
|
||||||
|
provides us nontrivial information.
|
||||||
|
{{< /sidenote >}} Our `decEq` function, given two types `a` and `b`, returns
|
||||||
|
`Dec (a = b)`. Thus, it will return either a proof that `a = b` (which we can
|
||||||
|
then use to convince the Idris type system that two `SafeExpr` values are,
|
||||||
|
in fact, of the same type), or a proof of `a = b -> Void` (which tells
|
||||||
|
us that `a` and `b` are definitely not equal). If you're not sure what the deal with `(=)`
|
||||||
|
and `Void` is, check out
|
||||||
|
[this section]({{< relref "typesafe_interpreter_revisited.md" >}}#curry-howard-correspondence)
|
||||||
|
of the previous article.
|
||||||
|
|
||||||
|
A lot of the work in implementing `decEq` went into constructing proofs of falsity.
|
||||||
|
That is, we needed to explicitly list every case like `decEq IntType BoolType`, and create
|
||||||
|
a proof that `IntType` cannot equal `BoolType`. However, here's how we use `decEq` in
|
||||||
|
the typechecking function:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 76 78 >}}
|
||||||
|
|
||||||
|
We always throw away the proof inequality! So, rather than spending the time
|
||||||
|
constructing useless proofs like this, we can just switch `decEq` to return
|
||||||
|
a `Maybe (a = b)`. The `Just` case will tell us that the two types are equal
|
||||||
|
(and, as before, provide a proof); the `Nothing` case will tell us that
|
||||||
|
the two types are _not_ equal, and provide no further information. Let's
|
||||||
|
see the implementation of `decEq` now:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 13 23 >}}
|
||||||
|
|
||||||
|
Lines 14 through 16 are pretty simple; in this case, we can tell at a glance
|
||||||
|
that the two types are equal, and Idris can infer an equality proof in
|
||||||
|
the form of `Refl`. We return this proof by writing it in a `Just`.
|
||||||
|
Line 23 is the catch-all case for any combination of types we didn't handle.
|
||||||
|
Any combination of types we don't handle is invalid, and thus, this case
|
||||||
|
returns `Nothing`.
|
||||||
|
|
||||||
|
What about lines 17 through 22? This is the case for handling the equality
|
||||||
|
of two pair types, `(lt1, lt2)` and `(rt1, rt2)`. The equality of the two
|
||||||
|
types depends on the equality of their constituents. That is, if we
|
||||||
|
know that `lt1 = rt1` and `lt2 = rt2`, we know that the two pair types
|
||||||
|
are also equal. If one of the two equalities doesn't hold, the two
|
||||||
|
pairs obviously aren't equal, and thus, we should return `Nothing`.
|
||||||
|
This should remind us of `Maybe`'s monadic nature: we can first compute
|
||||||
|
`decEq lt1 rt1`, and then, if it succeeds, compute `decEq lt2 rt2`.
|
||||||
|
If both succeed, we will have in hand the two proofs, `lt1 = rt1`
|
||||||
|
and `lt2 = rt2`. We achieve this effect using `do`-notation,
|
||||||
|
storing the sub-proofs into `subEq1` and `subEq2`.
|
||||||
|
|
||||||
|
What now? Once again, we have to use `replace`. Recall its type:
|
||||||
|
|
||||||
|
```Idris
|
||||||
|
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
|
||||||
|
```
|
||||||
|
|
||||||
|
Given some proposition in terms of `a`, and knowing that `a = b`, `replace`
|
||||||
|
returns the original proposition, but now in terms of `b`. We know for sure
|
||||||
|
that:
|
||||||
|
|
||||||
|
```Idris
|
||||||
|
PairType lt1 lt2 = PairType lt1 lt2
|
||||||
|
```
|
||||||
|
|
||||||
|
We can start from there. Let's handle one thing at a time, and try
|
||||||
|
to replace the second `lt1` with `rt1`. Then, we can replace the second
|
||||||
|
`lt2` with `rt2`, and we'll have our equality!
|
||||||
|
|
||||||
|
Easier said than done, though. How do we tell Idris which `lt1`
|
||||||
|
we want to substitute? After all, of the following are possible:
|
||||||
|
|
||||||
|
```Idris
|
||||||
|
PairType rt1 lt2 = PairType lt1 lt2 -- First lt1 replaced
|
||||||
|
PairType lt1 lt2 = PairType rt1 lt2 -- Second lt1 replaced
|
||||||
|
PairType rt1 lt2 = PairType rt1 lt2 -- Both replaced
|
||||||
|
```
|
||||||
|
|
||||||
|
The key is in the signature, specifically the expressions `P x` and `P y`.
|
||||||
|
We can think of `P` as a function, and of `replace` as creating a value
|
||||||
|
of `P` applied to another argument. Thus, the substitution will occur
|
||||||
|
exactly where the argument of `P` is used. Then, to achieve each
|
||||||
|
of the above substitution, we can write `P` as follows:
|
||||||
|
|
||||||
|
```Idris {linenos=table, hl_lines=[2]}
|
||||||
|
t1 => PairType t1 lt2 = PairType lt1 lt2
|
||||||
|
t1 => PairType lt1 lt2 = PairType t1 lt2
|
||||||
|
t1 => PairType t1 lt2 = PairType t1 lt2
|
||||||
|
```
|
||||||
|
|
||||||
|
The second function (highlighted) is the one we'll need to use to attain
|
||||||
|
the desired result. Since `P` is an implicit argument to `replace`,
|
||||||
|
we can explicitly provide it with `{P=...}`, leading to the following
|
||||||
|
line:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 20 20>}}
|
||||||
|
|
||||||
|
We now have a proof of the following proposition:
|
||||||
|
|
||||||
|
```Idris
|
||||||
|
PairType lt1 lt2 = PairType rt1 lt2
|
||||||
|
```
|
||||||
|
|
||||||
|
We want to replace the second `lt2` with `rt2`, which means that we
|
||||||
|
write our `P` as follows:
|
||||||
|
|
||||||
|
```Idris
|
||||||
|
t2 => PairType lt1 lt2 = PairType rt1 t2
|
||||||
|
```
|
||||||
|
|
||||||
|
Finally, we perform the second replacement, and return the result:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 21 22 >}}
|
||||||
|
|
||||||
|
Great! We have finished implement `decEq`.
|
||||||
|
|
||||||
|
### Adjusting The Typechecker
|
||||||
|
It's time to make our typechecker work with tuples.
|
||||||
|
First, we need to fix the `IfElse` case to accept `Maybe (a=b)` instead
|
||||||
|
of `Dec (a=b)`:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 71 78 "hl_lines=7 8" >}}
|
||||||
|
|
||||||
|
Note that the only change is from `Dec` to `Maybe`; we didn't need to add new cases
|
||||||
|
or even to know what sort of types are available in the language.
|
||||||
|
|
||||||
|
Next, we can write the cases for the new expressions in our language. We can
|
||||||
|
start with `Pair`, which, given expressions of types `a` and `b`, creates
|
||||||
|
an expression of type `(a,b)`. As long as the arguments to `Pair` are well-typed,
|
||||||
|
so is the `Pair` expression itself; thus, there are no errors to handle.
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 79 83 >}}
|
||||||
|
|
||||||
|
The case for `Fst` is more complicated. If the argument to `Fst` is a tuple
|
||||||
|
of type `(a, b)`, then `Fst` constructs from it an expression
|
||||||
|
of type `a`. Otherwise, the expression is ill-typed, and we return an error.
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 84 89 >}}
|
||||||
|
|
||||||
|
The case for `Snd` is very similar:
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 90 96 >}}
|
||||||
|
|
||||||
|
### Evaluation Function and Conclusion
|
||||||
|
We conclude with our final `eval` and `resultStr` functions,
|
||||||
|
which now look as follows.
|
||||||
|
|
||||||
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 97 111 "hl_lines=7-9 13-15" >}}
|
||||||
|
|
||||||
|
As you can see, we require no error handling in `eval`; the expressions returned by
|
||||||
|
`typecheck` are guaranteed to evaluate to valid Idris values. We have achieved our goal,
|
||||||
|
with very little changes to `typecheck` other than the addition of new language
|
||||||
|
constructs. In my opinion, this is a win!
|
||||||
|
|
||||||
|
As always, you can see the code on my Git server. Here's
|
||||||
|
[the latest Idris file,](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV3.idr)
|
||||||
|
if you want to check it out (and maybe verify that it compiles). I hope you found
|
||||||
|
this interesting!
|
||||||
78
themes/vanilla/assets/scss/code.scss
Normal file
78
themes/vanilla/assets/scss/code.scss
Normal file
@@ -0,0 +1,78 @@
|
|||||||
|
@import "variables.scss";
|
||||||
|
|
||||||
|
$code-color-lineno: grey;
|
||||||
|
$code-color-keyword: black;
|
||||||
|
$code-color-type: black;
|
||||||
|
$code-color-comment: grey;
|
||||||
|
|
||||||
|
code {
|
||||||
|
font-family: $font-code;
|
||||||
|
background-color: $code-color;
|
||||||
|
border: $code-border;
|
||||||
|
padding: 0 0.25rem 0 0.25rem;
|
||||||
|
}
|
||||||
|
|
||||||
|
pre code {
|
||||||
|
display: block;
|
||||||
|
box-sizing: border-box;
|
||||||
|
padding: 0.5rem;
|
||||||
|
overflow: auto;
|
||||||
|
}
|
||||||
|
|
||||||
|
.chroma {
|
||||||
|
.lntable {
|
||||||
|
border-spacing: 0;
|
||||||
|
padding: 0.5rem 0 0.5rem 0;
|
||||||
|
background-color: $code-color;
|
||||||
|
border-radius: 0;
|
||||||
|
border: $code-border;
|
||||||
|
display: block;
|
||||||
|
overflow: auto;
|
||||||
|
|
||||||
|
td {
|
||||||
|
padding: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
code {
|
||||||
|
border: none;
|
||||||
|
padding: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
pre {
|
||||||
|
margin: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
.lntd:last-child {
|
||||||
|
width: 100%;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.lntr {
|
||||||
|
display: table-row;
|
||||||
|
}
|
||||||
|
|
||||||
|
.lnt {
|
||||||
|
display: block;
|
||||||
|
padding: 0 1rem 0 1rem;
|
||||||
|
color: $code-color-lineno;
|
||||||
|
}
|
||||||
|
|
||||||
|
.hl {
|
||||||
|
display: block;
|
||||||
|
background-color: #fffd99;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.kr, .k {
|
||||||
|
font-weight: bold;
|
||||||
|
color: $code-color-keyword;
|
||||||
|
}
|
||||||
|
|
||||||
|
.kt {
|
||||||
|
font-weight: bold;
|
||||||
|
color: $code-color-type;
|
||||||
|
}
|
||||||
|
|
||||||
|
.c, .c1 {
|
||||||
|
color: $code-color-comment;
|
||||||
|
}
|
||||||
@@ -31,31 +31,6 @@ h1, h2, h3, h4, h5, h6 {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
code {
|
|
||||||
font-family: $font-code;
|
|
||||||
background-color: $code-color;
|
|
||||||
}
|
|
||||||
|
|
||||||
pre code {
|
|
||||||
display: block;
|
|
||||||
padding: 0.5rem;
|
|
||||||
overflow-x: auto;
|
|
||||||
border: $code-border;
|
|
||||||
}
|
|
||||||
|
|
||||||
div.highlight table {
|
|
||||||
border: $code-border !important;
|
|
||||||
border-radius: 0px;
|
|
||||||
|
|
||||||
pre {
|
|
||||||
margin: 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
code {
|
|
||||||
border: none;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
.container {
|
.container {
|
||||||
position: relative;
|
position: relative;
|
||||||
margin: auto;
|
margin: auto;
|
||||||
|
|||||||
35
themes/vanilla/i18n/en.toml
Normal file
35
themes/vanilla/i18n/en.toml
Normal file
@@ -0,0 +1,35 @@
|
|||||||
|
[Home]
|
||||||
|
other = "Home"
|
||||||
|
|
||||||
|
[About]
|
||||||
|
other = "About"
|
||||||
|
|
||||||
|
[Resume]
|
||||||
|
other = "Resume"
|
||||||
|
|
||||||
|
[Tags]
|
||||||
|
other = "Tags"
|
||||||
|
|
||||||
|
[RecentPosts]
|
||||||
|
other = "Recent posts"
|
||||||
|
|
||||||
|
[AllPosts]
|
||||||
|
other = "All Posts"
|
||||||
|
|
||||||
|
[PostedOn]
|
||||||
|
other = "Posted on {{ .Date.Format \"January 2, 2006\" }}."
|
||||||
|
|
||||||
|
[TableOfContents]
|
||||||
|
other = "Table of Contents"
|
||||||
|
|
||||||
|
[ReadingTime]
|
||||||
|
other = "{{ .WordCount }} words, about {{ .ReadingTime }} minutes to read."
|
||||||
|
|
||||||
|
[Note]
|
||||||
|
other = "note"
|
||||||
|
|
||||||
|
[Tagged]
|
||||||
|
other = "Tagged \"{{ .Title }}\""
|
||||||
|
|
||||||
|
[AllTags]
|
||||||
|
other = "Below is a list of all the tags ever used on this site."
|
||||||
35
themes/vanilla/i18n/ru.toml
Normal file
35
themes/vanilla/i18n/ru.toml
Normal file
@@ -0,0 +1,35 @@
|
|||||||
|
[Home]
|
||||||
|
other = "Главная"
|
||||||
|
|
||||||
|
[About]
|
||||||
|
other = "О Сайте"
|
||||||
|
|
||||||
|
[Resume]
|
||||||
|
other = "Резюме"
|
||||||
|
|
||||||
|
[Tags]
|
||||||
|
other = "Метки"
|
||||||
|
|
||||||
|
[RecentPosts]
|
||||||
|
other = "Недавние статьи"
|
||||||
|
|
||||||
|
[AllPosts]
|
||||||
|
other = "Все Статьи"
|
||||||
|
|
||||||
|
[PostedOn]
|
||||||
|
other = "Статья опубликована {{ .Date.Format \"January 2, 2006\" }}."
|
||||||
|
|
||||||
|
[TableOfContents]
|
||||||
|
other = "Оглавление"
|
||||||
|
|
||||||
|
[ReadingTime]
|
||||||
|
other = "{{ .WordCount }} слов, чтение займет примерно {{ .ReadingTime }} минут."
|
||||||
|
|
||||||
|
[Note]
|
||||||
|
other = "примечание"
|
||||||
|
|
||||||
|
[Tagged]
|
||||||
|
other = "Статьи c меткой \"{{ .Title }}\""
|
||||||
|
|
||||||
|
[AllTags]
|
||||||
|
other = "Ниже приводится список всех меток на сайте."
|
||||||
@@ -6,14 +6,14 @@
|
|||||||
<a class="button" href="{{ $.Site.BaseURL }}/tags/{{ . | urlize }}">{{ . }}</a>
|
<a class="button" href="{{ $.Site.BaseURL }}/tags/{{ . | urlize }}">{{ . }}</a>
|
||||||
{{ end }}
|
{{ end }}
|
||||||
</p>
|
</p>
|
||||||
<p>Posted on {{ .Date.Format "January 2, 2006" }}.</p>
|
<p>{{ i18n "PostedOn" . }}</p>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
<div class="post-content">
|
<div class="post-content">
|
||||||
{{ if not (eq .TableOfContents "<nav id=\"TableOfContents\"></nav>") }}
|
{{ if not (eq .TableOfContents "<nav id=\"TableOfContents\"></nav>") }}
|
||||||
<div class="table-of-contents">
|
<div class="table-of-contents">
|
||||||
<div class="wrapper">
|
<div class="wrapper">
|
||||||
<em>Table of Contents</em>
|
<em>{{ i18n "TableOfContents" }}</em>
|
||||||
{{ .TableOfContents }}
|
{{ .TableOfContents }}
|
||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
|
|||||||
@@ -1,7 +1,7 @@
|
|||||||
{{ define "main" }}
|
{{ define "main" }}
|
||||||
{{ .Content }}
|
{{ .Content }}
|
||||||
|
|
||||||
Recent posts:
|
{{ i18n "RecentPosts" }}:
|
||||||
<ul class="post-list">
|
<ul class="post-list">
|
||||||
{{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
|
{{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
|
||||||
{{ partial "post.html" . }}
|
{{ partial "post.html" . }}
|
||||||
|
|||||||
@@ -6,14 +6,16 @@
|
|||||||
<meta name="description" content="{{ .Description }}">
|
<meta name="description" content="{{ .Description }}">
|
||||||
{{ end }}
|
{{ end }}
|
||||||
|
|
||||||
<link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata&family=Raleway&family=Lora&display=block" media="screen">
|
<link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata:wght@400;700&family=Raleway&family=Lora&display=block" media="screen">
|
||||||
<link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
|
<link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
|
||||||
{{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
|
{{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
|
||||||
{{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
|
{{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
|
||||||
|
{{ $code := resources.Get "scss/code.scss" | resources.ToCSS | resources.Minify }}
|
||||||
{{ $icon := resources.Get "img/favicon.png" }}
|
{{ $icon := resources.Get "img/favicon.png" }}
|
||||||
{{- partial "sidenotes.html" . -}}
|
{{- partial "sidenotes.html" . -}}
|
||||||
<link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
|
<link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
|
||||||
<link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
|
<link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
|
||||||
|
<link rel="stylesheet" href="{{ $code.Permalink }}" media="screen">
|
||||||
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
|
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
|
||||||
<link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
|
<link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
|
||||||
|
|
||||||
|
|||||||
@@ -3,11 +3,11 @@
|
|||||||
</div>
|
</div>
|
||||||
<nav>
|
<nav>
|
||||||
<div class="container">
|
<div class="container">
|
||||||
<a href="/">Home</a>
|
<a href="/">{{ i18n "Home" }}</a>
|
||||||
<a href="/about">About</a>
|
<a href="/about">{{ i18n "About" }}</a>
|
||||||
<a href="https://github.com/DanilaFe">GitHub</a>
|
<a href="https://github.com/DanilaFe">GitHub</a>
|
||||||
<a href="/Resume-Danila-Fedorin.pdf">Resume</a>
|
<a href="/Resume-Danila-Fedorin.pdf">{{ i18n "Resume" }}</a>
|
||||||
<a href="/tags">Tags</a>
|
<a href="/tags">{{ i18n "Tags" }}</a>
|
||||||
<a href="/blog">All Posts</a>
|
<a href="/blog">{{ i18n "AllPosts" }}</a>
|
||||||
</div>
|
</div>
|
||||||
</nav>
|
</nav>
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
<li>
|
<li>
|
||||||
<a href="{{ .Permalink }}" class="post-title">{{ .Title }}</a>
|
<a href="{{ .Permalink }}" class="post-title">{{ .Title }}</a>
|
||||||
<p class="post-wordcount">{{ .WordCount }} words, about {{ .ReadingTime }} minutes to read.</p>
|
<p class="post-wordcount">{{ i18n "ReadingTime" . }}</p>
|
||||||
<p class="post-preview">{{ .Summary }} . . .</p>
|
<p class="post-preview">{{ .Summary }} . . .</p>
|
||||||
</li>
|
</li>
|
||||||
|
|||||||
@@ -6,4 +6,9 @@
|
|||||||
{{ .Scratch.Set "u" $t }}
|
{{ .Scratch.Set "u" $t }}
|
||||||
{{ end }}
|
{{ end }}
|
||||||
{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
|
{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
|
||||||
{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d" (.Get 2)) }}
|
{{ if (.Get 4) }}
|
||||||
|
{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
|
||||||
|
{{ else }}
|
||||||
|
{{ .Scratch.Set "opts" "" }}
|
||||||
|
{{ end }}
|
||||||
|
{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
|
||||||
|
|||||||
@@ -4,7 +4,7 @@
|
|||||||
<label class="sidenote-label" for="numbernote-{{ $id }}">({{ $id }})</label>
|
<label class="sidenote-label" for="numbernote-{{ $id }}">({{ $id }})</label>
|
||||||
<input class="sidenote-checkbox" type="checkbox" id="numbernote-{{ $id }}"></input>
|
<input class="sidenote-checkbox" type="checkbox" id="numbernote-{{ $id }}"></input>
|
||||||
<span class="sidenote-content sidenote-{{ .Get 0 }}">
|
<span class="sidenote-content sidenote-{{ .Get 0 }}">
|
||||||
<span class="sidenote-delimiter">[note:</span>
|
<span class="sidenote-delimiter">[{{ i18n "note" }}:</span>
|
||||||
{{ .Inner }}
|
{{ .Inner }}
|
||||||
<span class="sidenote-delimiter">]</span>
|
<span class="sidenote-delimiter">]</span>
|
||||||
</span>
|
</span>
|
||||||
|
|||||||
@@ -2,7 +2,7 @@
|
|||||||
<label class="sidenote-label" for="{{ .Get 1 }}">{{ .Get 2 }}</label>
|
<label class="sidenote-label" for="{{ .Get 1 }}">{{ .Get 2 }}</label>
|
||||||
<input class="sidenote-checkbox" type="checkbox" id="{{ .Get 1 }}"></input>
|
<input class="sidenote-checkbox" type="checkbox" id="{{ .Get 1 }}"></input>
|
||||||
<span class="sidenote-content sidenote-{{ .Get 0 }}">
|
<span class="sidenote-content sidenote-{{ .Get 0 }}">
|
||||||
<span class="sidenote-delimiter">[note:</span>
|
<span class="sidenote-delimiter">[{{ i18n "Note" }}:</span>
|
||||||
{{ .Inner }}
|
{{ .Inner }}
|
||||||
<span class="sidenote-delimiter">]</span>
|
<span class="sidenote-delimiter">]</span>
|
||||||
</span>
|
</span>
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
{{ define "main" }}
|
{{ define "main" }}
|
||||||
<h2>Tagged "{{ .Title }}"</h2>
|
<h2>{{ i18n "Tagged" . }}</h2>
|
||||||
|
|
||||||
<ul class="post-list">
|
<ul class="post-list">
|
||||||
{{ range .Pages.ByDate.Reverse }}
|
{{ range .Pages.ByDate.Reverse }}
|
||||||
|
|||||||
@@ -1,6 +1,6 @@
|
|||||||
{{ define "main" }}
|
{{ define "main" }}
|
||||||
<h2>{{ .Title }}</h2>
|
<h2>{{ i18n "Tags" }}</h2>
|
||||||
Below is a list of all the tags ever used on this site.
|
{{ i18n "AllTags" }}
|
||||||
|
|
||||||
<ul>
|
<ul>
|
||||||
{{ range sort .Pages "Title" }}
|
{{ range sort .Pages "Title" }}
|
||||||
|
|||||||
Reference in New Issue
Block a user