Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Раз уж заговорили об ООП

Совсем недавно Андреас Россберг показал, как надо было делать SML, см. http://www.mpi-sws.org/~rossberg/1ml/1ml.pdf. В MLях традиционно (т.е. во всех ML без зависимых типов) существует два независимых уровня языка: языковое ядро и язык описания модулей/функторов. Андреас Россберг, показал как обойтись без такого расслоения, сделать модули first class citizens, и при этом не выйти за рамки System Fω, не потерять разрешимости тайп-чекинга и весьма сильного автовыведения типов, не смотря на довольно сильный сабтайпинг. Конечно знать бы заранее, SML надо было бы основывать именно на этом подходе, он во сто крат элегантнее.

С другой стороны, подход к прозрачности/инкапсуляции в модулях тут ad hoc'овый, в то время как Конор МакБрайд (https://pigworker.wordpress.com/2015/01/05/linear-dependent-types/) показал, как надо. Просто в модулях (они же контексты) поля надо аннотировать элементами моноида {0, 1, *}, 0 это proof-irrelevant-поля, это те самые opaque-поля, значение которых мы не можем смотреть в рантайме, программа относительно них таким образом заведомо параметрично-полиморфна. Элемент * означает, что значение поля можно использовать сколько угодно раз, это как обычно. А вот значение 1, означает что элемент можно использовать ровно один раз, это позволяет представлять resources/entities.

Польза "ООП" в рамках функциональных языков программирования сводится именно к поддержке вот такого синтаксического сахара (не выходяшего за рамки подлежащего исчисления, напр. System Fω), позволяющего удобно описывать тайпклассы и алгебраические структуры более общего вида. Единственное, из соображений того самого удобства, хочется поддержки наследования (не дублировать определения кольца в определении поля) и номинального сабтайпинга (язык должен понимать, что поле это тоже кольцо, раз мы одно от другого унаследовали). Особенно их хочется, когда начинаешь пользоваться орнаментами...
Tags: deptypes, fprog
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment