Основывая на чём можно выбрать OCamL или Erlang или Haskell

>Я специально настраиваю Емакс так, чтобы скобки были максимально яркие и мигали оранжевым цветом.

Поделись .emacs тру-лиспера. ;)

> Дело вкуса, на самом деле. Если нравится играть в угадайку с компилятором рантайме — милости прошу.

А зачем играть в угадайку? Тебе в любом случае придется писать тесты, с любой системой типов (даже с зависимыми), в случае динамики _больше_ тестов чем в случае статики писать не придется. Потому что если проходятся статически-специфичные тесты, то это гарантирует, что и никаких ошибок связанных с динамической типизацией нет.

Если будешь злоуптортеблять выводом типов — не такое еще выскочит.

Полиморфизм старших рангов без вывода типов? Да вы, батенька, шутник.

Ты не поверишь, но теория типов это как раз та самая предметная область.

Та самая - это какая?

> Взаимоисключающие параграфы.

Это где же? Вот именно что - быстро прогнать тест и обнаружить ошибку, вместо того, чтобы разбираться чего там нагородил тайпчекер.

Ну задай тогда тему...

Э, але, это же ты пытаешься доказать, что статика все заруливает, ты и дай тему, на которой она заруливет. пока у тебя только пег-парсеры, да и то заруливает как-то сомнительно.

> Пишу, конечно. Но одно дело тестировать поведение программы, совсем же другое — выполнять работу компилятора.

А если прошли юнит-тесты, которые проверяют поведение программы, то все тесты, которые покрывают «работу компилятора» пройдут гарантированно. По-этому и писать их не нужно.

>Не могу. Считаем, что здесь динамическая и статическая типизация сыграли вничью, и этот пример просто ничего не доказывает.

Что-то быстро слился хачкель-фанбой. Видать не знает чушка про Calculus of Constructions.

>По-этому и писать их не нужно.
Поэтому и писать их не нужно. nazi fix

Поддерживаю.
В системе важнее то, насколько правильно она работает (что и выясняется с помощью совокупности тестов - модульных, функциональных, регрессионных и интеграционных), а не то, на какой классненькой системе вывода типов она забацана.
И вообще, в разработке, имхо, яп даже не вторичен, а третичен.

Теоретизирующий петушок закукарекал.

Посмотрел бы я как ты для атомной станции юнит-тестики писать собрался.

Видишь ли, есть софт двух типов - первого (софт для всяких атомных станций), который должен быть верифицирован полностью, и второго (все остальное), который верифицировать не надо, достаточно лишь знать, что вероятность того, что оно не работает, крайне мала. Для первого типа система типов хаскиля сильно недостаточна (тут зависимые типы, CoC и доказательства корректности), для второго - сильно избыточна (т.к. есть юнит-тесты). В результате хаскиль пролетает везде.

Поделись .emacs тру-лиспера. ;)

У Алекса Отта смотри конфиг, мой гораздо проще и хуже организован.

Видишь ли, есть софт двух типов - первого (софт для всяких атомных станций), который должен быть верифицирован полностью, и второго (все остальное), который верифицировать не надо

Это расхожее клише. Программное обеспечение слишком ненадёжное, основные автоматические контуры защит тепловых станций делают механическими.

Для первого типа система типов хаскиля сильно недостаточна (тут зависимые типы, CoC и доказательства корректности)

Сильная система типов и статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише. Ариан-5 вполне себе успешно взорвалась из-за переполнения.

Сильная система типов и статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише. Ариан-5 вполне себе успешно взорвалась из-за переполнения.

Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

Кстати, в Ариан софт был на Аде, что символично: мертворожденный бастард языка-зомби Алгол был обречен на «успех».

>то все тесты, которые покрывают «работу компилятора» пройдут гарантированно.

Только в мечтах. На практике, ты никогда не сможешь обеспечить 100% покрытие.

Кроме того, ты опять все сводишь к некой сферической «проверке правильности», причем в какой-то совершенно непонятной интерпретации. Если свести твое утверждение в область электроники, то ты утверждаешь а) что разные виды разъемов не нужны, б) что поскольку тип раъема и зараенее описанный электирческий интерейс не могут гарантировать правильность передаваймых сигналов — они не нужны. Поэтому все провода должны быть одинакового цвета и толщины, а если есть сомнения, то на плате все написано, в) что вместо того чтобы ломать голову почему я не могу воткнуть разъем типа A в разъем типа B, намного проще подключить как есть, подать питание, и тогда выгоревшее место на плате явно укажет на совершенную ошибку.

Абсурд же.

Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

А я вот помню, как darcs с segmentation fault валился. Из-за ошибки в рантайме, написанно на Си, правда, но факт есть факт: формально нельзя доказать, что программа без ошибок работать будет.

Поделись .emacs тру-лиспера. ;)

;;; Common Lisp mode settings
(setq auto-mode-alist
      (append '(("\\.lisp$"   . lisp-mode)
                ("\\.lsp$"    . lisp-mode)
                ("\\.cl$"     . lisp-mode)
                ("\\.asd$"    . lisp-mode)
                ("\\.system$" . lisp-mode))
              auto-mode-alist))
(add-hook 'lisp-mode-hook
          (lambda ()
            (setq lisp-indent-function 'common-lisp-indent-function)
            (setq show-trailing-whitespace t)
            (setq truncate-lines t)))

;;; Redshank mode settings
(autoload 'redshank-mode "redshank"
  "Minor mode for editing and refactoring (Common) Lisp code." t)
(autoload 'turn-on-redshank-mode "redshank"
  "Turn on Redshank mode.  Please see function `redshank-mode'." t)
(add-hook 'lisp-mode-hook 'turn-on-redshank-mode)

;;; SLIME settings
(load (expand-file-name "~/.quicklisp/slime-helper.el"))
(slime-setup '(slime-fancy slime-indentation slime-tramp
               slime-asdf slime-sprof))
(setq lisp-lambda-list-keyword-parameter-alignment t)
(setq lisp-lambda-list-keyword-alignment t)
(setq slime-net-coding-system 'utf-8-unix)
(setq slime-default-lisp 'sbcl)
(setq slime-lisp-implementations
      `((sbcl ("/home/lisper/local/bin/sbcl") :coding-system utf-8-unix)
        (ccl  ("/home/lisper/local/bin/ccl")  :coding-system utf-8-unix)
        (abcl ("/home/lisper/local/bin/abcl") :coding-system utf-8-unix)
        (lw   ("/home/lisper/local/bin/lw")   :coding-system utf-8-unix)))
(eval-after-load 'slime
  '(progn
     (setq common-lisp-hyperspec-root "file:///home/lisper/Documents/Programming/Lisp/Common Lisp/HyperSpec/")
     (setq slime-scratch-file "~/.emacs.d/tmp/scratch.lisp")
     (setq slime-edit-definition-fallback-function 'find-tag)
     (setq slime-complete-symbol*-fancy t)
     (setq slime-complete-symbol-function 'slime-fuzzy-complete-symbol)
     (setq slime-when-complete-filename-expand t)
     (setq slime-truncate-lines nil)
     (setq slime-autodoc-use-multiline-p t)))
(add-hook 'lisp-mode-hook
          (lambda ()
            (setq slime-use-autodoc-mode t)))
(defun my/customized-lisp-keyboard ()
  (define-key slime-repl-mode-map (kbd "C-c ;") 'slime-insert-balanced-comments)
  (local-set-key [C-tab] 'slime-fuzzy-complete-symbol)
  (local-set-key [return] 'newline-and-indent))
(add-hook 'lisp-mode-hook 'my/customized-lisp-keyboard)

> Ну вот зачем же так сразу, да в лужу? Речь шла не о какой-то там говносистемке типов как в Ц++ и даже не о SystemF, а о CoC - типизированном лямбда-исчислении высшего порядка, мать его за ногу. И в нем можно формально доказать, что никаких переполнений не будет.

Угу, но вот только:

1. Переполнений может и не будет, но будет какая-то другая херня, отсутствие которой ты _забыл доказать_. И нет никакого способа проверить - а доказал ли ты отсутствие всех классов багов или какой-то класс в каком-то месте оказался доказательством не покрыт.

2. Нет способа проверить правильность твоего доказательства. Это задача алгоритмически неразрешимая. Ты, конечно, можешь попытаться доказать, что доказательство верно. Но кто докажет, что верно это твое последнее доказательство? Никто. Т.о. наличие доказательства отсутствия ошибок не гарантирует, собственно, 100% отсутствия ошибок.

3. Нельзя доказать, что «программа работает», т.к. это понятие нельзя формально выразить. Можно доказать, что работа программы соответствует спецификации, но кто тебе гарантирует, что спецификация корректна (те самые «в спецификации забыли указать, что переполнений быть не должно» - как раз близки к этой теме) или хотя бы непротиворечива? Ответ: никто и никогда, это невозможно.

4. Реальная программа работает в реальном мире на реальном железе, спецификации которых во втором случае возможно, а в первом - обязательно - неполны и некорректны.

5. В итоге даже при наличии полного доказательства надежность таких систем гарантируется в бОльшей степени более надежными методами тестирования. Доказательства же - это так, поиграться. Чисто бонус.

Вывод отсюда простой: есть смысл доказывать корректность отдельных алгоритмов (ну типа - квиксорт действительно сортирует) или отсутствие отдельных классов багов (например отсутствие сегфолтов), но полная формальная верификация - это не более чем мокрые мечты анонимных аналитиков.

> Только в мечтах. На практике, ты никогда не сможешь обеспечить 100% покрытие.

А зачем нам 100% покрытие? во-первых, 100% покрытие не гарантирует того, что программа будет работать, во-вторых - никакого покрытия ошибок типов вообще _ не надо_. апологеты статики никак не могут понять одной простой вещи - ошибки типов имеют такой характер, что программа с подобными ошибками чуть менее чем всегда валится на первом же тесте логики. Когда же тестов логики _много_, то вероятность наличия ошибки типов настолько меньше вероятности наличия непокрытой тестами ошибки логики, что ей просто можно пренебречь. В самом деле - ну кому нужно отлаживать программу на предмет ошибок типов, если вероятность того, что там ошибка типов - 0.01%, а вероятность того, что там ошибка логики - 1%?

Если свести твое утверждение в область электроники

То мы получим некорректную аналогию. Некорректные аналогии - единственный метод ведения дискуссии у хаскианалитиков. Ну вот хотя бы:

в) что вместо того чтобы ломать голову почему я не могу воткнуть разъем типа A в разъем типа B, намного проще подключить как есть, подать питание, и тогда выгоревшее место на плате явно укажет на совершенную ошибку.

Переформулируем так:

вместо того чтобы ломать голову почему я не могу воткнуть разъем типа A в разъем типа B, намного проще подключить как есть, подать питание, и тогда загоревшаяся лампочка на тестовом стенде явно укажет на совершенную ошибку.

И уже никакого абсурда, не правда ли?

На том, что производная собственного ЧСВ станет положительной, уже говорили?

> То мы получим некорректную аналогию. Некорректные аналогии - единственный метод ведения дискуссии у хаскианалитиков.

Аналогии — это вообще единственный метод ведения дискуссии у тех, кто не разбирается в теме. Корректность или некорректность аналогий тут совершенно не при чем. Так что лучше завязывай с ними.

И, кстати, кто такие хаскианалитики?

Тащемта, наоборот, сильно отрицательной.

Ну, для меня, например, одна из сильных сторон статической типизации — это высокая выразительность типов объявленных функций. Так, например, при первом взгляде на тип функции можно уже много сказать о ее поведении. Можно сразу увидеть, какими инвариантами функция обладает. Порой однострочный тип функции говорит о ней больше, чем ее словесное описание в пару абзацев.

Еще типы дают неплохой профит при продумывании архитектуры программы. Можно легко заниматься проектированием сверху вниз, продумывая первым делом типы, а потом уже потихоньку дописывая необходимый код.

Ну и юнит-тесты, конечно же, писать для хацкельных библиотек гораздо проще, чем для питоновых, например.

> Вот именно что - быстро прогнать тест и обнаружить ошибку, вместо того, чтобы разбираться чего там нагородил тайпчекер.

Откуда эта навязчивая мысль, что тайпчекер обязательно покажет ошибку не в том месте, а рантайм в том? Ну бред же. И рантайм, и тайпчекер порой ошибки показывают не в тех местах, но обычно еггог вылезает и в том, и в дргом случае в непосредственной близости.

> Так что лучше завязывай с ними.

А я с ними и не начинал.

> Ну, для меня, например, одна из сильных сторон статической типизации — это высокая выразительность типов объявленных функций. Так, например, при первом взгляде на тип функции можно уже много сказать о ее поведении. Можно сразу увидеть, какими инвариантами функция обладает. Порой однострочный тип функции говорит о ней больше, чем ее словесное описание в пару абзацев.

Но только для этого статическая типизация _не нужна_, никто тебе не мешает использовать вместо типов те же контракты, которые по выразительности соответствуют CoC, до которого всяким хаскилям как до китая раком.

> Откуда эта навязчивая мысль, что тайпчекер обязательно покажет ошибку не в том месте, а рантайм в том? Ну бред же. И рантайм, и тайпчекер порой ошибки показывают не в тех местах, но обычно еггог вылезает и в том, и в дргом случае в непосредственной близости.

Ну вообще да - и рантайм и чекер показывают ошибку ровно в том месте, где оказались нарушены типы, проблема в том, что:

1. Рантайм проверки могут быть насколько угодно точными, ими можно выразить то, что статическая система типов не выразит (без зависимых типов), по-этому позиционирование в этих случаях сколь угодно точное (при желании можно гарантировать, что ошибка будет всегда показана в месте возникновения).

2. Тайпинференс. При массивном использовании тайпинференса компилятор за счет варьирования типов может перенести ошибку как угодно далеко от места ее реального возникновения. Именно по-этому, кстати, хорошим стилем является использование только локального тайпинференса, а за глобальный в приличных местах пробивают с ноги. И именно по-этому полного тайпинференса никогда не будет в мейнстримных языках. Это просто игрушка.

>контракты, которые по выразительности соответствуют CoC

Идиот и не лечится. И как только потратил время на ничтожество, не способное отличить рантайм-костыли от системы типов.

Контрактиками своими ты даже зависимые типы не перекроешь, а про CoC даже не заикайся. Ты бы хоть для приличия упомянул публике, что все дилды в рантайме предлагаешь ловить, это же дети могут читать...

Хочешь конернтики?

Хоршо. Тип (Monad m) => m a определяет два независимых логических слоя в программе. Слой «m» и слой «a». return — переход а -> m, (<$>) — переход m -> a, (<*>) — производит вычисления в слое a на уровне слоя m, (>>), (>>=) — вычисления в m, ($) - вычисления в a.

Для чего такой подход нужен, я надеюсь сам догадаешься.

Типы, прежде всего, — инструмент проектирования. А потом — все остальное.

>Ну вообще да - и рантайм и чекер показывают ошибку ровно в том месте,

Если типы примитивные — да. А если нет? :)

>> Не могу. Считаем, что здесь динамическая и статическая типизация сыграли вничью, и этот пример просто ничего не доказывает.

Что-то быстро слился хачкель-фанбой.

Я не пользуюсь Хаскелем, знаю о нем довольно мало и вообще к нему равнодушен.

Видать не знает чушка

ПНХ.

> статическая типизация как панацея ото всех бед в рантайме - это тоже расхожее клише.

...придуманное противниками статической типизации %)

>Кроме того, ты опять все сводишь к некой сферической «проверке правильности», причем в какой-то совершенно непонятной интерпретации. Если свести твое утверждение в область электроники, то ты утверждаешь а) что разные виды разъемов не нужны, б) что поскольку тип раъема и зараенее описанный электирческий интерейс не могут гарантировать правильность передаваймых сигналов — они не нужны. Поэтому все провода должны быть одинакового цвета и толщины, а если есть сомнения, то на плате все написано, в) что вместо того чтобы ломать голову почему я не могу воткнуть разъем типа A в разъем типа B, намного проще подключить как есть, подать питание, и тогда выгоревшее место на плате явно укажет на совершенную ошибку.

спасибо, записал в цитатничек

Сложилось впечатление, что ты считаешь, что прохождение тестов, проверяющих поведение программы, гарантирует корректную работу программы. Это не так. Тесты не могут такого гарантировать, разве что их будет очень много, где-то так пару миллиардов.

Сравни сколько времени затрачивается на прохождение всех тестов тесты и сколько на вывод типов. А теперь представь, что после обнаружения ошибки компилятором юнит-тест не проводится.

> Контрактиками своими ты даже зависимые типы не перекроешь, а про CoC даже не заикайся.

Контракты проверяются в рантайме, по-этому там может быть любой предикат, так что по выразительности они соответствуют CoC. А строго говоря, выше CoC - многие программные сущности, которые могут быть использованы в контрактах, в CoC не выразишь, в CoC вообще много чего нет.

И как только потратил время на ничтожество, не способное отличить рантайм-костыли от системы типов.

А где я писал, что контракты проверяются в компайл-тайме? Тут же выбор простой - либо используем костыль в компайл-тайме, который не дает никаких гарантий, либо используем развитую систему типов в рантайме с обширными возможностями, которая дает полные гарантии отслеживания, классификации и корректной обработки ошибок. Первое неплохо для написания диссеров, второе - для реального программирования систем, которые должны быть защищены от ошибок.

> Хоршо. Тип (Monad m) => m a определяет два независимых логических слоя в программе. Слой «m» и слой «a». return — переход а -> m, (<$>) — переход m -> a, (<*>) — производит вычисления в слое a на уровне слоя m, (>>), (>>=) — вычисления в m, ($) - вычисления в a.

Замечательно, но это не имеет никакого отношения к типам, т.к.

1. Монады можно спокойно реализовать и в динамическом ЯП.

2. Это не более чем хаскикостыли - в дизайне хаскеля есть несколько критичных недостатков, которые попытались решить при помощи монад. в других ЯП недостатков хаскеля нет, и монады там не нужны. Гордое решение средствами ЯП проблем, которые этот же ЯП и создает, на пример пользы этих средств никак не тянет.

3. Вообще в нормальном языке монада - это просто переопределенная аппликация, только хаскидебилы навернули вокруг кучу ненужного теорката, типов и прочего говна, в результате чего уже сами не видят леса за деревьями.

Для чего такой подход нужен, я надеюсь сам догадаешься.

Ну чего же ты? Сказал а - говори б. Для чего он нужен?

Типы, прежде всего, — инструмент проектирования.

Ну проектируй с типами в любом динамическом ЯП, тебе никто не запрещает. Еще можешь использовать вместо типов контракты - будет куда выразительнее. Так что контракты как средство проектирования смотрятся на порядок удобнее.

> Если типы примитивные — да. А если нет? :)

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

> Сложилось впечатление, что ты считаешь, что прохождение тестов, проверяющих поведение программы, гарантирует корректную работу программы. Это не так. Тесты не могут такого гарантировать, разве что их будет очень много, где-то так пару миллиардов.

А гарантировать корректную работу программы вообще нельзя, я выше уже объяснял почему. Даже соответствие работы программы спецификациям и то нельзя гарантировать. А еще ньюанс - никто не гарантирует, что ты верно перевел спецификации на «язык типов». Грубо говоря - сам код программ это и есть перевод спецификации на некоторый ЯП, если ты пытаешься выразить _всю_ спецификация в типах, то вероятность посадить ошибку так же вероятна, как вероятность посадить ошибку в коде (потому что написание типов и написание кода в данном случае по сути одно и то же). Т.о. еще возникает вопрос - а соответствуют ли твои типы спецификации? И задача проверки такого соответствия изоморфна задаче отладки программы. Именно по-этому имеет смысл покрывать типами лишь некоторое подмножество спецификации.

Тесты не могут такого гарантировать, разве что их будет очень много, где-то так пару миллиардов.

Тесты гарантируют, что программа «наверное работает правильно». Ничего _более_ этого гарантировать нельзя вообще, никаким способом. По-этому всегда и везде вердикт о корректности программы выносится именно после тестирования (даже если корректность уже была доказана формальными методами). Формальное доказательство не может заменить и не заменит никогда тестирования, оно лишь придает нам больше уверенности, но является по сути добавочным к тестированию. И нужно оно только в том случае, когда нам надо не «наверное работающую программу» а «очень наверное работающую программу», что реально бывает чрезвычайно редко (почти всегда это «очень» просто не окупится).

Тут еще один момент - трудно представить себе схему, которая будет корректно работать, если мы перепутаем разъемы, то есть тут введение «типизации» нас не ограничивает. С другой стороны, тайпчекер работает так, что отвергает любую программу, _корректность_ которой не может доказать. А из всех корректных программ он может доказать корректность лишь очень узкого подмножества. Все остальные корректные программы им будут отвергнуты. Несмотря на то, что они корректны, ага.

>Монады можно спокойно реализовать и в динамическом ЯП.

Можно. Но пользоваться нельзя.

Это не более чем хаскикостыли

Какие, нахрен костыли?

это просто переопределенная аппликация

Ну, дык. Ясен пень, что монада — аппликативный функтор.

навернули вокруг кучу ненужного теорката

Заметь, не слова о теоркате.

Для чего он нужен?

На уровень m выносятся самые фундаментальные/абстрактные/общие (нужное подчеркнуть) вычисления. На уровень a — наоборот. Теория типов гарантирует, что уровни не пересекутся. Плюс m зависит от a, в смысле m a и m b — разные типы.

Еще можешь использовать вместо типов контракты

О! С бледже^W Карри-Говардом? Есть такие реализации? Где?

> Можно. Но пользоваться нельзя.

Почему же нельзя, если можно?

Какие, нахрен костыли?

Если бы не ИО, не было бы в хаскеле вообще никаких монад.

Ну, дык. Ясен пень, что монада — аппликативный функтор.

нет, переопределение аппликации к аппликативному функтору свести нельзя, там нужен именно bind.

На уровень m выносятся самые фундаментальные/абстрактные/общие (нужное подчеркнуть) вычисления. На уровень a — наоборот.

Например - какие вычисления выносятся на уровень а и какие на уровень m?

Теория типов гарантирует, что уровни не пересекутся.

Я более чем уверен, что это же можно гарантировать и без теории типов, осталось только узнать что именно подразумевается под этим «уровни не пересекутся».

О! С бледже^W Карри-Говардом?

Что под этим подразумевается?

> Плюс m зависит от a, в смысле m a и m b — разные типы.

А я хочу, чтобы они были одним типом. Нет, в хаскиле так нельзя? Спасибо, ваша система типов говно. Когда в ней хотя бы такие вот тривиальные вещи можно будет выразить - тогда и позовете.

Посмотрел бы я как ты для атомной станции юнит-тестики писать собрался.

атомная станция - это аппартно-программный комплекс, а ты туп

>> Посмотрел бы я как ты для атомной станции юнит-тестики писать собрался.

атомная станция - это аппартно-программный комплекс

Ты хочешь сказать, что для аппаратно-программного комплекса unit-тесты написать нельзя?

>Если бы не ИО

Ужас. Кругом мифы. Констукции из Control.Monad — попытка генерализации вычисления, сферического и в вакууме. Есть еще Control.Arrow, и внезапно, Control.Category. Служат примерно для тех же вещей.

IO — монадический интерфейс к хаскелевскому вводу-выводу, и вся его «магия» происходит не из сущности монад, а из сущности хаскелевского IO, в котором действительно полно костылей, как я слышал.

нет, переопределение аппликации к аппликативному функтору свести нельзя, там нужен именно bind.

А ты в курсе что функция f : a -> b — монада? Мой самый любимый пример на хаскеле (пока) f = (:) =<< length
Красиво и ненапряжно. Правда мозги слегка греются, пока сообразишь почему это работает. Так, что можно и свести... :P

Что под этим подразумевается?

Эти хреновины для описания контрактов, они сделаны через изоморфизм Карри-Говарда? Или может быть там есть возможность строить обычные логические высказывания, без Изоморфизма?

>А я хочу, чтобы они были одним типом.

Ты про зависимые (от значений) типы? Иш чего захотел...

Юзай Coq, Agda тогда, или вообще Epigram.

Или может тебе лямбда-куба уже мало?

> IO — монадический интерфейс к хаскелевскому вводу-выводу, и вся его «магия» происходит не из сущности монад, а из сущности хаскелевского IO

Я в курсе. Но факт есть факт - если бы в хаскиле был нормальной ИО (не монадический), то на практике монадами бы пользовались примерно столько же, сколько пользуются упомянутыми тобой стрелками и категориями. То есть нихрена, реально.

А ты в курсе что функция f : a -> b — монада?

Монада (в хаскиле) - это тройка из типа с кондом *->*, bind и return. Какой у нас тип и bind с return для твой функции?

Эти хреновины для описания контрактов, они сделаны через изоморфизм Карри-Говарда? Или может быть там есть возможность строить обычные логические высказывания, без Изоморфизма?

Что значит «сделаны через изоморфизм Карри-Говарда»? Что значит «строить обычные логические высказывания без изоморфизма»? И при чем тут вообще логические высказывания? Контракт - это предикат на входах/выходах ф-и. Ну и внешнем состоянии (если речь о каких-то сложных контрактах типо темпоральных, например).

> Юзай Coq, Agda тогда, или вообще Epigram.

Нет, спасибо, лучше контрактов навешаю. Выразительность выше, зато никакого анального рабства у тайпчекера.

Выбирай C++ и не сношай себе и окруюащим мозги.

Какой у нас тип и bind с return для твой функции?

Тебе исходники base влом открыть? Ах да, ты же не разрабатываешь программы на хаскеле. Ты его только обсираешь.

instance Functor ((->) r) where
        fmap = (.)

instance Monad ((->) r) where
        return = const
        f >>= k = \ r -> k (f r) r

И отвечая на твой вопрос: bind - функциональная композиция, return — const.

Контракт - это предикат на входах/выходах ф-и.

Ну, предикат это и есть логическое высказывание.

>Нет, спасибо, лучше контрактов навешаю.

Дык ты определись чего хочешь-то? Хочешь зависимых (от значений) типов — добро пожаловать к тайпчекеру.

А если не хочешь — не кати на хаскель в котором зависимых (от значений) типов нет.

> Тебе исходники base влом открыть?

Вот это, значит мне надо лезть в какие-то неизвестные исходники и искать в них не-знаю-что («монада функции f»)? Замечательное предложение.

instance Functor ((->) r)

А, так это для -> монада. Ну так бы сразу и говорил. Только она не совсем честная. Но ты вкурсе, да?

Ну, предикат это и есть логическое высказывание.

Угу. Но-таки зачем тебе понадобился изоморфизм Карри-Говарда? Контракты-то не в компайлтайме, они пишутся на самом ЯП. Так что никаких костылей тут не надо.

> добро пожаловать к тайпчекеру

Зачем?

А если не хочешь — не кати на хаскель в котором зависимых (от значений) типов нет.

Ну тут речь о чем - с одной стороны система типов хаскеля бедна и примитивна (стыдно сказать - для нее даже существует алгоритм тайпинферренса!), ничего интересного в ней не выразить, никаких толковых гарантий не получить. С другой стороны она достаточно упорота, чтобы обеспечить йоплю с тайпчекером. Другими слвоами - она пролетает везде, по всем пунктам. там недо-, тут пере-.