![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Раз уж заговорили об ООП
Mar. 24th, 2015 12:17 pmСовсем недавно Андреас Россберг показал, как надо было делать 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ω), позволяющего удобно описывать тайпклассы и алгебраические структуры более общего вида. Единственное, из соображений того самого удобства, хочется поддержки наследования (не дублировать определения кольца в определении поля) и номинального сабтайпинга (язык должен понимать, что поле это тоже кольцо, раз мы одно от другого унаследовали). Особенно их хочется, когда начинаешь пользоваться орнаментами...
С другой стороны, подход к прозрачности/инкапсуляции в модулях тут ad hoc'овый, в то время как Конор МакБрайд (https://pigworker.wordpress.com/2015/01/05/linear-dependent-types/) показал, как надо. Просто в модулях (они же контексты) поля надо аннотировать элементами моноида {0, 1, *}, 0 это proof-irrelevant-поля, это те самые opaque-поля, значение которых мы не можем смотреть в рантайме, программа относительно них таким образом заведомо параметрично-полиморфна. Элемент * означает, что значение поля можно использовать сколько угодно раз, это как обычно. А вот значение 1, означает что элемент можно использовать ровно один раз, это позволяет представлять resources/entities.
Польза "ООП" в рамках функциональных языков программирования сводится именно к поддержке вот такого синтаксического сахара (не выходяшего за рамки подлежащего исчисления, напр. System Fω), позволяющего удобно описывать тайпклассы и алгебраические структуры более общего вида. Единственное, из соображений того самого удобства, хочется поддержки наследования (не дублировать определения кольца в определении поля) и номинального сабтайпинга (язык должен понимать, что поле это тоже кольцо, раз мы одно от другого унаследовали). Особенно их хочется, когда начинаешь пользоваться орнаментами...
