LINUX.ORG.RU

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


0

5

Я догадываюсь, что это какая-то паранойа !!! Но как !?

Конечно очевидный вариант - попробовать все. И подумать.

Пробую... Думаю... А дальше что ???

OCamL похож на F#, красив и удобен... хорошо. Применять можно везде, к web имеет много забавных наработок.

Erlang имеет достаточно мощную, стабильную виртуальную машину и синтаксис очень забавный ! Интересный web server yaws и NoSQL DBMS.

Haskell выигрывает по полярности и там есть много действительно хороших библиотек вообще в любой сфере...

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


Ответ на: комментарий от tailgunner

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

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

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

я хочу сказать, что для аппаратно-программного комплекса надо сначала определить что подразумевается под словом «модульное тестирование», в общем случае так писать - не очень грамотно

shty ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

Ну так можно вообще assert-том обойтись (+ какой-то сахар над ним же).

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

стыдно сказать - для нее даже существует алгоритм тайпинферренса!

Вообще-то, он уже undecidable (в GHC) - можно осуществлять тьюринг-полные вычисления в type-level. И там не SystemF, а SystemFC (разные вещи), а в JHC так вообще Lambda Cube + Pure Type System.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Как-то не похоже что их мало используют без IO.

Чем непохоже? Монады к языку изначально прибиты гвоздями - их используют. В других языках не прибиты - их не используют (хотя могут). Вывод очевиден, нет? Если бы вместо монад прибили стрелки - использовали бы все в хаскиле стрелки. вот и все.

Ну так можно вообще assert-том обойтись (+ какой-то сахар над ним же).

Ну да, а можно обойтись и обычным if-ом (сахаром над которым и является контракт).

anonymous ()
Ответ на: комментарий от quasimoto

> Вообще-то, он уже undecidable (в GHC) - можно осуществлять тьюринг-полные вычисления в type-level.

Ну скажем так «алгоритма не существует» и «алгоритм может повиснуть» - две принципиально разные вещи. Во втором случае алгоритм по факту _есть_, при чем универсальный.

а SystemFC (разные вещи)

Там совершенно несущественные с формальной точки зрения дополнения.

а в JHC так вообще

А в чем оно там сильнее SystemF?

anonymous ()
Ответ на: комментарий от anonymous

Монады к языку изначально прибиты гвоздями - их используют.

Не монады (или там стрелки с функторами) прибиты, а классы типов как средство строить общий интерфейс к разным сущностям. Вот есть такое естественное для хаскеля средство - его и используют. Также как в С++ используют перегрузку (аналог ad-hoc полиморфизма) и шаблоны (аналог параметрического полиморфизма) как естесвенные для С++ средства достижения той же цели. Ну или как методы и макросы в Common Lisp.

В других языках не прибиты - их не используют (хотя могут).

Точнее, используют то, что есть - нечто, что позволяет строить общий интерфейс. Особенности классов типов в хаскеле продиктованны особенностями его системы типов, так что можно о них забыть и продолжать спорить о том что лучше - well typed (в чём-то) языки или ill typed. С тем что и те и другие должны быть строгими, я думаю, все согласятся.

Ну да, а можно обойтись и обычным if-ом

и.е. верификация в рантайме.

Ну скажем так «алгоритма не существует» и «алгоритм может повиснуть» - две принципиально разные вещи. Во втором случае алгоритм по факту _есть_, при чем универсальный.

Можно ли построить разрещающий алгоритм который за конечное время ответит на вопрос «эта программа хорошо типизирована или нет?» - для языка GHC нельзя.

Там совершенно несущественные с формальной точки зрения дополнения.

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

А в чем оно там сильнее SystemF?

Там просто core language - настоящий лямбда куб со специальной PTS (т.е. не SystemFC как у GHC), а хаскель - front-end язык. Можно поставить вопрос о языке который будет так же как хаскель стараться соблюдать баланс между мощностью системы типов и простотой написания програм и иметь более мощную систему типов (с нормальными типо-термами), но такого пока не придумали - что-то вроде агды язык не повернётся назвать ЯП общего назначения.

quasimoto ★★★★ ()
Ответ на: комментарий от AIv

> Никогда не задумывались, почему смешение RGB дает произвольный цвет видимого спектра? Как это так выходит - сложили три фотона с разными длинами волн и получили что то среднее?

Да, кстати, а почему так происходит? Можно какую-нить ссылку про это дело кинуть?

P.S. Вопрос давно интересует, но систематическими поисками ответа не занимался :-)

Sahas ★★★★★ ()
Ответ на: комментарий от quasimoto

> Не монады (или там стрелки с функторами) прибиты, а классы типов как средство строить общий интерфейс к разным сущностям.

Нет, вот именно что прибиты именно _монады. Были бы прибиты стрелки - юзали бы все стрелки. Но прибили монады. Потому что ИО (в первую очередь). В языках, в которых монады не прибиты, монады никто и не использует. Потому что они никакого профита не дают. У Маклейна во вступлении, по-моему, как раз все написано по этому поводу.

Вот есть такое естественное для хаскеля средство - его и используют.

В том и дело, что _не_ естественное. Есть ИО. Его сделали через монады (это факты). Но не делать же через монады _только_ ИО? Решили при помощи кривых костылей сделать через монады еще что-нибудь. Чтобы ИО не смотрелось чересчур убого. Ну а кто-то потом в монадах решил найти глубокий смысл. Глубокий смысл в чем угодно найдут - СПГС же.

Также как в С++ используют перегрузку (аналог ad-hoc полиморфизма) и шаблоны (аналог параметрического полиморфизма) как естесвенные для С++ средства достижения той же цели. Ну или как методы и макросы в Common Lisp.

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

Точнее, используют то, что есть - нечто, что позволяет строить общий интерфейс.

Ну вот именно. Нормальные языки используют то, что подходит (что позволяет строить наиболее удобный общий интерфейс в данном случае), а хаскидебилы повсюду суют монады, потому что это МОНАДЫ, потому что они прибиты к языку. Суть то в чем - в других языках монады можно использовать с тем же успехом, что и в хаскиле. Но никто не использует (за реально редким исключением). Почему? Ответ прост - монады к языку не прибиты. А когда они к языку не прибиты - то нахер не нужны, есть более удобные средства. Если бы монады были _реально_ полезны, то их бы и в других языках использовали (благо концепция тривиальна. Но не используют.

anonymous ()
Ответ на: комментарий от quasimoto

> С тем что и те и другие должны быть строгими, я думаю, все согласятся.

Имеется ввиду строгая статическая/динамическая типизации? Тогда да, конечно.

и.е. верификация в рантайме.

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

Можно ли построить разрещающий алгоритм который за конечное время ответит на вопрос «эта программа хорошо типизирована или нет?» - для языка GHC нельзя.

Еще раз повторяю, «алгоритм есть, но он иногда виснет» и «алгоритма никто не придумал В ПРИНЦИПЕ» - это существенно разные вещи. С формальной точки зрения да - разница, вроде, неощутима. На практике - ощутима вполне. Ну это как «мы написали программу, она решает вашу задачу, но виснет на некоторых входах, потому что эти входы не имеют смысла» и «у нас никакой программы нет, но мы зуб даем - даже если напишем, программа на некоторых входах будет виснуть». Чувствуется разница?

Там ряд костылей, которые в GHC сделаны так, что позволяют писать отображения из типа в тип и из типа в терм (ну и GADTs).

Из типа в терм у нас и так есть (лямбда-стрелка), ну а омега это понятно, но это реально на практике почти ничего не добавляет.

Там просто core language - настоящий лямбда куб со специальной PTS (т.е. не SystemFC как у GHC), а хаскель - front-end язык.

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

> Языки с захардкоженой системой типов - прошлый век. Система типов должна быть «гибкой» (типа - в этом модулей нам верификация не нужна - у нас динамика, тут - обычная лямбда-стрелка, здесь - используем зависимые типы, а потом объединяем все модули в одной программе). Соответственно единственный выход - ЯП должен быть строго динамическим, чекеры внешними.

А есть уже такие языки? Так сказать, «языки нашего века»?

tailgunner ★★★★★ ()
Ответ на: комментарий от anonymous

Нет, вот именно что прибиты именно _монады.

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

И вот таких концептов в хаскеле множество - Functor для отображений сохраняющих структуру ADT, Traversable для обходов разных (возможно рекурсивных) ADT, Foldable для их свёртки, Monoid для моноидальных ADT, ну и так далее (Functor => Pointed => Applicative => Monad => ..., Category => Arrow => ...). Что-то вроде паттернов в ООП (есть даже прямые аналогии).

Ну а теперь Monad - монадический интерфейс. Вот тип «список», монадическим интерфейсом для него будет list comprehensions, для типа «множество» - set comprehensions (те самые, что в теории множеств используются), тип «парсер комбинатор» - комбинаторы позволяющие построить сложный парсер который будет способен разобрать, в том числе, контекстно-зависимые языки. Если строить к парсерам аппликативный интерфейс, то будет возможно разбирать только контекстно-свободные языки - но есть выбор какой интерфейс использовать.

Вы же не против построения монадного интерфейса ко всем этим ADT?

Теперь (IO a) - это такой волшебный тип, в том смысле, что если мы имеем функцию (f :: ... -> a), то мы знаем, что f _всегда_ будет возвращать значение _именно_ типа `a' и всегда одно и то же для одних и тех же аргуметов этой функции, но если имеем (g :: ... -> IO a), то это может быть `a', а может быть и что-то другое, и, возможно, не всегда одно и то же (пользователь ввёл невалидные данные, или тред записал в общую переменную что-то новое). Короче IO обворачивает всё что не укладывается в детерменированную (ссылочно-прозрачную) логику.

Ну и реализация монадического интерфейса к IO позволяет выполнять такие «плохие» (с точки зрения чистоты системы типов и математического смысла слова «функция») вычисления последовательно.

Вы против разделения pure кода (outside IO) и unpure кода (inside)?

Или против того, что к этому ADT тоже написан монадический интерфейс?

Были бы прибиты стрелки - юзали бы все стрелки.

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

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

В более слабых языках - да. В более сильных - монады остаются на месте.

В том и дело, что _не_ естественное. Есть ИО. Его сделали через монады (это факты).

Опять не то (про что я в этом посте выше писал) - IO он сам по себе, это странный ADT такой (без доступа к конструкторам/аккессорам), и к нему уже потом построен монадический интерфейс (равно как и функторный/точечный/аппликативный).

Решили при помощи кривых костылей сделать через монады еще что-нибудь.

Ага, list и set comprehensions, парсеры и принтеры - что-нибудь :)

Глубокий смысл в чем угодно найдут - СПГС же.

ИМХО, тут больше дело в том как кто-то, исходя из своего «мировозрения», отвечает на три вопроса которые я выше задал.

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

А я про монады не говорю, я вообще про классы типов - безусловно аналог перегрузки. Шаблоны - аналог параметрического полиморфизма. Ну а макросы, в контексе этого разговора, это костыль который позволяет создать видимость параметрического полиморфизма если того в языке нет.

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

Суть то в чем - в других языках монады можно использовать с тем же успехом, что и в хаскиле. Но никто не использует (за реально редким исключением). Почему? Ответ прост - монады к языку не прибиты. А когда они к языку не прибиты - то нахер не нужны, есть более удобные средства. Если бы монады были _реально_ полезны, то их бы и в других языках использовали (благо концепция тривиальна. Но не используют.

Есть такое дело, связано с понятием ЯОВУ (язык очень высокого уровня). Языки которые возникают в прикладном программировании можно расположить в таком порядке повышения «уровня» (кавычки - это не серьёзно, если что):

  1. Только значения.
  2. + функции.
  3. + функции котрые значения (first class functions - lambdas, HOFs, closures).
  4. + типы.
  5. + параметрические типы.
  6. + типы которые значения (first class types).
  7. + какой-то логический фреймворк (axioms, theorems, tactics).

Так вот, до уровня (5) выговорить что-то вроде

foo :: {m :: Bar} -> m (m a) -> m a

нельзя - язык типов слишком бедный (если он есть).

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

Ну а если в языке ещё duck typing то сами ADT-обвёртки вроде Maybe или Either теряют смысл - там где в хаскеле будет

path :: Env -> [Env -> Maybe Env] -> Maybe Env
path e = foldl' (>>=) (Just e)

(т.е. используем общий интерфейс - не пишем кучу case-ов) где-нибудь в лиспе будет просто последовательность аппликаций, не нужно заворачивать/разворачивать/спасать типы, всегда можно примешать к (предполагаемому) типу `a' тип `b' получив (or a b), который всё равно субтип универсального `t' - ну что можно в таком бедном языке выразить? :)

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

Про JHC - http://repetae.net/computer/jhc/jhc.shtml, но там не все идеи ещё реализованы (вроде вывода регионов и устранения GC). Ну и комментарии в src/E/Type.hs и src/E/TypeCheck.hs - собственно классы типов там реализованы штатно вокруг типов этого E.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

Нет, речь шла о монадах, а не о тайпклассах. Суть такова - ИО в хаскеле кривой, ИО сделан через монады. Тайпклассы — _ортогональны_ монадам. они с монадами никак не связаны. В хаскеле могло быть какое-нибудь другое средство для выражения монад (вместо тайпклассов) это бы ничего не изменило. Так что надо говорить именно о монадах, а не о тайпклассах. Вообще, какая связь между тайпклассами и монадами? Очевидно никакой. Так что не надо подменять понятия.

Вот тип «список», монадическим интерфейсом для него будет list comprehensions

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

Вы против разделения pure кода (outside IO) и unpure кода (inside)?

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

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

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

anonymous ()
Ответ на: комментарий от quasimoto

> В более слабых языках - да. В более сильных - монады остаются на месте.

Это все софистика. Вы говорите - использование монад имеет смысл. я говорю - не имеет. Я привожу в пример факт - есть множество языков (щарп, джава, плюсы, руби, питон, лиспы - это навскидку) где монады легко делаются, но их там никто не использует. Внимание, вопрос: почему? Следуя вашей логике, использовать должны. Мой ответ - монады к этим языкам не прибиты, а потому и нахер там не нужны, вот и не используют. Ваш ответ?

Опять не то (про что я в этом посте выше писал) - IO он сам по себе, это странный ADT такой (без доступа к конструкторам/аккессорам), и к нему уже потом построен монадический интерфейс (равно как и функторный/точечный/аппликативный).

Да вы поймите, что не сам по себе. Думали, думали, как сделать ИО - и решили - а сделаем через монады. Но чтобы монады не выглядели кривым костылем (точнее _слишком_ кривым костылем, просто кривым костылем они для любого адекватного человека все ранво выглядят) настрогали других (не ИО) монад. Тот же список или maybe. От которых толку нет, котоыре реально не нужны иникакого профита не приносят - единственный смысл существования этих монад оттенять ИО. Типа не только ИО единым. И вот вы прекрасный пример того, как люди ведутся на эту уловку, которая прикрывает дыры дизайна. То есть монады - они вслед за ИО пошли, именно так, а не наоборот. Не было бы ИО - не было бы монад. То есть, они были бы - но так же как стрелки. То есть лежат в какой-то там библиотеке и их никто не трогает, разве что just for lulz.

Ага, list и set comprehensions, парсеры и принтеры - что-нибудь :)

Так ведь видите в чем дело - list и set comprehensions, парсеры и принтеры - реализованы _без_ монад и ортогональны монадам :) Это уже _после_ того как они реализованы просто взяли и притянули за уши - а пусть у нас тот же список монадой будет! Это никому не надо, естественно, никакой пользы такая штука (считать список монадой) не дает. Но дыру в дизайне прикрывает.

ИМХО, тут больше дело в том как кто-то, исходя из своего «мировозрения», отвечает на три вопроса которые я выше задал.

Это какие вопросы?

А я про монады не говорю

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

> Ну макросы не имеют никакого отношения к параметрическому полиморфизму.

Точнее имеют, но только в том смысле, что параметрический полиморфизм элементарно реализуется на макросах. То есть если в вашем ЯП есть макросы и ваш ЯП поддерживает лямбда-стрелку, то он искаробки. А если не искаробки - то он поддерживает вообще весь лямбда-куб. Короче говоря - параметрический полиморфизм - это просто костыль для тех языков, в которых нету макросов. Конечно, он хорошо если 1% юзкейзов макросов покрывает, но это важный 1% :)

anonymous ()
Ответ на: комментарий от quasimoto

> Языки которые возникают в прикладном программировании можно расположить в таком порядке повышения «уровня»

Неверно. Все динамические языки по определению более высокоуровневы, чем статические :)

нельзя - язык типов слишком бедный (если он есть).

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

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

А его и не надо «очерчивать». «очерчивать» - это все низкий уровень, на высоком уровне мы используем и все. Очертит за нас компилятор :)

не нужно заворачивать/разворачивать/спасать типы, всегда можно примешать к (предполагаемому) типу `a' тип `b' получив (or a b)

Ага, вот тем высокоуровневый язык от низкоуровневого и отличается - вот этой вот ручной работы делать не надо :)

ну что можно в таком бедном языке выразить? :)

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

anonymous ()
Ответ на: комментарий от quasimoto

Экхм, я ожидал ссылки на статью с формальным описанием системы типов, а не ссылки на какие-то комменты где-то, да еще и не рабочие. Гм. У них что, нету спеки для системы типов? Что за бред? Ну тогда это просто студенческая поделка и никакой ценности не представляет не понимаю, какой смысл приводить ее в пример.

anonymous ()
Ответ на: комментарий от Macil

> Так это же Lovesan :)

Нет. Лавсан бы сказал, что языки с захардкоженной семантикой и синтаксисом - прошлый век ;)

anonymous ()
Ответ на: комментарий от anonymous

Суть такова - ИО в хаскеле кривой, ИО сделан через монады.

IO реализован в _рантайме_, а не в _языке_. Со стороны языка есть тип IO и примитивные функции с ним, которые в языке не выражаются (а тянутся к рантайму). Далее в _языке_ есть средство «классы типов» с помощью которого (средствами языка!) определён общий монадический интерфейс и его реализация (опять - средствами языка!) для того типа IO. Короче IO живёт в рантайме, а монады - целиком в языке. Так как IO может быть «сделан через монады»? Это просто неправда. То же самое, что утверждать, что из-за наличия list comprehension тип list «сделан через монады» - эти list comprehension можно делать с помощью родных списочных функций (map, append, concat и т.п.), а можно построить монадический интерфейс и использовать его. Точно также IO можно было бы использовать с помощью родных примитивов, но, во-первых, можно написать instance Monad IO where (и тут выражаем методы через примитивы) и он будет удовлетворять всем законам, и, во-вторых, монадный интерфейс удобнее (тем более с do). Так почему бы так не сделать?

Вообще, какая связь между тайпклассами и монадами?

Если её нет, то я не понимаю тогда о каких «монадах» идёт речь. Если бы вы ткнули носом в тупые костыли именно в какой-нибудь реализации, тогда, может быть, было бы понятнее (типа - вот IO в рантайме, вот типы класов в языке, инстансы, а вот тут пошёл какой-то бред).

Другими словами - есть у нас объект А. Мы говорим «А - монада». Можем ли мы что-то полезное сделать с А? Нет.

Ага, т.е. если объект у нас инстанс Show, то мы можем с ним сделать полезную операцию (отобразить в строку) без оглядки на суть A. То же самое про Binary (сериализация), Traversable (обход) и т.п. - полезные типы классов. Т.е. вам не понятно в чём общая суть именно Monad? В чём вообще польза? Если говорить в общем, то это то, о чём Macil говорил - если к A построен правильный монадический интерфейс, то мы можем разделять вычисления на два логических слоя inside A и outside A, в случае с IO - inside IO и outside IO (тут разница только в том, что перемешать эти слои нельзя, нету run IO).

В хаскеле вообще нету unpure кода

Ну, внутри IO у меня unpure код, т.к. я не могу гарантировать типо-безопасность и ссылочную прозрачность. Если я вытащу значения из IO (с помощью unsafe* функций) то эта проблема распостранится на весь остальной код (GHC может просто упасть в кору).

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

Офигеть, и как же все прикладные программы тогда работают?)

Второе - бывают чисто функциональные языки и без монад (тот же Clean).

А какая там система типов?

Ну в самом деле, я же не виноват, что дизайн хаскеля делался через жопу?

Где лучше?

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

щарп, джава, плюсы, руби, питон, лиспы - это навскидку

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

То есть монады - они вслед за ИО пошли, именно так, а не наоборот. Не было бы ИО - не было бы монад.

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

Это какие вопросы?

Это где знаки вопроса были. Мне пока не понятно как вы пришли к выводу, что IO сделан через монады, и я не понимаю что значит «сделан через монады».

Речь ведь шла именно о монадах. А конкретно о том, что монады - кривой костыль. Раз о монадах не говорили - то и не влезайте.

То что костыль - это ваша фантазия, так что я всё таки влез в разговор.

Точнее имеют, но только в том смысле, что параметрический полиморфизм элементарно реализуется на макросах.

Вот Common Lisp - как определить тип (ADT, т.е. набор классов или структур) «список чего-то», чтобы можно было по месту уточнять чего список. Можно определить отдельно список-чисел, отдельно список-списков, или список-чего-угодно, или кодировать списки точечными парами (тип - пара чего удоно или null). Параметрично - нельзя. Как сделать параметрично на макросах и ещё чтобы было элементарно?

на макросах можно спокойно реализовать CoC

Надо говорить не реализовать, а нафигачить :)

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

Все динамические языки по определению более высокоуровневы, чем статические :)

Странное понятие высокоуровневости. В ассемблере я могу спокойно обратится по адрусу за границами сегментов, в си, при аккуратной работе с указателями и массивами, уже не могу, при этом си выше уровнем (уже появились новые абстракции). В динамическом языке я могу спокойно написать ill typed код, в статически типизированном языке - это сложнее (появились абстракции типов). Какой отсюда вывод? В языке с логическим фреймворком я ещё могу что-то сделать, например, утверждать коммутативность функции.

Экхм, я ожидал ссылки на статью с формальным описанием системы типов, а не ссылки на какие-то комменты где-то, да еще и не рабочие. Гм. У них что, нету спеки для системы типов?

Литературы по pure type systems и lambda cube и так достаточно. В JHC просто реализация. Я его в пример привёл потому что вы вечно ругаете SystemF - под капотом не обязательно должна быть она, там и PTS может быть и CoC, другое дело, что если мы захотим повысить мощность именно front-end языка (то есть хаскеля), то TI станет сложнее и пользователю придётся писать кучу типов при каждом терме, баланс нарушится - суть хаскеля именно в том, что есть баланс между мощностью системы типов и простотой написания програм.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

>что перемешать эти слои нельзя, нету run IO

Я протестую! Функции runX не смешивают слои. Функция runX — удобный способ сказать «всем спасибо, все свободны, но больше в услугах этого слоя я не нуждаюсь», когда работаем со стеком монад, например.

Проблемы же IO связаны с хитрожопой машинерией рантайма, и в принципе, меня как программиста не волнуют. Более того, мне совершенно ничего не стоит «избавиться» от ненужного IO, благо техник много: и удобные (<$>) и (<*>) с (=<<), и возможность вынести «чистые» вычисления за IO, и проектирование вычислений по форме a -> m b (а не m a -> m b как это делают начинающие программисты). Также совершенно ничего не стоит добавить еще один слой IO, потому что любая монада проектируется как трансформер, а обычные монады представлены трансформерами в форме m Identity b (и вообще используются только в туториалах), и поменять Identity на IO не стоит вообще ничего. В mtl'овских монадах даже liftIO писать не нужно.

Самое смешное, что функция runIO :: IO a -> a теоретически может существовать. Такая функция должна создавать некий контекст в рамках глобального IO в котором будет работать физическое IO. При вычислении runIO а) создаем контекст, б) вычисляем свой аргумент в eager-режиме, в) грохаем контекст, все физические IO завершаются. И никакой инконсистентности нет. Это и сделают, когда IO генерализуют в рамках какого-нибудь STM или RWS. Но, еще раз повторюсь, мне на это, как программисту, глубоко пофиг.

ЗЫ: Таки поражает железобетонное КЗ в мозгах околохаскелистов: Монады—IO—unsafePerformIO—императивщина—не_нужно.

Macil ★★★★★ ()
Ответ на: комментарий от quasimoto

> IO реализован в _рантайме_, а не в _языке_.

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

Точно также IO можно было бы использовать с помощью родных примитивов

Ну нельзя.

Т.е. вам не понятно в чём общая суть именно Monad?

Мне как раз понятно - ее нет, этой общей пользы. Реально, мы не можем написать такой код, который бы, во-первых, делал что-то полезное, во-вторых - использовал исключительно те свойства монад, которые не включаются в аппликативный функтор, и, в-третьих, не учитывал бы особенностей конкретной монады (то есть работал бы «для монад в общем»). Монады просто слишком различаются семантически. Код, который имеет определенный смысл для монады А не будет иметь совершенно никакого смысла для монады B (сравним, например, с тем же функтором, где семантика fmap практически всегда совпадает).

если к A построен правильный монадический интерфейс, то мы можем разделять вычисления на два логических слоя inside A и outside A, в случае с IO - inside IO и outside IO

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

Ну, внутри IO у меня unpure код

Ну да, только выполнять этот код никто не будет. Семантически можно вообще считать, что IO a - это просто такой String, который содержит код на некотором неспецифицированном ЯП, который, в свою очередь, при выполнении на некотором неспецифицированном вычислителе (у которого семантика не определена) «вернет» то, что в некотором смысле мы можем считать объектом «типа» a. По-этому в хаскеле нету никакого unpure кода - то что внутри ИО это не код на хаскеле, и он не исполняется вычислителем хаскеля.

Офигеть, и как же все прикладные программы тогда работают?)

Программа на хаскеле возвращает ИО - то есть некоторую другую программу. То есть, формально, программа на хаскеле - это то, что выполняется во время компиляции. Далее в результате компиляции мы получаем программу, которая является представлением нашего ИО. Как это ИО представлено, и как оно будет вычисляться - это уже к хаскелю и его рантайму отношения никакого не имеет, возможно, это будет питонячий код, выполняемый интерпретатором питона :)

А какая там система типов?

System F с какими-то расширениями.

Где лучше?

Да везде где есть нормальный ИО.

anonymous ()
Ответ на: комментарий от quasimoto

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

А зачем нам высказываться о монадном интерфейсе? Достаточно того, что монады можно использовать. Но никто не использует. Почему?

Но сейчас я вижу _практическое_ использование и монад

Ну так я уже объяснил почему. Сделали монадический интерфейс к ИО, но не оставлять же его единственным? Это выглядело бы как пятое колесо. Вот и наделали монад из чего-угодно, хотя смысла в этом никакого нет (ну вот например - что дает монадический интерфейс для списков вдобавок к уже существующему list comprehension? ничего, верно). Дело-то ведь в чем- мы не можем не использовать ИО. А отсюда следует что не можем не использовать монады.

Это где знаки вопроса были. Мне пока не понятно как вы пришли к выводу, что IO сделан через монады, и я не понимаю что значит «сделан через монады».

Будем считать, что это значит «работа с ИО ведется через монадический интерфейс». И семантически в хаскеле никакого другого способа для работы с ИО не определено и определено быть не может.

Вот Common Lisp - как определить тип (ADT, т.е. набор классов или структур) «список чего-то», чтобы можно было по месту уточнять чего список.

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

Как сделать параметрично на макросах и ещё чтобы было элементарно?

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

Надо говорить не реализовать, а нафигачить :)

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

anonymous ()
Ответ на: комментарий от quasimoto

> В динамическом языке я могу спокойно написать ill typed код

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

Литературы по pure type systems и lambda cube и так достаточно. В JHC просто реализация.

Реализация чего? Я имею ввиду - что именно там шире, чем System F, в этой реализации?

Я его в пример привёл потому что вы вечно ругаете SystemF - под капотом не обязательно должна быть она

Что значит «под капотом»? Важно, какая у нас система типов в ЯП, а чего там под капотом - не важно совершенно. Если уж на то пошло, то PTS _всегда_ будет «под капотом».

anonymous ()
Ответ на: комментарий от quasimoto

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

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

anonymous ()
Ответ на: комментарий от Macil

> Самое смешное, что функция runIO :: IO a -> a теоретически может существовать. Такая функция должна создавать некий контекст в рамках глобального IO в котором будет работать физическое IO. При вычислении runIO а) создаем контекст, б) вычисляем свой аргумент в eager-режиме, в) грохаем контекст, все физические IO завершаются.

Этого ничего в хаскеле сделать нельзя, т.к. в хаскеле вообще нету способа вычислить ИО (просто согласно семантике ЯП).

anonymous ()
Ответ на: комментарий от anonymous

Точно также IO можно было бы использовать с помощью родных примитивов

Ну нельзя.

{-# LANGUAGE UnboxedTuples, ForeignFunctionInterface #-}

import Prelude ( ($), (.), const )
import Foreign.C
import GHC.Types

--------------------------------------------------------------------------------

class Functor f where
  map :: (a -> b) -> f a -> f b

class Functor f => Pointed f where
  pure :: a -> f a

class Pointed f => Applicative f where
  (<*>) :: f (a -> b) -> f a -> f b

class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  (>>)  :: m a -> m b -> m b
  m >> n = m >>= const n

--------------------------------------------------------------------------------

instance Functor IO where
  map f x = x >>= (pure . f)

instance Pointed IO where
  pure x = IO $ \s -> (# s, x #)

instance Applicative IO where
  a <*> b = a >>= \x -> b >>= \y -> pure $ x y

instance Monad IO where
  (IO m) >>= k = IO $ \s -> case m s of
    (# s', x #) -> unIO (k x) s'
      where unIO (IO a) = a

--------------------------------------------------------------------------------

foreign import ccall "putchar" putchar :: CInt -> IO ()
foreign import ccall "getchar" getchar :: IO CInt

t1 = getchar >>= pure

t2 = getchar >>= putchar

т.е. можно как угодно конструировать/разбирать вручную термы IO, они (как вы уже заметили) будут своеобразным DSL который должен выполнить рантайм (но к нему сводить всё тоже нельзя - есть ещё *Var-ы, STM, треды). При этом легко можно построить что-то unsafe от чего рантайм либо упадёт, либо бросит исключение (в зависимости от того как он сделан), но если использовать монадический (и более слабые - функторный, точечный и аппликативный) интерфейс, то есть _гарантия_, что получившийся IO всегда будет правильный. Именно по этому стандартные модули не экспортируют конструкторы и аккессоры для IO.

Был бы интерфейс через стрелки - использовали бы повсюду стрелки. Так ок?

Ну напишите тогда инстансы Category IO и Arrow IO?

Монады просто слишком различаются семантически. Код, который имеет определенный смысл для монады А не будет иметь совершенно никакого смысла для монады B

Не иначе как нужно смотреть не на аналогии, а на аналогии между аналогиями :) Т.е. монадный интерфейс несколько более абстрактный, чем функторный.

Семантически можно вообще считать, что IO a - это просто такой String, который содержит код на некотором неспецифицированном ЯП, который, в свою очередь, при выполнении на некотором неспецифицированном вычислителе (у которого семантика не определена) «вернет» то, что в некотором смысле мы можем считать объектом «типа» a. По-этому в хаскеле нету никакого unpure кода - то что внутри ИО это не код на хаскеле, и он не исполняется вычислителем хаскеля.

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

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

Достаточно того, что монады можно использовать. Но никто не использует. Почему?

Я всякий раз как пытаюсь проследить генезис монад в языке с динамической типизацией, или без параметрических типов вижу, что они там естесвенно не возникают. В хаскеле с его свойствами они возникают естественно. Нет, понятно конечно, что это идеология - где-то в начале 90-ых появились статьи про реализацию IO в pure языке с помощью монадических интерфейсов и решили делать так (а не через unsafe функции или там систему эффектов).

делали монадический интерфейс к ИО, но не оставлять же его единственным?

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

Думаете, создатели языка и библиотек так прям сидели и думали - «ох, блин, IO монада, надо ещё монад наделать - парсеров, принтеров, ридеров, врайтеров, это ж сколько дисеров!». Или руководствовались соображениями удобства?

что дает монадический интерфейс для списков вдобавок к уже существующему list comprehension?

Там сахар для этих comprehension превращается в цепочку >>= и >>, также как и do-сахар. Так что, наверное, ничего. Зато укладывается в идеологию.

Повторяю - в высокоуровневых (динамических) языках не надо заниматься всякими низкоуровневыми вещами навроде «определять тип»

Только гетерогенность, только хардкор :)

Инстанцируем шаблон (вызываем макрос) получаем нужную ф-ю (всмысле с нужным монотипом).

(define-data list
  nil
  (cons (first)
        (rest)))

Вот из такой штуки я могу сгенерировать define-structur-ы (типы произведения), и вариантный тип (тип сумму), это будет гетерогенный список. Но что мне генерировать из этого:

(define-data (list a)
  nil
  (cons (first a)
        (rest  a)))

?

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

Ну на макросах обычно «фигачат», это же факт. Для racket-а (или для чего-нибудь такого) уже написали что-нибудь?

Реализация чего? Я имею ввиду - что именно там шире, чем System F, в этой реализации?

Реализация core language, который мощнее SystemF (λPω > λ2 + λω), что позволяет, например, реализовать классы типов не отдельно в виде табличек спецификацый методов (как в C++), а непосредственно, передавая типо-термы в функции.

при динамической типизации корректно типизированные программы не отвергаютсЯ, при статической - отвергаются

Пример такой программы, которая отвергается статически типизированным языком? А то обычно наоборот. Пример - если я высказываюсь «бинарная функция» в динамическом языке, то что ещё я могу сказать? Я могу написать счётное количество таких функций. Но если я высказываюсь:

(/\) :: Boolean -> Boolean -> Boolean

то множество сокращается до 16 возможных определений. Если добавить алгебраические утверждения, то и вообще можно добраться до однозначно разрешимого определения таблицы значений (без её непосредственного задания).

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

Люди которые пишут на хаскеле воспринимают это не как йоплю, а как помощь компилятора. И вообще типы это ещё и логика, а не просто какие-то проверки времени компиляции (чем богаче язык типов, тем больше такой «логики»).

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

>Этого ничего в хаскеле сделать нельзя, т.к. в хаскеле вообще нету способа вычислить ИО (просто согласно семантике ЯП).

Тебе уже неоднократно объясняли, что IO зависит от конкретной реализации конкретного рантайма и к хаскелю отношения не имеет.

Вот пример того как IO в хаскеле вычисляется... Точнее не вычисляется: const () $ putStrLn «Foo» Собственно ради этого вся возня и затевалась.

Macil ★★★★★ ()
Ответ на: комментарий от quasimoto

Ну на макросах обычно «фигачат», это же факт. Для racket-а (или для чего-нибудь такого) уже написали что-нибудь?

ты про

#lang racket

(define list-of-integers? (listof integer?))

(define/contract (test xs)
  (-> list-of-integers? void?)
  (print 'ok))

(test '(1 2 3))
(test '(1 2 a))
?

korvin_ ★★★★★ ()
Ответ на: комментарий от anonymous

> «алгоритм есть, но он иногда виснет» и «алгоритма никто не придумал В ПРИНЦИПЕ»

А напомни ты себе определения алгоритма и пойми, что «алгоритм есть, но он иногда виснет» — не алгоритм

anonymous ()
Ответ на: комментарий от quasimoto

> т.е. можно как угодно конструировать/разбирать вручную термы IO

Блаблабла. Проблема в том, что никаких Foreign.C в хаскеле нету и быть не может. Формальная семантика языка такие вещи запрещает (в рамках хаскеля просто нету никаких средств, чтобы выразить такую штуку как сишная функция). Так что это уже идут костыли конкретной реализации хаскеля, с самим хаскелем они никак не связаны.

Ну напишите тогда инстансы Category IO и Arrow IO?

Зачем?

Не иначе как нужно смотреть не на аналогии, а на аналогии между аналогиями :) Т.е. монадный интерфейс несколько более абстрактный, чем функторный.

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

Хаскель это такой чистый функциональный алгебраический язык, который генерирует строгие императивные программы, которые выполняются рантаймом реализации.

Ну да. Причем о рантайме ничего неизвестно.

anonymous ()
Ответ на: комментарий от quasimoto

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

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

А ещё удивительно

Ничего удивительного.

Думаете, создатели языка и библиотек так прям сидели и думали - «ох, блин, IO монада, надо ещё монад наделать - парсеров, принтеров, ридеров, врайтеров, это ж сколько дисеров!».

Именно так.

Или руководствовались соображениями удобства?

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

Там сахар для этих comprehension превращается в цепочку >>= и >>, также как и do-сахар.

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

Но что мне генерировать из этого:

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

Ну на макросах обычно «фигачат», это же факт. Для racket-а (или для чего-нибудь такого) уже написали что-нибудь?

Нет, а зачем, собственно? Ну сделаете вы диалект, который будет в обе стороны абсолютно несовместим с оригиналом. Зато хиндли-милнер, ага.

Реализация core language, который мощнее SystemF (λPω > λ2 + λω)

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

Пример такой программы, которая отвергается статически типизированным языком?

Ну это зависит от системы типов. В некоторых случаях даже банальное (if pred 1 «1») нельзя, в других - такое выражение типизировать можно (если есьт типы-объединения, например).

(чем богаче язык типов, тем больше такой «логики»)

Которые заведомо менее богаты, чем контракты.

anonymous ()
Ответ на: комментарий от Macil

> Тебе уже неоднократно объясняли, что IO зависит от конкретной реализации конкретного рантайма и к хаскелю отношения не имеет.

Так я это до вас и пытаюсь донести. В рамках хаскеля вообще нет такого понятия - «вычислить ИО». Мы IO из программы вернули - и все. Дальше мы с ним ничего делать не можем, что там с этим ИО происходит - это уже не проблема хаскеля.

anonymous ()
Ответ на: комментарий от korvin_

По-моему он про полиморфизм на макросах спрашивал.

anonymous ()
Ответ на: комментарий от anonymous

Проблема в том, что никаких Foreign.C в хаскеле нету и быть не может.

Не туда смотрите. Нужно не Foreign.C (это просто для примера - чтобы не определять родных примитивных IO функций), а GHC.Types (ну или что-то другое в другой реализации).

Формальная семантика языка такие вещи запрещает

Формальныя семантика никак не запрещает использовать:

type IOf a = State RealWorld -> (State RealWorld, a)

data IO a where
  IO :: { unIO :: IOf a } -> IO a

-- IO   :: IOf a -> IO a
-- unIO :: IO a -> IOf a

IO - обычный ADT, термы типа IO - обычные термы которые рантайм будет интрепретировать / компилировать во что-то по правилам интерпретации / трансляции IO примитивов (отдельно от правил трансляции core language).

И всё это вообще частный случай ST - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.3299.

Ну напишите тогда инстансы Category IO и Arrow IO?

Зачем?

Вы пишете что, если бы сделали стрелочный интерфейс к IO, то все бы юзали стрелки, при том, что стрелочный интерфейс к IO это нонсенс.

Ничего удивительного.

Я к тому что костыли это костыли, они не нуждаются в обоснованиях. Обосновывают обычно концепции, идеологии и удобные модели.

Ну есть спеки этого core language и его системы типов?

Таких статей как для SystemFC - нет.

И, кстати, странное решение - какой смысл делать в core language более богатую систему типов?

Систему для core language берут заведомо мощнее - не только чтобы реализовать haskell98, но и какие-то расширения. В GHC его core language избыточен для haskell98, но позволяет добавить RankNTypes, GADTs, FunDeps, разные расширенные инстансы, TypeFamilies и т.п. То что у JHC core language больше чем у GHC значит, что, в принципе, там можно реализовать больше расширений системы типов.

В некоторых случаях даже банальное (if pred 1 «1»)

А, ну да. Если типы алгебраичны для этого нужно чтобы (if :: Bool -> a -> b -> a :| b) и писать нужно (if pred (L 1) (R «1»)), а если типы как предикаты, то можно так и писать (if pred 1 «1»), но иметь тот же тип для if.

quasimoto ★★★★ ()
Ответ на: комментарий от korvin_

Ну assert сделать или написать пару макросов вокруг difine с assert-ом (и сказать что у нас тут «контракты») это не проблема. В динамическом языке - самое то, но это совсем не система типов, type level-а вообще нет, мы так и остаёмся с одними значениями.

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

(: test ((Listof Integer) -> Void))

Я правильно понимаю, что у нас так и будут гетерогенные структуры и мы просто в контракте устанавливаем их использование как гомогенных (так что в рантайме будут сыпаться исключения)?

Вот такой ворос:

  data A = A Int Int                    | (define-structure a int int)
  ------------------------------------------------------------------------------
  data A = forall a b. A a b            | (define-structure a t t)
  ------------------------------------------------------------------------------
  data A a b = A a b                    | ?

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

struct {
  int ...;
  int ...;
}

struct {
  object ...;
  object ...;
}

object == void*

или

object == int (тэгированный указатель)

в третьем слуае у нас есть type level с конструкторами типов. Вот я и спрашиваю - что делать в динамическом языке без type level-а?

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Ну assert сделать или написать пару макросов вокруг difine с assert-ом (и сказать что у нас тут «контракты») это не проблема. В динамическом языке - самое то, но это совсем не система типов, type level-а вообще нет, мы так и остаёмся с одними значениями.

я таки не понимаю, что тебя не устраивает? и чем по-твоему предикатная система типов — не система типов?

korvin_ ★★★★★ ()
Ответ на: комментарий от quasimoto

> в третьем слуае у нас есть type level с конструкторами типов. Вот я и спрашиваю - что делать в динамическом языке без type level-а?

зачем нам это в динамическом ЯП?

korvin_ ★★★★★ ()
Ответ на: комментарий от korvin_

я таки не понимаю, что тебя не устраивает?

Что нет type level-а? А если он и есть (вроде typed racket или TI в CMUCL), то довольно слабый.

и чем по-твоему предикатная система типов — не система типов?

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

зачем нам это в динамическом ЯП?

А зачем STL писался на схеме? За тем чтобы иметь обобщённые гомогенные структуры. Вот например в хаскеле есть система типов - каждому терму соответсвует тип, и то что тип может быть параметричным позволяет, помимо прочего, до запуска программы знать, что мы используем гомогенные структуры как гомогенные. А не так, что где проверили assert-ами гомогенность - всё будет хорошо, а где не проверили - как придётся.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Типы это, по определению, то что существует до запуска программы

в первый раз такое слышу, откуда инфа?

korvin_ ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.