gds (gds) wrote,
gds
gds

Господин Т-в, известный бывший кащенази, оказывается, серьёзно занялся функциональщиной в финансовых областях. Само по себе -- замечательно, я считаю.
А вот что мы читаем про зависимые типы: http://sorhed.livejournal.com/538077.html . Сначала я тоже было достал свой инструмент и даже как бы приготовился его любовно полировать, жалея, что не могу использовать для практических применений agda/coq (а то и что-то ещё, с зависимыми типами), но что-то меня остановило.
Напомню, изначально проблема в том, что с параметрическим типом, имеющим разные типовые параметры, надо уметь работать различными функциями, зависящими от параметров (как минимум, по критерию "можно/нельзя"), и уметь это статически типизировать.
И тут я начал вспоминать, где же мне приходилось такое делать.
"Ба!", -- думаю я. -- "Да это же обычный Паттерн "Фантомные Типы"! Ну да, универсальная типизация хиндли-милнера плюс параметрическая типизация.
type currency;
type commodity;
type instrument 'asset1 'asset2 = ...;
value some_generic_function : instrument 'a 'b -> some_result;
value function_for_currency1 : instrument currency 'b -> some_other_result;
value function_for_barter : instrument commodity commodity -> some_very_other_result;

И, конечно, небольшая ловкость рук в реализации значений с типом instrument 'asset1 'asset2. Однако, в целом, там всё можно свести к паттерн-матчингу (и assert false, например, для случаев, которые типизация явно не пропустит), а то и к более продуманным типам, допускающим подтипизацию (полиморфные варианты и объекты).
После изготовления -- оформить в модуль (надеюсь, в х-е они есть? ну, такие, с сигнатурками.) и использовать строго-типизированный интерфейс. При желании -- оформить как private type и открыть read-only доступ к представлению значений с типом instrument 'asset1 'asset2.

Хотел ещё Вставить картинку Вставить медиаролик Отключить автоформатирование, но уже запечатал конверт. Всем чмоке!

upd/
Ах да, вот ещё что имел ввиду автор: окамловское решение -- фууууу, потому что оно тупое, работает, даёт нужную типизацию и всё такое, а зависимые типы -- ваааау, потому что cs-ёбство для посвящённых, не реализованное почти нигде в практических языках программирования.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 13 comments
Ну к чему эта истерия, блин!
Разумеется, что имеется в виду, что если потребуется чуть бОльшее, то как в окамеле, так и в хацкеле, придётся извращаться, подыскивая выражение этого в типах.
А в зависимых типах надо будет только чуть усложнить тип.
Хотя, впрочем, это мои мысли, а за тов. sorhed я не готов утверждать, что именно он подразумевал.
я к тому, что люди игнорируют простые решения, предпочитая сложные. Конечно, потом может понадобиться и типизированный блекджек с типизированными шлюхами, но пока нужно гораздо более простое.
Ты же не пишешь фреймворк для логгирования (уровни событий, цели (файлы/консоль/syslogd), преобразование параметров функций в текст, препроцессор для исходников (надо же втыкать запись в лог в начале и в конце выполнения функции!)) в тех случаях, когда нужно всего лишь выдать пользователю две строки наподобие "12:52:00 Начинаем работу" + "12:55:23 Заканчиваем работу".
Так и тут: во-первых, для решения конкретной проблемы не нужны зависимые типы, и, во-вторых, решение -- в посте.
В рамках программирования в языке с зависимыми типами это нихера не простое решение.
Речь же, опять же, идёт о том, что если бы было простое и массовое программирование в зависимых типах, то вот эти самые фантомы в такой форме были бы не нужны.
Я всё больше склоняюсь к тому, чтобы хацкель пользовать только как backend и отличный runtime (GHC).
И несмотря на непродакшенность агды и некоторую непривычность, количество всякаго вуду в "обычных" языках типа хацкеля и окамеля, начинает превышать неудобство использования агды, по моему мнению.
Сейчас пока мы будем пользовать хацкель, но уже на следующем этапе от него будем избавляться.
> В рамках программирования в языке с зависимыми типами это нихера не простое решение.

Я и говорю: язык с зависимыми типами сам по себе является сложным решением, тогда как для данной конкретной проблемы есть простое решение на фантомных типах.

Про агду -- понял. Ну, у меня жс пока, палюбасику, и работы дофига, а там -- хоть чорт лысый пусть http обслуживает. Конечно, тем не менее, внутряк интересен.
> язык с зависимыми типами
> сам по себе является сложным решением

Так вот, я утверждаю, что агда уже сейчас проще, чем даже окамель, не говоря уже о хацкеле.
Более того, исходя из того, что я недавно узнал про окамель, так и CoQ уже попроще него будет ;-)
Сложность в этих языках только в практическом использованиие - мало библиотек, нет runtime'ов.
Но это решаемо.
Они умеют генерить в Haskell или OCaml, в агде даже есть нативное пользование хацкельных библиотек.

Насчёт остального... Будет всё, будет.
Впрочем, мне тут Капитан подсказывает, что есть ещё одна сложность в практическом использовании - мало практики использования.
Более того, исходя из того, что я недавно узнал про окамель...
Что же это было?
Говорят (тсссс, тихо!), что у него система типов не сильно-то и проще хацкелевой.
Наговаривают, наверное?
Мне сложно сравнить, я обе плохо знаю.
Если вспомнить про объекты, ко- и контравариантность, функторы над модулями, первоклассные модули (в 3.12), фантомные типы, existentials и пр., то определенно не очень простая система. Но мне всегда казалось, что в GHC и всяких коках еще сложнее должно быть.
Да, GHC ещё чуть посложнее будет.
А CoQ попроще будет, хоть и более мощный.
Правда, мелочей там сейчас в этом коке уже многовато.
Но вот агда2 совершенно точно проще и заметно.
если целью программирования является написание рабочего кода, а не, например, построение формальных доказательств или реализация лямбда-исчисления, то главным достоинством системы типов является умение описать вещи, встречающиеся в предметной области, так, чтобы они были близко к языку (чтобы был низкий импеданс, так сказать). Вот тут уже интересно, чтобы система типов была богатой. Пофиг, что модули и записи делают фактически одно дело, и пофиг, что записи и объекты похожи -- для некоторых применений лучше взять одно, для других -- другое. Опять же, подтипизация на полиморфных вариантах и объектах -- тоже штука, которую кое-где приходится эмулировать, а в окамле она просто есть.
Коковая (и уж Агдова точно) система типов для этого достаточно богатая и при этом более простая и естественная, чем хацкельная, ну и окамлёвая, впридачу.
Про подтипизацию согласен, правда, в большинстве случаев достаточно классов типов, и в Коке они есть.
В агде2 нету, но от этого никто не будет страдать, ибо эмуляция через записи в зависимых типах в 90% случаев вполне так удобна. За 100% не скажу, опыта маловато, но похоже, что даже и так.
Вот например, надо нам монадЪ. Ну сделали мы его записью из двух функций - return и >>=. Но можно вспомнить, что мы можем брать не просто какой-то тип данных, а функтор. И в зависимых типах это выглядит вполне естественно.
Перефразирую то, что я сказал ранее.
Даже окамель будет уже посложнее даже кока, а уж агды и подавно.
И несмотря на непродакшенность агды, где-то уже "вот сейчас" точка наступает, когда надо пользовать именно её, несмотря на практические недостатки.
Про кок скажу, что не нравится он мне очень, хотя уже и вполне продакшн.
А в категориях всё ищо проще...
Я думаю, что стоит открыть направление -
теоретико-категорный кащенизм!
Кто меня поддержит?