![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
О чистоте и лени
После N-ной провальной попытки изучить Haskell и понять суть религии под названием "монадический фетишизм", решил изобрести свой "велосипед", то есть чистый и ленивый язык программирования.
Для любой открытой системы важным моментов является взаимодействие с внешним миром. В данном случаем - порядок обмена информацией.
У энергичных языков порядок определяется непосредственно самой последовательностью инструкций в программе. Напротив, для ленивых языков последовательность выполнения инструкций неопределена, а значения вычисляются по мере необходимости. Поэтому для осуществления взаимодействия с внешним миром в ленивые языки порядок вводиться искусственно.
Одним из способов упорядочивания вычислений является ввод дополнительных переменных-маркеров, при помощи которых указываются дополнительные зависимости между подпрограммами. Например, подпрограмма "C" зависит от переменной "b", которая определяется в подпрограмме "B", в свою очередь подпрограмма "B" зависит от переменной "a", значение которой определяется в подпрограмме "A", что приводит к выполнению сначала подпрограммы "A", затем "B" и лишь затем "C". Эти переменные маркеры в Mozart-OZ получили название свободные (unbound) переменные, а в Clean - уникальные типы.
Другим способом упорядочивание вычислений является использование стиля передачи продолжений. Однако этот стиль труден для использования им требует модификации подпрограмм. К счастью последнего можно избежать при помощи подпрограммы-обертки. В Haskell этой оберткой является оператор bind, а монады по сути не что иное, как своеобразный "концептуальный сахар" над стилем передачи продолжений. В свою очередь Haskell оператор do является "синтаксическим сахаром" вокруг монад, создающих иллюзию того, что переменные меняют свое значение.
Так что на самом деле Haskell, как и Clean, - абсолютно чистый язык, а религия "монадический фетишизм" - удел тех, кто на видеть разницы между иллюзией и реальностью.
P.S.
Во загнул! С другой стороны, что взять с простого физ-химика, волей случая написавшего несколько маленьких программ на Perl.
Для любой открытой системы важным моментов является взаимодействие с внешним миром. В данном случаем - порядок обмена информацией.
У энергичных языков порядок определяется непосредственно самой последовательностью инструкций в программе. Напротив, для ленивых языков последовательность выполнения инструкций неопределена, а значения вычисляются по мере необходимости. Поэтому для осуществления взаимодействия с внешним миром в ленивые языки порядок вводиться искусственно.
Одним из способов упорядочивания вычислений является ввод дополнительных переменных-маркеров, при помощи которых указываются дополнительные зависимости между подпрограммами. Например, подпрограмма "C" зависит от переменной "b", которая определяется в подпрограмме "B", в свою очередь подпрограмма "B" зависит от переменной "a", значение которой определяется в подпрограмме "A", что приводит к выполнению сначала подпрограммы "A", затем "B" и лишь затем "C". Эти переменные маркеры в Mozart-OZ получили название свободные (unbound) переменные, а в Clean - уникальные типы.
Другим способом упорядочивание вычислений является использование стиля передачи продолжений. Однако этот стиль труден для использования им требует модификации подпрограмм. К счастью последнего можно избежать при помощи подпрограммы-обертки. В Haskell этой оберткой является оператор bind, а монады по сути не что иное, как своеобразный "концептуальный сахар" над стилем передачи продолжений. В свою очередь Haskell оператор do является "синтаксическим сахаром" вокруг монад, создающих иллюзию того, что переменные меняют свое значение.
Так что на самом деле Haskell, как и Clean, - абсолютно чистый язык, а религия "монадический фетишизм" - удел тех, кто на видеть разницы между иллюзией и реальностью.
P.S.
Во загнул! С другой стороны, что взять с простого физ-химика, волей случая написавшего несколько маленьких программ на Perl.
no subject
no subject
Хаскель никогда не задумывался исключительно простым, всегда был и остаётся красивым, а упрощение понимания - это какая-то странная цель.
no subject
Тем больше читал про монады - тем сильней они становились непонятными. Зачем они, если в Clean обходятся без них? Более того, для виртуальной машины parrot начиная с версий 0.0x, когда разработчики замучились жонглировать состояниями и передали все на CPS, можно легко писать чистый код без всяких монад. Возникает вывод, что монады, для чистого языка не являются необходимостью, а лишь удобная абстракция.
no subject
Вы читали документацию Клина по уникальным типам? Это просто звиздец какой-то. Понимать это, ИМХО, вообще невозможно, а вариантов применения на два порядка меньше, чем у хаскельных монад.
> Возникает вывод, что монады, для чистого языка не являются необходимостью, а лишь удобная абстракция.
Ну. Да. И шо? Удобная? Удобная. Потому и есть.
no subject
Просто путало меня то, что монады расматриваутся как необходимасть.
И это сбивало с толку.
P.S.
Спасибо за беседу. За подтверждение моих догадок.
Пуристический фетишизм
> не являются необходимостью, а лишь удобная абстракция.
Хехе, раз уж на то пошло, то и классы типов не являются необходимыми. Олег Киселёв показал, что достаточно одного предопределенного класса типов, даже новые инстансы у этого класса не нужны для того чтобы эмулировать произвольные классы типов.
Re: Пуристический фетишизм
Re: Пуристический фетишизм
Ссылку не подкинете?
Haskell with just one type class
Re: Haskell with just one type class
Всего один класс. Зато с двумя параметрами и функциональной зависимостью.
Неинтересно.
Re: Haskell with just one type class
Я думал, там банальное
class Pointed c where point :: cс инстансами типаdata Eq a = Eq {(==) :: a -> a -> a} instance Pointed (Eq Int) where point = Eq {(==) = internalIntEqRe: Haskell with just one type class
no subject
no subject
no subject
Разработок полно: есть зависимые типы с человеческим лицом, по сравнению с GADTs/type families (pisigma, ATS guarded types), есть лучшие системы типов для полиморфизма высшего ранга с импредикативного инстанцирования, чем текущие boxy types, есть разработки по типизированному staged execution, более интересные, чем текущее псевдоцитирование и прочий TH.
DPH и вообще вся подсистема паралеллизма похоже вообще какой-то своей жизнью живёт, и непонятно когда превратится в элегантную.
Хаскель от GHC - очень большой язык, монстр, подобно Си++, и это правильно. Он пионер ленивости-чистоты (недоделку Clean и ещё более недоделанные более ранние работы не считаем), да много чего пионер. И красоту ему сохранить практически невозможно.
no subject
> есть зависимые типы с человеческим лицом, по сравнению с GADTs/type families
Секундочку, ни GADT, ни type families зависимых типов не дают. Или я не так понял?
no subject
Надо сделать прокидывание значений между типами и... значениями. Ну, чтобы тип можно было параметризовать числом, например. И иметь возможность получить это число, если что.
GADT как суррогат зависимых типов
Общий обзор, чего можно делать, есть тут:
http://www.haskell.org/haskellwiki/Type_arithmetic
Основной вопрос - что такое зависимые типы. Надо договориться об определении сначала, потому что "типы, зависящие от значений" - это никуда не годное определение.
Касательно type families вроде понятно. А вот на счет GADT. Скажем, есть такая штука, как Reynolds style defunctionalization. Заключается она в том, что в программе все функции заменяют на вызовы одной функции apply таким нехитрым способом:
вместо foo bar пишут apply Foo bar, заводят алгебраик data Function = Foo | Map | Fold | ... ну и в apply пишут case по foo. Так вот, в книжке написано, что apply потребует зависимых типов. Но в то же время она прекрасно реализуется на GADT.
В целом, связь GADT и зависимых типов хорошо сформулирована в дискуссии на LtU:
"GADTs offer many, if not all, of the benefits of dependent types"
http://lambda-the-ultimate.org/node/1293
Соответственно, в Хаскеле уже на момент появления GADTs, до type families, было извращение, позволяющее делать то же, что и зависимые типы, но через одно место.
В-общем, и в эпиграм тоже через одно место, исследования постоянно идут и находят более удачные системы зависимых типов, примеры я приводил. Даже Агду2 можно рассматривать как прорыв по сравнению с эпиграм.