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-ёбство для посвящённых, не реализованное почти нигде в практических языках программирования.
  • 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