July 9th, 2012

glider

саммари меты

Много мыслей, мало что могу сформулировать, ибо моих знаний явно не хватает. Здесь присутствующим хочу посоветовать заценить уже опубликованные слайды на сайте конференции: http://meta2012.pereslavl.ru/program/program.html и ждать, когда опубликуют толки про: Development of the Productive Forces (суперкомпилятор для System F), неназванные темы из Session 7 (было очень интересно про то, как суперкомпиляция может привести к сверхлинейному ускорению).

Единственное что очень впечатлил следующий факт. Суперкомпиляция это не алгоритм, который преобразует программы, а скорее ноушен о том, что символическую интерпретацию можно обогатить сверткой (за деталями прогонки, обобщения и свертки отправляю уважаемых читателей к статье Ильи Ключникова в седьмом номере ПФП). Можно суперкомпилировать вывод типов в System F. Ребе udpn утверждает, что благодаря этому можно изрядно облегчить программирование на Агде. Я не шарю, поэтому подожду комментариев.
glider

зависимые типы в рантайме

Во время обсуждений на конфе я услышал про язык Алдор, который умеет вот что (хз где я это нагуглил, у меня остался только сниппет в эверноуте, паперу или слайды я уже найти не могу):

define ZmodCat(n:Integer):Category == Ring with {
  if (prime? n) then Field;
  Zmod(n:Integer):ZmodCat(n) == add {
    Rep == Integer;

    (a:%) + (b:%):% ==
    per mod((rep a) + (rep b), n);

    if (prime? n) then {
      inv(x:%):% == ...
    }
  }
}

Есть у нас кольцо вычетов по модулю n. Если n составное, то это кольцо (т.е определены сложение, умножение, ноль и единица). Если n простое, то это группа, ибо есть инверсия и можно вызвать inv. Иначе должна быть ошибка.

Моего ограниченного понимания зависимых типов хватает на то, чтобы осознать, что это можно сделать в случае, если n - константа времени компиляции. Но вот один чел на конфе утверждал, что этот же пример в Алдоре будет работать, если n вычисляется динамически (не просто 2 + 2, а реально динамически). "Работать" в том плане, что проверка типов прозрачно отложится до рантайма, и что программисту не надо будет никаких проверок писать руками - за него все сделает компилятор.