(no subject)
Создатель языка Haskell, сэр Simon Peyton Jones сейчас занимается новым поделием под названием Verse Core. Я немного получше сегодня разобрался в этой штуке, и мне кажется понимаю как вкладывать новшества этой штуки в обыкновенные языки программирования.
Во-первых, зачем это нужно? Нужно это для того, чтобы сделать язык более декларативным. Например, можно будет вот так:
Example 1
let x, y, z
x = (y, 3)
x = (2, z)
x
и вот так
Example 2
let x y : ℚ
x + y = 3
2x + y = 5
print(x)
В первом случае уравнения будут решены при помощи унификации, во втором солвером линейных уравнений. Важно что мы это не руками делаем, а пишем условия, а компьютер нам сам находит подходящее решение.
* * *
В качестве базы синтаксиса возьмём идеализированный академический флейвор Котлина, только с let вместо val для введения локальных констант.
На уровне выше всех остальных свободных от побочных эффектов конструкций языка мы введём четыре оператора:
all {body}, one {body}, a | b и _|_.
“Оператор выбора” | проходит через все конструкции языка. Например для любой функции f : (Int)-> Int
мы можем написать
f(1 | 2 | 3) и получить f(1) | f(2) | f(3). Если функция была от нескольких аргументов g : (Int, Int)-> Int, делаем все комбинации, отсортированные лексикографически:
g(1 | 2, 3 | 4) даст g(1, 3) | g(1, 4) | g(2, 3), g(2, 4).
На первый взгляд может показаться, что (1 | 2 | 3) формирует осообе значение типа ChoiceSequence(1, 2, 3), и применение функций к таковому даёт новый ChoiceSequence, но нет, семантика тут не такая. Выбор не функционирует на уровне значений, let x = (1 | 3) присваивает x значение 1, и если что-то пойдёт в будущем не так, то произойдёт fallback и всё последующее (и предыдущее) вычисление будет произведено заново с вариантом x = 3.
Пустая choice sequence обозначается _|_ и к чему её ни примени, получится оно самое.
Оператор one {body} берёт первый из подходящих результатов либо возвращает _|_ если нет ни одного.
Оператор all собирает все результаты в список:
Example 3
all {let x = (3 | 4); x + 1}
Применение операции с побочными эффектами (скажем, print) к значению энфорсит единственность, т.е. если там не ровно один вариант ответа, кидается exception.
Теперь расширим конструкцию let. Прежде у нас всегда был только короткий вариант `let name = value`.
Сейчас мы позволим этой конструкции во-первых вводить неинициализированные переменные
`let name : Type` или даже просто `let name` в ситуации если тип выводим по контексту.
Более того, если Type перечислимый, то тогда конструкция
`let name : Type` эквивалентна `let name = t1 | t2 | ...`, например
`let n : Nat` то же самое что `let n = 0 | 1 | 2 | ...`.
В индентированном блоке после инструкции let мы позволим вводить дополнительные условия на любые переменные или аргументы. Это выше использовалась в примерах 1 и 2. Собственно конструкция `let x = 5` эквивалентна
let x
x = 5
Приведём также следующие примеры
let n : Int
1 < n
n < 5
print(all {n})
# prints 2, 3, 4
А, например, вот такая конструкция
fun factorial(n : Int)
let
n ≥ 0
...
означает, что если факториал попытаются вызвать с отрицательным аргументом, вычисление не начнётся, а сразу будет выдано _|_. А вот вызов factorial(1 | -1) напротив выдаст один единственный результат.
Example 4
let x, f
f = {v ↦ let {v = (3 · 3, 4 + 4)}}
f(x)
print(x)
# (9, 8)
Вызов f(x) принуждает значение x.
Example 5
let list = listOf(10, 20, 30)
let i
list[i]
# third line enforces i = (0, 1, 2), thus the whole program returns (10 | 20 | 30).
Вот такая экспрессивная штука выходит.
Во-первых, зачем это нужно? Нужно это для того, чтобы сделать язык более декларативным. Например, можно будет вот так:
Example 1
let x, y, z
x = (y, 3)
x = (2, z)
x
и вот так
Example 2
let x y : ℚ
x + y = 3
2x + y = 5
print(x)
В первом случае уравнения будут решены при помощи унификации, во втором солвером линейных уравнений. Важно что мы это не руками делаем, а пишем условия, а компьютер нам сам находит подходящее решение.
* * *
В качестве базы синтаксиса возьмём идеализированный академический флейвор Котлина, только с let вместо val для введения локальных констант.
На уровне выше всех остальных свободных от побочных эффектов конструкций языка мы введём четыре оператора:
all {body}, one {body}, a | b и _|_.
“Оператор выбора” | проходит через все конструкции языка. Например для любой функции f : (Int)-> Int
мы можем написать
f(1 | 2 | 3) и получить f(1) | f(2) | f(3). Если функция была от нескольких аргументов g : (Int, Int)-> Int, делаем все комбинации, отсортированные лексикографически:
g(1 | 2, 3 | 4) даст g(1, 3) | g(1, 4) | g(2, 3), g(2, 4).
На первый взгляд может показаться, что (1 | 2 | 3) формирует осообе значение типа ChoiceSequence(1, 2, 3), и применение функций к таковому даёт новый ChoiceSequence, но нет, семантика тут не такая. Выбор не функционирует на уровне значений, let x = (1 | 3) присваивает x значение 1, и если что-то пойдёт в будущем не так, то произойдёт fallback и всё последующее (и предыдущее) вычисление будет произведено заново с вариантом x = 3.
Пустая choice sequence обозначается _|_ и к чему её ни примени, получится оно самое.
Оператор one {body} берёт первый из подходящих результатов либо возвращает _|_ если нет ни одного.
Оператор all собирает все результаты в список:
Example 3
all {let x = (3 | 4); x + 1}
Применение операции с побочными эффектами (скажем, print) к значению энфорсит единственность, т.е. если там не ровно один вариант ответа, кидается exception.
Теперь расширим конструкцию let. Прежде у нас всегда был только короткий вариант `let name = value`.
Сейчас мы позволим этой конструкции во-первых вводить неинициализированные переменные
`let name : Type` или даже просто `let name` в ситуации если тип выводим по контексту.
Более того, если Type перечислимый, то тогда конструкция
`let name : Type` эквивалентна `let name = t1 | t2 | ...`, например
`let n : Nat` то же самое что `let n = 0 | 1 | 2 | ...`.
В индентированном блоке после инструкции let мы позволим вводить дополнительные условия на любые переменные или аргументы. Это выше использовалась в примерах 1 и 2. Собственно конструкция `let x = 5` эквивалентна
let x
x = 5
Приведём также следующие примеры
let n : Int
1 < n
n < 5
print(all {n})
# prints 2, 3, 4
А, например, вот такая конструкция
fun factorial(n : Int)
let
n ≥ 0
...
означает, что если факториал попытаются вызвать с отрицательным аргументом, вычисление не начнётся, а сразу будет выдано _|_. А вот вызов factorial(1 | -1) напротив выдаст один единственный результат.
Example 4
let x, f
f = {v ↦ let {v = (3 · 3, 4 + 4)}}
f(x)
print(x)
# (9, 8)
Вызов f(x) принуждает значение x.
Example 5
let list = listOf(10, 20, 30)
let i
list[i]
# third line enforces i = (0, 1, 2), thus the whole program returns (10 | 20 | 30).
Вот такая экспрессивная штука выходит.