LINUX.ORG.RU

Вышел пятый выпуск Haskell Platform

 , , , ,


2

5

Вчера, 3 июня, спустя примерно полгода со времени предыдущего релиза, вышел пятый (за номером 2012.2.0.0) выпуск Haskell Platform — простого в установке окружения разработки для языка Haskell.

Данный выпуск включает в себя:

>>> Подробности

★★★★

Проверено: mono ()
Последнее исправление: Silent (всего исправлений: 1)
Ответ на: комментарий от petyuna

Почему ты так думаешь? Просто это не так афишируется.

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

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

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

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

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

в лиспе нет четкого разграничения, где какой стиль

Сколько лисп-диалектов — столько и стилей.

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

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

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

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

А масло - ни что иное, как какой-то неправильный маргарин, ага.

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

А если просто взять сильных программистов и попросить их выучить хаскель? Насколько велики шансы на успех?

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

Ты планируешь это писать в вакансии или говорить уже после устройства? «Ребята, у нас серьезно меняется платформа завтра все пишем на хаскелле?»

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

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

Сильный программист не может быть узко-специализированным.

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

А если просто взять сильных программистов и попросить их выучить хаскель? Насколько велики шансы на успех?

А что знают «сильные программисты»? Если у них порядок с матаном и прочим, и, внимание, если они поймут, в чем сила ФП, тогда успех будет автоматом.

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

А что знают «сильные программисты»? Если у них порядок с матаном и прочим, и, внимание, если они поймут, в чем сила ФП, тогда успех будет автоматом.

Ага, щас. :-)

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

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

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

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

Вы не поняли, _хороший_ программист _обязан_ быть математиком, иначе он не хороший программист, а просто кодер ;)

Язык построен на в общем-то мощных идеях, но с точки зрения software engineering у него и его стандартного инструментария есть масса больших проблем.

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

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

> А что знают «сильные программисты»? Если у них порядок с матаном и прочим, и, внимание, если они поймут, в чем сила ФП, тогда успех будет автоматом.

100% гарантию дают только в сберкассе :)

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

Что касается силы ФП. У него есть и слабости. О них тоже надо знать. Кстати, хаскель тут хороший пример. Монада State только для передачи состояния через череду маленьких крохотных функций - это нечто!

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

И все же, хотелось бы услышать обоснование этого «Язык построен на в общем-то мощных идеях, но с точки зрения software engineering у него и его стандартного инструментария есть масса больших проблем.» :)

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

+100500 Математика ведь и в структурах данных, и в асимптотике итп.

Кстати, вопрос тем кто в теме. У какого языка круче экосистема: у фа-диеза или хаскеля (возможноть дергать дотнет-библиотеки не в счет)?

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

Что касается силы ФП. У него есть и слабости. О них тоже надо знать. Кстати, хаскель тут хороший пример. Монада State только для передачи состояния через череду маленьких крохотных функций - это нечто!

А самое веселое начинается, когда приходится использовать monad transformers.

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

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

1. синтаксис - сложный и постоянно меняющийся. Из-за этого сложно или невозможно написать нормальный инструментарий для автоматического анализа, рефакторинга, и т.д. И да, я в курсе про HaRe. При этом я не считаю, что синтаксис сложен для людей.

2. finalizers, навешиваемые на объекты и завязанные на работу GC.

3. cabal, что умеет установить пакеты, но не может их удалить.

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

5. а когда к этому добавляется прикол с несколькими версиями одного и того же пакета в системе тогда проще все снести и переустановить.

6. монады сложно соединить. Monad transformers это ужас.

7. все исключения - unchecked. Гарантировать, что исключение не будет выброшено в критичном участке - невозможно.

8. ленивость иногда ставит в тупик даже экспертов, резко влияя на скорость выполнения при казалось бы минимальных изменениях, слабо относящихся к притормозившему коду.

9. в сыром виде система типов недостаточна. А расширения часто не совместимы между собой или могут привести к явно неправильному поведению.

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

P.S. что за идея?

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

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

Не знаю, где вы нашли таких экспертов. Насчёт резкого изменения скорости - так это вполне ожидаемо.

Monad transformers это ужас.

Хм, а что в них ужасного? Давеча скрещивал Random, List и Writer, всё просто и понятно.

все исключения - unchecked

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

в сыром виде система типов недостаточна.

Мир вообще несовершенен.

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

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

Чтобы это гарантировать нужно гарантировать тотальность кода. В критичном месте можно не использовать частичных функций (head, read и т.д.), использовать только функции для которых известно что они тотальны, писать тотальные функции, смотреть выхлопы GHC на предмет покрытия cases и guards (с -Wall).

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

Что-то вроде

import Data.Time
import Control.Applicative

brazil :: TimeZone
brazil = TimeZone (- 3 * 60) False "BRT"

getBrazilOfficialTime :: IO ZonedTime
getBrazilOfficialTime = utcToZonedTime brazil <$> getCurrentTime

не подходит?

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

Выше ответили.

P.S. что за идея?

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

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

Не знаю, где вы нашли таких экспертов.

Например:

It is very difficult to predict the time and space behavior of lazy functional programs.

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

Чистый код тоже может поделить на ноль или сделать head [].

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

Чистый код тоже может поделить на ноль или сделать head [].

head [] избежать можно, выше говорили как. При делении на ноль исключение по умолчанию не возникает, а возвращается NaN, также как и в других языках.

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

head [] избежать можно

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

При делении на ноль исключение по умолчанию не возникает, а возвращается NaN, также как и в других языках

> 1 `div` 0
*** Exception: divide by zero
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

It is very difficult to predict the time and space behavior of lazy functional programs.

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

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

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

При делении на ноль исключение по умолчанию не возникает, а возвращается NaN, также как и в других языках

> 1 `div` 0
*** Exception: divide by zero

Речь о плавающем делении, а ты показал целое.

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

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

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

Речь о плавающем делении, а ты показал целое.

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

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

Если я упомянул NaN, значит речь всяко шла о плавающих числах. Про целочисленное деление согласен.

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

Если я упомянул NaN, значит речь всяко шла о плавающих числах.

(/) для плавающих чисел не является примером частичной функции, поэтому просто не интересна. Речь о том, что в нынешнем хаскеле всегда существуют частичные функции отсутствие которых никак нельзя гарантировать статическими средствами, поэтому даже в чистом коде действительно нельзя дать 100% гарантию того, что не возникнет исключение.

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

всегда существуют частичные функции

Ну это... Можно же при желании понаписать функций вроде

div' :: Integral  a => a -> a -> Maybe a
dmfd
()
Ответ на: комментарий от quasimoto

Этот второй шаг тоже можно сделать (agda, например).

Забавно. Как в этом случае будет выглядеть тот же div или head?

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

Не знаю, где вы нашли таких экспертов. Насчёт резкого изменения скорости - так это вполне ожидаемо

http://www.starling-software.com/misc/icfp-2009-cjs.pdf

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

Monad transformers это ужас.

Хм, а что в них ужасного? Давеча скрещивал Random, List и Writer, всё просто и понятно.

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

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

Ага, а что делать с «нечистым»?

Мир вообще несовершенен.

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

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

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

Ну конечно, очевидно, само собой разумеется - нет.

Уродливо и неочевидно.

Почему неочевидно? Достаточно смотреть на сигнатуры, а что внутри - на совести автора.

А если система типов в хаскеле не дает решить проблему

Бро, покажи мне язык с идеальной системой типов, я на него тут же перейду.

Ага, а что делать с «нечистым»?

Зависит от ситуации.

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

P.S. Для человека с более-менее математическим складом ума система типов в хаскеле довольно подходящая.

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

Можно же при желании понаписать функций вроде

Можно делать монадические обобщения вроде

headM :: Monad m => [a] -> m a
headM [] = fail "empty list"
headM x = return $ head x

-- > runIdentity (headM [])
-- *** Exception: empty list
-- > headM [] :: Maybe a
-- Nothing

divM :: (Monad m, Integral a) => a -> a -> m a
divM _ 0 = fail "division by zero"
dviM x y = return $ div x y

-- > runIdentity (1 `divM` 0)
-- *** Exception: division by zero
-- > 1 `divM` 0 :: Maybe Int
-- Nothing

readM :: (Monad m, Read a) => String -> m a
readM s | [x] <- [x | (x, "") <- reads s] = return x
        | otherwise = fail $ "parse error: \"" ++ s ++ "\""

-- > runIdentity (readM "q1" :: Identity Int)
-- *** Exception: parse error: "q1"
-- > readM "q1" :: Maybe Int
-- Nothing

которые частичны в одних монадах и тотальны в других.

Как в этом случае будет выглядеть тот же div или head?

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

take : ∀ {a} {A : Set a} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

head : ∀ {a} {A : Set a} → List A → List A
head = take 1

обычный (как в хаскеле) и при этом правильный head возможен для «векторов»:

head : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
head (x ∷ xs) = x

тут на уровне системы типов известно, что в векторе достаточно элементов для выполнения head.

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

Чтобы это гарантировать нужно гарантировать тотальность кода.

И как ее гарантировать с практической точки зрения?

В критичном месте можно не использовать частичных функций (head, read и т.д.), использовать только функции для которых известно что они тотальны, писать тотальные функции,

Да, head и read это вообще песня. Причем это - часть _стандартной_ библиотеки. Лично я их не использую, но можешь ли предложить способ на 100% гарантировать, что ни в моем коде, ни в коде библиотек они не вызываются?

смотреть выхлопы GHC на предмет покрытия cases и guards (с -Wall).

Свой-то код еще как-то можно проверить...

Что-то вроде

import Data.Time

import Control.Applicative

brazil :: TimeZone

brazil = TimeZone (- 3 * 60) False «BRT»

getBrazilOfficialTime :: IO ZonedTime

getBrazilOfficialTime = utcToZonedTime brazil <$> getCurrentTime

У меня это выводит вот что:

2012-06-06 12:03:09.919154 BRT

Тут есть минимум такие проблемы:

1. явно приходится для каждой зоны конструировать ее описание. Ты не можешь просто сказать «зона Бразилии», приходится указывать какой сдвиг по отношению к GMT и летнее ли там время. А все это меняется со временем, причем слабопредсказуемо. Фактически, в некоторых странах правительство может объявить что они прямо завтра неожиданно переходят на зимнее время. И как твой софт будет это поддерживать? :)

2. формат времени неправильный. Должно быть что-то типа «06/06/2012 12:03:09.919154». Правильный формат времени для Бразилии описан, например, тут: http://en.wikipedia.org/wiki/Date_and_time_notation_in_Brazil

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

P.S. Для человека с более-менее математическим складом ума система типов в хаскеле довольно подходящая.

О да.. :-) Сильный аргумент. Вообще-то я не о том, что она сложная, если тебе не очевидно. Я о том, что она «закрытая» и ее расширения не совместимы одно с другим.

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

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

Конечно. «Лучшее» - враг «хорошего». Даже если «хорошее» ну просто очень плохое. :)

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

не будет пропущена тайпчекером - обычный head просто не пишется

Ясно, спасибо.

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

что она «закрытая»

Пример «открытой». Не совсем понимаю, что под этим понятием кроется.

и ее расширения не совместимы одно с другим.

Вам виднее, я пока с этим не сталкивался.

Лично я их не использую, но можешь ли предложить способ на 100% гарантировать, что ни в моем коде, ни в коде библиотек они не вызываются?

Часто приходилось сталкиваться с исключениями в чужом коде?

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

И как ее гарантировать с практической точки зрения?

Никак :) В хаскеле это невыразимые в языке / тулзах чисто умозрительные построения (например, можно ожидать, что length никогда не упадёт, а read - может упасть).

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

но можешь ли предложить способ на 100% гарантировать, что ни в моем коде, ни в коде библиотек они не вызываются?

Вот так, даже для сторонних библиотек, нельзя конечно. Есть пакет safe (0.3.3!), выше я привёл примеры монадических безопасных функций - можно определить тип MyLayer представляющий определённый безопасный уровень в стеке приложения, написать правильный instance Monad MyLayer и на этом уровне использовать безопасные монадические функции. Но это как раз из серии использования / сочинения монадических трансформеров (у которых, к тому же, константный оверхед).

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

Да, я посмотрел - как понял, в Sao Paulo всегда стабильно UTC-03, а в остальном - надо писать сложную функцию, учитывающую топологию (там в каждом штате свои правила). Это явно не задача стандартной библиотеки / платформы хаскеля, но задача специального софта.

Должно быть что-то типа «06/06/2012 12:03:09.919154»

Форматированием занимается Data.Time.Format:

> formatTime defaultTimeLocale "%d/%m/%Y %T%Q" <$> getBrazilOfficialTime
"06/06/2012 12:43:45.624452"
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Вообще, практически проще форкать лёгкие потоки, связывать в них STM очереди для сообщений, обрабатывать SomeException, посылать сообщение родителю и падать.

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

явно приходится для каждой зоны конструировать ее описание

Ага, пакет time имеет просто непосредственное отношение к хаскелю.

Если твоя предметная область подразумевает необходимость работы со временем, то используй соответствующие библиотеки, благо FFI устроен неплохо, а GHC'шный линковщик спокойно разбирается как с .o, так и с .so, в т.ч. и в байт-код режиме ghci. Т.е. можешь спокойно написать решение твоей проблемы на C, примитивную FFI прослойку, и спокойно работать.

А time - предельно простенький пакет, для несложных сценариев использования.

Запомни, хаскель это не фреймворк навроде .Net и Java. Хаскель спокойно интегрируется в сишную экосистему.

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

thesz, самый сильный программист на Haskell в России

В пауэрлифтинге? :)

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

В compile time нельзя проверить, что один из параметров - ноль.

Можно, например, гарантировать проверку делителя на 0 :)

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

А что возвращать-то в таком случае?

Исключение бросай, например. Хотя это уже не важно - то, что в некотором участке кода не будет division-by-zero, гарантировано.

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

Некто Лев Валкин делился в жжешке подобным опытом обучения хаскелю, окамлу и эрлангу группы кодеров, в гугле инфа должна быть. Да, наверное, ты читал. Там просто история успеха. Окамл, вроде, получше хаскела пошел.

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

Лев Валкин и группа кодеров просто неосиляторы хаскеля.

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

А что будет с div в агде?

Учитывая, что числа там реализуются как

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

... но допустим, что

postulate
  ℕ : Set
  zero : ℕ
  suc : ℕ → ℕ
  -- etc.

и они реализованы очень хорошо. div из стандартной библиотеки имеет сигнатуру

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ

то есть принимает два натуральных числа (то есть термы типа ℕ) и возвращает натуральное число (так что является простой функцией), кроме этого он принимает неявный (implicit) аргумент тип которого зависит (dependent type) от терма divisor, этот неявный аргумент представляет собой доказательство утверждения которое вычисляется в ⊥ если равенство (equality предикат / identity type) divisor ≡ 0 выводимо (decidable) и в ⊤ в обратном случае. То есть тут эта проблема тоже решается на уровне типов, как и в случае с head (только более муторно). Если у нас будет ⊥, ненаселённый тип, то div будет подобен такой функции

foo : ℕ → ℕ → ⊥ → ℕ
foo _ _ = ⊥-elim

её применение foo 1 2 имеет тип ⊥ → ℕ и вычисляется в ⊥-elim, нет доказательства которое можно передать, так что оно не имеет нормальной формы для полного применения и не пройдёт тайпчек.

В случае ⊤ (населённый тип) будет подобно

bar : ℕ → ℕ → ⊤ → ℕ
bar _ _ tt = 42

применение bar 1 2 tt имеет нормальную форму 42 и tt это передаваемое доказательство. В случае с div, так как аргумент неявный, доказательство строится автоматически, tt подставляется неявно. 1 div 1 имеет нормальную форму 1, 1 div 0 не имеет нормальной формы, останавливается на

1 div 0
| (1 divMod 0
   | _.dm 1 0 1
     (λ y y<x →
        _.dm 1 0 y
        (.Induction.WellFounded.Some.wfRec-builder
         (λ dividend →
            (divisor : ℕ) →
            {.Data.Bool.T (.Data.Bool.not ⌊ Nat._≟_ divisor 0 ⌋)} →
            DivMod' dividend divisor)
         (_.dm 1 0) y (<-well-founded′ 1 y y<x)))
     0)

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

Интересно ещё, что делать с числами из IO - то ли для них div не применим потому что нельзя построить соответсвующее доказательство, то ли можно как-то выкрутиться.

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

Мало что понял :( Но правильно ли я полагаю, что фразу

доказательство строится автоматически, tt подставляется неявно

вкупе с

Интересно ещё, что делать с числами из IO - то ли для них div не применим потому что нельзя построить соответсвующее доказательство,

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

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

Зря, ой зря, Вы позволяете исключениям возникать. Этого нельзя делать даже на уровне машинного языка (Х.З., что это).

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

можно с какой-то натяжкой интерпретировать, как если в compile time вычисляется значение знаменателя

Нет, это не значит, что знаменатель вычисляется в compile time, для него просто в compile time доказывается неравенство нулю. Это, буквально, proof carrying code.

Для примера:

t : ℕ → ℕ → ℕ
t m n = m div n

t принимает любые натуральные числа, но div хочет построить доказательство невыводимости n ≡ 0, чего в контексте t сделать нельзя - будет примерно такое сообщение:

Unsolved metas: T (not ⌊ n ≟ 0 ⌋)

так что div применим только тогда когда из контекста выводимо неравенство нулю знаменателя, каких-то знаний чему именно он равен (главное, что не нуль, по сути, просто по всюду поддерживается ℕ \ {0} для нужного аргумента) не предполагается. Такой контекст должен поддерживаться на всём протяжении вызовов div <- t1 <- t2 <- ... и так далее до интерфейса с пользователем, например, до emacs-mode agdы, или до IO (когда agda компилируется в хаскель). При этом интерфейс отделяет консистентное ядро от неконсистентного окружения, IO, например, реализуется как примитивы FFI, поэтому вполне может (и должно) падать, зависать, фильтровать поступающий контент и т.п. По сути, хорошее IO и система событий вообще это такая система, которая будет уметь «добывать» из событий то что можно отдать консистентному ядру и отсеивать остальное.

Касательно постулатов (в т.ч. примитивов FFI), они могут ломать консистентность как добавляя плохие аксиомы, например:

postulate
  contradiction : {ℓ : Level} {φ : Set ℓ} → ¬ φ

absurd : ⊥
absurd = contradiction tt

так и строя FFI к плохим функциям:

postulate
  _div_ : Integer → Integer → Integer

{-# COMPILED _div_ Prelude.div #-}
quasimoto ★★★★
() автор топика
Ответ на: комментарий от Virtuos86

А потом этот же некто Лев Валкин написал пост всё в той же жежешечке. Только уже без помпы, пафоса и по-тихому, типа «а вдруг не заметят?».

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

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

p.s. мораль: есть язык, код на котором принципиально не падает в рантайме, но этот код как правило нельзя скомпилировать.

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

Если ты говоришь про то, что он написал отдельный компактный веб-сервер вместо впендюривания этой же функциональности на том же Си куда-то там в Ерланг ВМ, то там про хаскель речи даже не шло.
По-моему везде, где хотят получить производительность, пишут на Си. Тот же хаскельный Core пока не перепиливают что-то на самом хаскеле.

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

А Вы Валуева отсосать попросите - и всё сразу узнаете.

Ученики в теме?!

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

Пример «открытой». Не совсем понимаю, что под этим понятием кроется.

ОК. Если система типов позволяет добавить ограничения, чтобы что-то гарантировать, то она - открытая. Не хочешь гарантий и ограничений - не используй. Плюс в том, что если тебе нужно что-то совсем дикое, и система типов для этого недостаточно выразительна, то можно «пойти по минному полю» и все равно написать работающий код. Возможно Qi или Go могут быть примерами. Сам я на них пока не писал.

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

и ее расширения не совместимы одно с другим.

Вам виднее, я пока с этим не сталкивался.

Rank2 types + ExistentialQuantification вроде не сильно совместимы.

И даже GADT плохо дружит с type classes (хоть они и часть основной системы).

Понятно, что иногда их можно как-то скрестить, но ни разу не видел красивых примеров. Более того, код с несколькими расширениями похож на извраты типа фибоначи на шаблонах C++.

Часто приходилось сталкиваться с исключениями в чужом коде?

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

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

Тот же хаскельный Core пока не перепиливают что-то на самом хаскеле.

Не Core а RTS, наверно? Всё что касается Core как раз на хаскеле в компиляторе.

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

Никак :) В хаскеле это невыразимые в языке / тулзах чисто умозрительные построения (например, можно ожидать, что length никогда не упадёт, а read - может упасть).

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

Поэтому классических read и head просто не должно быть. Должно быть типа так:

head :: [a] -> Maybe a

Вот так, даже для сторонних библиотек, нельзя конечно. Есть пакет safe (0.3.3!), выше я привёл примеры монадических безопасных функций - можно определить тип MyLayer представляющий определённый безопасный уровень в стеке приложения, написать правильный instance Monad MyLayer и на этом уровне использовать безопасные монадические функции. Но это как раз из серии использования / сочинения монадических трансформеров (у которых, к тому же, константный оверхед).

Ага.

Во-первых оверхед.

А во-вторых, пакеты типа safe просто уменьшают головную боль во время дебага. Они не делают статических проверок. А отсутствие необходимости делать дебаг - основной аргумент haskell-фанбоев и прочих штангистов. :-)

Да, я посмотрел - как понял, в Sao Paulo всегда стабильно UTC-03, а в остальном - надо писать сложную функцию, учитывающую топологию (там в каждом штате свои правила). Это явно не задача стандартной библиотеки / платформы хаскеля, но задача специального софта.

В том-то и дело, что это пока в Sao Paulo всегда стабильно UTC-03. Если завтра их правительство решит перейти на систему, где каждый чётный день у них будет UTC-04 - так и будет. И софт это обязан поддерживать. Поэтому у той же жабы есть возможность глянуть объект TimeZone даже по конкретному городу и он сам сделает всю магию (внутри он видимо смотрит в tzdata).

formatTime defaultTimeLocale «%d/%m/%Y %T%Q» <$> getBrazilOfficialTime

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

И я не занудствую, я показываю _практические_ задачи. Которые академикам, живущим среди эндофункторов, не очень видны. :-)

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

Ага, пакет time имеет просто непосредственное отношение к хаскелю.

Имеет. Это практически часть стандартной библиотеки.

Запомни, хаскель это не фреймворк навроде .Net и Java. Хаскель спокойно интегрируется в сишную экосистему.

Учишь отца детей делать? Молодец.

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

а) мой библиотеки были быстрее системный в 10-100 раз. И лишь из-за удивительной кривоты «стандартных».

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

в) мой код работал бы еще быстрее, но некоторые оптимизации просто невозможно реализовать даже в великом и могучем GHC. Если конкретно, то там нет нормального thread-local state. Максимум, что можно сделать - общее отображение с ThreadID на некие значения. А это тормозит просто адово. И я не верю, что ситуация изменится в ближайшие несколько лет. Потому что комонады народу интереснее чем решение практических задач.

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

Постоянно. Вся системная библиотека ими полна.

Я имел в виду не проблемы, возникающие от опасного применения стандартных функций (head []), а падения при правильном применении.

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

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

Rank2 types + ExistentialQuantification

Не знал. Приходилось пользоваться только RankNTypes и GeneralizedNewtypeDeriving. Они вроде не конфликтуют.

типа фибоначи на шаблонах C++

Ну зачем нужно было это говорить, я же теперь сколько времени зря потрачу! (Считал шаблонами только факториал)

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

Поэтому классических read и head просто не должно быть.

Во всех языках широкого применения (C, C++, Java, ...) есть такие частичные функции которые падаю или бросают исключение потому что реализованы не для всех элементов своих доменов (про динамически типизированные языки вообще молчим). Хаскель никак не выбивается из этого ряда, не будь в нём таких функций он бы был не хаскелем, а какой-нибудь агдой (с ошибками уровня «хотел прибавить 2, прибавил 1» или «хотел пойти туда по control flow, а пошёл не туда»).

head :: [a] -> Maybe a

Да

head :: (Pointed f, Failable f) => a -> f a

если кому-то не нравится Maybe - может написать свой Pointed / Failable instance который будет возращать удобные аналоги Just и Nothing (возможно ещё с сообщениями для Nothing, как у Either).

То что можно вместо Pointed и Failable сделать Monad, это, вообще, неправильно. Так же как неправильна классическая иерархия классов типов (более правильная описана в typeclassopedia), она, в частности, не позволяет написать instance Monad Data.Set без обвёрток (правильная - позволяет).

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

В safe как раз

headMay :: [a] -> Maybe a

Они не делают статических проверок.

Если в функцию попал пустой список, но нужно вернуть его элемент, делать нечего - нужно либо бросать исключение, либо возвращать конструктор обвёртки. Чтобы гарантировать, что пустой список вообще не попадёт это нужно отследить весь control flow вплоть до IO (а что и как делать в IO?), для чего хаскельная система типов и сопутсвующий тайпчекер не предназначены.

Поэтому у той же жабы есть возможность глянуть объект TimeZone даже по конкретному городу и он сам сделает всю магию (внутри он видимо смотрит в tzdata).

Это хорошо, кто-то явно взял, сел и написал нужный код :) Может есть подобный сишный функционал? Тогда FFI можно сделать довольно просто (придётся только написать кучу data для стран и их внутренних территорий).

Это все прекрасно, если defaultTimeLocale - бразильская. А если нет, и нужно бразильскую найти?

У defaultTimeLocale такой код, то есть она нужна чтобы обзывать месяцы и дни на местном языке и задаёт принятый способ форматирования дат и времени. Для форматирования которое ты попросил ничего этого не используется (ни названий месяцев, ни дней, ни %X, %r, %P, %p, %x и т.п.), так что можно даже написать

formatTime undefined "%d/%m/%Y %T%Q" <$> getBrazilOfficialTime

formatTime не потянется к undefined и не упадёт (т.е. не кинет исключение). Но если нужно что-то более бразильское - можно подобным образом написать brazilTimeLocale, примерно с таким же кодом как и для defaultTimeLocale, можно унаследовать:

brazilTimeLocale :: TimeLocale
brazilTimeLocale = defaultTimeLocale { {- тут переопределяемые поля -} }

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

Нужно показывать местное время? Первое что приходит на ум - AJAX-ом, с помощью какого-нибудь jQuery, стянуть время с какого-нибудь ресурса (т.е. CSI, под ресурсом подразумевается REST API). С какого ресурса - не знаю, нужно поискать, либо самому написать ресурс используя уже готовые библиотеки для форматирования времени (с такими тоже не сталкивался).

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

Смешно

а) мой библиотеки были быстрее системный в 10-100 раз. И лишь из-за удивительной кривоты «стандартных».

В Хаскельном листе есть тема про то, почему стандартные либы медленные, почему список - стандартный тип и т.д. Там все ответы. Написать свое, чтобы оно работало в 10 раз быстрее стандартного можно, но Вы поинтересуйтесь, зачем так было сделано изначально.

anonymous
()
Ответ на: Смешно от anonymous

В Хаскельном листе есть тема про то, почему стандартные либы медленные, почему список - стандартный тип и т.д. Там все ответы. Написать свое, чтобы оно работало в 10 раз быстрее стандартного можно, но Вы поинтересуйтесь, зачем так было сделано изначально.

И есть, значит, причины, почему

* почти ВСЕ вычисления, связанные с временем делаются с использованием Integer, хотя часто хватает и Int

* GHC не оптимизирует даже такую тривиальщину, как целочисленное деление (не заменяет на умножение и сдвиг)

* не позволяет быстрый доступ к thread-local state

* не позволяет вернуть из FFI структуру (а лишь указатель на нее)

* не инлайнил (уже инлайнит) выделение малюсеньких блоков памяти и вычисление, сколько же нужно выделить, даже если все для этого известно на этапе компиляции

?

:-)

Ну-ну.

rtvd ★★★★★
()
Ответ на: комментарий от quasimoto
import Data.Time
import Data.Time.LocalTime.TimeZone.Series
import Data.Time.LocalTime.TimeZone.Olson
import System.FilePath
import Control.Monad

timeZoneDb :: FilePath
timeZoneDb = "/usr/share/zoneinfo"

newtype Region = Region { timeZoneFile :: FilePath }
  deriving ( Show, Read, Eq )

region :: String -> Region
region reg = Region $ timeZoneDb </> reg

subRegion :: String -> String -> Region
subRegion reg subReg = Region $ timeZoneDb </> reg </> subReg

getLocalTime :: Region -> IO LocalTime
getLocalTime region = liftM2
  (flip utcToLocalTime')
  getCurrentTime
  (getTimeZoneSeriesFromOlsonFile $ timeZoneFile region)
*Main> getLocalTime (region "Japan")
2012-06-07 21:37:06.694734
*Main> getLocalTime (subRegion "America" "Sao_Paulo")
2012-06-07 09:37:09.11207
  • /usr/share/zoneinfo можно носить с собой и выставлять timeZoneDb при сборке библиотеки.
  • Вместо Region, region и subRegion на строках можно нагенерировать много нормальных data и рендерить их в FilePath, учитывая
    $ find /usr/share/zoneinfo | wc -l
    1809
    

    это будет, примерно, 4000LOC боилерплейта.

  • Проблему форматирования времени и даты так как это принято в данном регионе это не решает.
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto
  • То что getLocalTime в IO, а /usr/share/zoneinfo на диске, это не хорошо. Поэтому нужно переписывать (генерировать, скорее всего) всё что в /usr/share/zoneinfo в виде нормальных хаскельных data.
quasimoto ★★★★
() автор топика
Ответ на: комментарий от rtvd

И еще меня умиляет, как зело умные разработчики Haskell легко и непринуждённо приютили ту самую «billion-dollar mistake», которая была сделана еще в 1965 при разработке Algol ( http://en.wikipedia.org/wiki/Null_pointer#Null_pointer ).

При этом указатели параметризованы типом, хотя в результате половина низкоуровневого кода состоит из castPtr или как там его. А вот объявить указатель как Read-Only уже нельзя.

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

генерировать

*Main> getOlsonFromFile "/usr/share/zoneinfo/Europe/Moscow" >>= putStrLn . ("moscow :: OlsonData\nmoscow = " ++) . show
moscow :: OlsonData
moscow = OlsonData { [skiped]

И так рекурсивно для всего /usr/share/zoneinfo, тогда его можно не использовать и писать

getLocalTime moscow

-- где
getLocalTime :: OlsonData -> Maybe LocalTime

-- или
getLocalTime :: OlsonData -> LocalTime
quasimoto ★★★★
() автор топика
Ответ на: комментарий от rtvd

разработчики Haskell легко и непринуждённо приютили ту самую «billion-dollar mistake»

Разработчики Cyclone её тоже приютили (но там можно объявить указатель как never null). Ну и Ptr это типа FFI - оно должно полностью отражать типы Си.

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

почти ВСЕ вычисления, связанные с временем делаются с использованием Integer, хотя часто хватает и Int

Cогласен. Добивает представление даты как (Integer, Int, Int). Но опять же, пакет time - предельно простой и примитивный. И хотя идет вместе с бинарниками GHC, на стандартный ну никак не тянет, тем более на звание стандартной библиотеки. Стандартная библиотека - это base.

Дай хоть ссылку на твою библиотеку, интересно же...

не позволяет вернуть из FFI структуру (а лишь указатель на нее)

O_o А как ты это себе представляешь?

не позволяет быстрый доступ к thread-local state

Наверное, потому что разработчики клали на bound threads, и я их за это не виню. Да, TLS - классный механизм обмена в рамках FFI, но не в этой жизни.

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

разработчики Haskell легко и непринуждённо приютили ту самую «billion-dollar mistake»

Разработчики Cyclone её тоже приютили

И?

(но там можно объявить указатель как never null).

Это всяко лучше чем то, что в haskell.

Ну и Ptr это типа FFI - оно должно полностью отражать типы Си.

ОК, можно и с такой точки зрения смотреть. Но тогда Int хаскеля не эквивалентен int в C. Как это прокомментируете? :-)

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

Дай хоть ссылку на твою библиотеку, интересно же...

Дал бы, но не могу. Зато могу сказать, что это была просто обертка над clock_gettime и время там разделялось на наносекунды и секунты с момента Unix Epoch.

O_o А как ты это себе представляешь?

А в чем проблема-то?

Сложно вернуть данные на стеке?

Наверное, потому что разработчики клали на bound threads

А при чем тут bound threads? Почему нет доступа к TLS нитей вообще? Пусть он даже будет не доступен из FFI. Все равно будет лучше.

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

Сложно вернуть данные на стеке?

Сложно. Будут проблемы со сборкой мусора. Нужно заводить два разных механизма размещения, по аналогии с C++ и вносить изменения в Core.

Почему нет доступа к TLS нитей вообще?

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

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

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

не считая bounded threads.

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

И?

Never null pointer это довольно экзотическая вещь пока (вот, в Cyclone есть, наряду с обычными указателями и «толстыми», с арифметикой, указателями).

Но тогда Int хаскеля не эквивалентен int в C. Как это прокомментируете?

Int хаскеля != Int FFI, Int FFI это CInt. Сишный int понятие зависящее от архитектуры, у меня, например, сейчас на 64 битах 4 байтный int и, соответственно, sizeOf (undefined :: CInt) == 4, maxBound :: CInt == 2147483647, но sizeOf (undefined :: Int) == 8, maxBound :: Int == 9223372036854775807. При этом фиксированные числа в хаскеле не тегированы, так что их bounds и size вполне нормальные, но могут быть боксированы (вокруг небоксированных I16#, I32#, I64#, Int# и т.п.). Боксированная арифметика это ещё один повод поругать хаскель :) Боксированные прочие типы - тоже (вот в MLTon сделали compile time стирание параметрических типов и полностью небоксированную безопасную арифметику и небоксированные массивы). Слабый анализатор строгости - ещё один повод его ругать (вот в Clean же запилили уникальные типы и хороший анализатор строгости). Ещё в GHC, в силу инфраструктурных причин, не получилось сделать optimistic evaluation, которые в некоторых случаях намного лучше нестрогой стратегии. STG VM делает практически невозможным чтение ассемблерных выхлопов. Конкурентный GC не инкрементальный. Можно использовать seq, ($!) и deepseq, но писать удобно энергичный код нельзя (можно представить себе возможность включить для модуля / функции нужную стратегию вычисления, типа как с {-# RULES #-}). Нет top-level state (не нужно?). Нет возможностей дистрибутивного программирования (Cloud Haskell пока не вполне готов). Нет нормального REPL-а. Расширения GHC за рамками Haskell 2010 действительно выглядят как набор костылей. Вообщем, можно много к чему придираться. Но хороших вещей в языке и вокруг тоже много.

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

это была просто обертка над clock_gettime

А на одной неполноценной системе clock_gettime сильно неочевиден в случае 32-битности, и полностью отсутствует в случае 64-битности.

А значит, таскать с собой Cygwin, со всеми вытекающими.

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

Сложно вернуть данные на стеке?

Сложно. Будут проблемы со сборкой мусора. Нужно заводить два разных механизма размещения, по аналогии с C++ и вносить изменения в Core.

Не вижу проблем.

Например, если утверждается, что FFI позволяет функции возвращать Storable то должно быть возможно пробросить структуру назад. Runtime выделает ей место на стеке, вызывает внешнюю функцию. Та возвращает структуру, записывая данные в выделенное ей место на стеке в соотвествии с её calling convention. Runtime формирует haskellевый объект, используя указатель на стек. Где проблема?

Почему нет доступа к TLS нитей вообще?

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

Ну и пусть они не системные. Мне же не из foreign function нужно получить доступ к TLS.

Единственная проблема, которую я вижу сходу, это проблема с системой типов.

Нужны функции (очень приблизительно) вроде таких:

get :: IO a

put :: a -> IO ()

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

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

Ну и пусть они не системные. Мне же не из foreign function нужно получить доступ к TLS.

а можно поинтересоваться, как opengl-ные баиндинги работают, которые thread-state используют?

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

А на одной неполноценной системе clock_gettime сильно неочевиден в случае 32-битности, и полностью отсутствует в случае 64-битности.

А значит, таскать с собой Cygwin, со всеми вытекающими.

Запускать на кофемолках как-бы и не планировалось... :-)

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

а можно поинтересоваться, как opengl-ные баиндинги работают, которые thread-state используют?

Не знаю. Но там явно другая ситуация: при работе с OpenGL важно чтобы была только одна нить, причем это должна быть нить с точки зрения OS. Что она там делает уже дело десятое и свое состояние она скорее всего держит не на стороне haskell runtime.

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

возможность привязать нить к потоку есть, есть возможность из FFI достучаться до thread-local-state, есть возможность вернуть значение в haskell runtime, есть возможность передачи значения из haskell runtime в FFI. Дальше дело только в небольшой реализации?

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

возможность привязать нить к потоку есть, есть возможность из FFI достучаться до thread-local-state, есть возможность вернуть значение в haskell runtime, есть возможность передачи значения из haskell runtime в FFI. Дальше дело только в небольшой реализации?

До какого именно thread-local-state есть возможность достучаться? До того что у OS thread или haskell Thread?

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

OS thread. Какой нафиг thread-local-state может быть для легких потоков, или сформулирую по другому, зачем он может быть нужен?

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

Запускать на кофемолках как-бы и не планировалось...

Вот. Поэтому time и есть, такой как есть. Работает хреновенько, зато везде.

В идеале конечно, сделать бы эмуляцию POSIX в рамках GHC. Но, видимо, это никому не нужно.

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

OS thread. Какой нафиг thread-local-state может быть для легких потоков, или сформулирую по другому, зачем он может быть нужен?

Он много зачем может быть нужен :-) И уж точно он может быть (но не в Haskell).

Для примера можно глянуть Common LISP и его special variables.

Пример использования: я знаю, что в потоках (в терминах haskell) могут быть нужны блоки памяти, в которых будет делаться некоторая низкоуровневая работа. Например, форматирование числа в base8 или прием данных из сети. Если есть быстрый доступ к TLS, то просто выделяется блок памяти и с ним делают что нужно. Причем выделяется не более одного на haskell поток и не нужно делать синхронизацию вручную. Если легковесный поток когда-либо будет передаваться в другой поток в терминах OS, то там все равно будет своя синхронизация, которой будет достаточно. Если пытаться делать этот же трюк имеющимися средствами, то получится тормозное уродство.

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

Если есть быстрый доступ к TLS, то просто выделяется блок памяти и с ним делают что нужно

Почему нельзя выделить блок памяти как IOUArray?

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

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

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

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

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

И совсем уж не понимаю проблему чтения данных из сети при наличии всех streaming iteratees-like библиотек типа iteratees, conduit, и т.д.

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

Почему нельзя выделить блок памяти как IOUArray?

Можно, но прийдется таскать его повсюду. А желательно не таскать.

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

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

Проблема в том, что это можно реализовать только медленными способами. А именно, иметь где-то IORef или что-то похожее с Map TreadID a. И работать с этой Map. Это - медленно. Очень медленно. Если знаете способ быстрее - поделитесь пожалуйста.

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

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

Да, прекрасно. Как гарантируется то, что он не расшаривается. И как факт его существования скрыть внутри реализации, чтобы пользователю не приходилось создавать его, протаскивать во всех случаях использования и потом уничтожать? Можно пример?

И совсем уж не понимаю проблему чтения данных из сети при наличии всех streaming iteratees-like библиотек типа iteratees, conduit, и т.д.

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

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

А можно агрументацию с чего бы вдруг IORef это медленно?

Плюс можно вполне через замыкание, можно параметром внешней функции, как тот же IORef держать так и мутабельный буфер.

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

Да, прекрасно. Как гарантируется то, что он не расшаривается. И как факт его существования скрыть внутри реализации, чтобы пользователю не приходилось создавать его, протаскивать во всех случаях использования и потом уничтожать? Можно пример?

повторюсь: StateT, ST (появляются ограничения), замыкание, параметр внешней функции.

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

как я понимаю, там там идёт выделение освобождение (если компилятор не делает чудо), но нужно помнить, что это выделение освобождение, не обозначает тяжелых системных вызовов. И в идеале (в зависимости от последующей обработки) работа идёт за O(1) по памяти.

«игрушки», это обоснованное утвеждение или опять для красного словца?

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

Да, прекрасно. Как гарантируется то, что он не расшаривается. И как факт его существования скрыть внутри реализации, чтобы пользователю не приходилось создавать его, протаскивать во всех случаях использования и потом уничтожать? Можно пример?

повторюсь: StateT, ST (появляются ограничения), замыкание, параметр внешней функции.

Пример можно?

Вот что хочу видеть (в псевдокоде)

tls :: TLS Int
tls = liftTLS 13

showValue :: IO ()
showValue = do
  v <- getTLS tls
  putStrLn $ show v

foo :: IO ()
foo = do
  showValue -- shows 3 as it was forked when TLS variable was assigned to 3 in the parent thread at the time of spawning
  setTLS tls 6
  showValue -- shows 6

main = do
  showValue -- shows 13 (default value)
  withTLS tls 5 showValue -- shows 5 as TLS variable was temporarily re-assigned
  showValue -- shows 13 as previous value has been returned
  withTLS tls 3 $ fork foo
  sleep 100
  showValue -- show 13 as forked thread has no impact
  sleep 300
  showValue -- show 13, same reason

Как это сделать, предлагаемыми методами? И да, надо чтобы было быстро. Желательно не более трёх-четырёх ассемблерных инструкций.

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

как я понимаю, там там идёт выделение освобождение (если компилятор не делает чудо), но нужно помнить, что это выделение освобождение, не обозначает тяжелых системных вызовов. И в идеале (в зависимости от последующей обработки) работа идёт за O(1) по памяти.

«игрушки», это обоснованное утвеждение или опять для красного словца?

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

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

А можно агрументацию с чего бы вдруг IORef это медленно?

IORef сам по себе может и не медленно работает.

А вот если надо из множества потоков трогать IORef (Map ThreadID a) то уже будет небыстро.

Ну гляньте ради Бога на то, что GHC генерит. Если есть TLS, то доступ к переменной в нём реально сделать _очень_ быстрым. Почти таким же быстрым, как и создание boxed Int. Я очень надеюсь, что Вам очевидно, что вытаскивание из IORef а затем lookup и выяснение, не Nothing ли вернули, занимает несколько больше времени.

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

Вот что хочу видеть

Это всё делается с помощью

glob :: IORef Int
{-# NOINLINE glob #-}
glob = unsafePerformIO $ newIORef 13

только в foo надо новый IORef передавать, а не ожидать, что оно замкнёт синтаксическую (!) tls, это нонсенс в хаскеле.

Впрочем, если убрать glob в main и отдавать её явно всем функциям, то хуже от этого не станет, но одним хаком станет меньше.

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

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

абсолютно не применяя мозга:

import Control.Concurrent                                                          
import Control.Monad.State                                                         
import Control.Monad.IO.Class                                                      
                                                                                   
local x f = do -- bracket get put (\_ -> put x >> f)                               
    x' <- get                                                                      
    put x                                                                          
    r <- f                                                                         
    put x'                                                                         
    return r                                                                       
                                                                                   
showValue = get >>= liftIO . print                                                 
                                                                                   
runTLS x f = runStateT f x                                                         
                                                                                   
foo = do                                                                           
    showValue                                                                      
    put 6                                                                          
    showValue                                                                      
                                                                                   
main = runTLS 13 $ do                                                              
    showValue                                                                      
    local 5 showValue                                                              
    showValue                                                                      
    liftIO $ forkIO $ runTLS 3 foo >> return ()                                    
    liftIO $ threadDelay 100                                                       
    showValue                                                                      
    liftIO $ threadDelay 300                                                       
    showValue                                                                      

asm выхлоп: http://paste.lugons.org/show/2008/

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

Это же модель состояния, там не применяется ни IORef, ни MVar.

но указанное поведение там выполняется, за исключением того, что создаётся новый объект при обновлении состояния. Вообще можно сделать аналог Reader, с состоянием IORef a, хотя в этом смысла нет совершенно. А если так уж хочется мутабельности, то я так понимаю, что нужно выделять нужный блок и туда делать unsafe запись и чтение.

И даже не понятно, хорошо это или плохо :)

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

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

/me придумал, как сделать красиво, но боюсь моё haskell-фу слишком низко для этого.

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

можно сделать аналог Reader, с состоянием IORef a

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

module Control.Monad.RefEnv where

import Data.IORef
import Control.Applicative
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State hiding ( modify )

-- | As @local@ but for @MonadState@.
with :: MonadState x m => x -> m a -> m a
with x m = put x >> m

-- | Run a monad transformer @t@ in a monad @m@ (reduce one layer in app stack).
class RunT t m where
  runT :: t m a -> m a

-- | Create a new monad transformer layer in app stack.
new :: (Monad m,  MonadTrans t, RunT t' m) => t' m a -> t m a
new = lift . runT

-- | Reference/Environment (i.e. State/Reader) transformer.
newtype RefEnvT r e m a = RefEnvT { runRefEnvT :: r -> e -> m a }

instance MonadTrans (RefEnvT r e) where
  lift m = RefEnvT $ \_ _ -> do { x <- m ; x `seq` return x }

instance Monad m => Monad (RefEnvT r e m) where
  return = lift . return
  RefEnvT m >>= f = RefEnvT $ \r e -> do { x <- m r e ; runRefEnvT (f x) r e }
  RefEnvT m >> RefEnvT m' = RefEnvT $ \r e -> m r e >> m' r e

instance Monad m => Functor (RefEnvT r e m) where
  fmap = liftM

instance Monad m => Applicative (RefEnvT r e m) where
  pure = return
  (<*>) = ap

instance (Alternative m, Monad m) => Alternative (RefEnvT r e m) where
  empty = lift empty
  RefEnvT m <|> RefEnvT n = RefEnvT $ \r e -> m r e <|> n r e

instance MonadPlus m => MonadPlus (RefEnvT r e m) where
  mzero = lift mzero
  RefEnvT m `mplus` RefEnvT n = RefEnvT $ \r e -> m r e `mplus` m r e

instance MonadIO (RefEnvT r e IO) where
  liftIO = lift

instance Monad m => MonadReader e (RefEnvT r e m) where
  ask = RefEnvT $ \_ e -> return e
  local f (RefEnvT m) = RefEnvT $ \r e -> m r (f e)

type IORefEnvT x e = RefEnvT (IORef x) e IO

instance MonadIO m => MonadState x (RefEnvT (IORef x) e m) where
  get = RefEnvT $ \r _ -> liftIO $ readIORef r
  put x = RefEnvT $ \r _ -> liftIO $ writeIORef r x

modify :: (x -> x) -> IORefEnvT x e ()
modify f = RefEnvT $ \r _ -> liftIO $ modifyIORef r f

instance RunT (RefEnvT (IORef x) e) IO where
  runT t = do
    r <- newIORef undefined
    runRefEnvT t r undefined

-- * Example.

t1 :: IORefEnvT Int String ()
t1 = local (const "read-only") $ with 0 $ do
  ask >>= lift . putStrLn
  get >>= lift . print
  put 2
  get >>= lift . print
  new $ with 500 foo
  modify (* 5)
  get >>= lift . print
  where
    foo :: IORefEnvT Int () ()
    foo = get >>= lift . print

-- > runT t1
-- read-only
-- 0
-- 2
-- 500
-- 10

Получается Reader для локального окружения с только-чтением и State для локального мутабельного (через IORef) окружения. Можно ещё для MVar и STM сделать инстансов. C помощью new . with как раз создаётся ещё один слой в стеке в котором создаётся новый IORef для очередной переменной хранящей локальное состояние обновляемое по put / get.

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

просто офигенно..

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

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

Точно. А runT всё-таки нужно оставить как было, или с data-default сделать:

instance (Default x, Default e) => RunT (RefEnvT (IORef x) e) IO where
  runT t = do
    r <- newIORef def
    runRefEnvT t r def
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

и для любителей самому управлять памятью и смотреть asm можно добавить ещё один инстанс. Правда для полноценного кода ещё modify в класс нужно будет обернуть, чтобы инстансы соотв можно было добавить.

type PtrEnvT x e = RefEnvT (Ptr x) e IO

instance (MonadIO m,Storable x) => MonadState x (RefEnvT (Ptr x) e m) where
  get = RefEnvT $ \r _ -> liftIO $ peek r
  put x = RefEnvT $ \r _ -> liftIO $ poke r x

-- instance (MonadState m) => MonadModify x (RefEnvT (Ptr x) e m) where
--modify f = RefEnvT $ \r _ -> liftIO $ peek r >>= poke r . f

instance (Storable x) => RunT (RefEnvT (Ptr x) e) IO where                         
  runT t = bracket malloc free (\p -> runRefEnvT t p undefined) 

в идеале в этот подход можно расширить до хранения буфера, но это уже совсем не путь haskell.

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

или просто в разных файлах делать и экспортировать в каждом свой метод.

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

Если этот IORef не виден извне (локальный в пределах модуля), то неясно, как это поможет получать доступ к значениям, привязанным к потокам. Ведь любой поток, обращающийся к IORef будет работать с одним и тем же значением. А нужно, чтобы они все видели только свои.

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

C другим примером пишется

newT :: (RunT t m, MonadTrans t', Monad m') => (m a -> m' b) -> t m a -> t' m' b
newT f = lift . f . runT

forkT :: (RunT t IO, MonadTrans t') => t IO a -> t' IO ThreadId
forkT = newT (forkIO . void)

fork :: (RunT t IO, MonadTrans t) => t IO a -> t IO ThreadId
fork = forkT

так что

t2 :: IORefEnvT Int String ()
t2 = local (const "read-only") $  do
  ask >>= lift . putStrLn
  get >>= lift . print
  put 2
  get >>= lift . print
  s <- ask
  fork $ local (const (s ++ "2")) $ with 500 $ do
    lift $ threadDelay 500000
    ask >>= lift . putStrLn
    get >>= lift . print
  newT forkIO foo
  modify (* 5)
  get >>= lift . print
  lift $ threadDelay 2000000
  modify (+ 7)
  get >>= lift . print
  where
    foo :: IORefEnvT Int () ()
    foo = do
      lift $ threadDelay 1000000
      get >>= lift . print

-- > runT t2
-- read-only
-- 0
-- 2
-- 10
-- read-only2
-- 500
-- 0
-- 17

у каждого потока своя IORef недоступная из других потоков и доступная для чтения / изменения по get / put. При этом написать fork в IORefEnvT не получается никак кроме через newT (или подобным образом), то есть fork автоматом будет создавать новую локальную IORef.

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

Этот пример не эквивалентен.

Данные жестко привязанны к сигнатуре функций. Сигнатура foo явным образом показывает, что она работает со скрытым состоянием определенного типа.

Да, можно сказать, что это типа как бы TLS. Но это - уродливый TLS, что мало чем лучше MVar (Map ThreadId a). Даже по-сути хуже, потому что:

1. тот же MVar (Map ThreadId a) можно спрятать в каком-то модуле, да так, что о нём никто ничего не будет знать. И все будет работать. В Вашем же примере про «a» знают все, т.к. оно должно быть частью сигнатур.

2. этих MVar (Map ThreadId a) может быть много и разных типов. В вашем же примере это значит, что надо при добавлении еще одной такой TLS переменной весь код перелопатить и вместо m a сигнатуры примут вид типа m (a, b, c, d) ещё чего похлеще. Работать с этим будет не особо весело. Плюс, это поломает API.

3. особенно забавно будет работать пункт №2, когда есть несколько библиотек, использующих тот же самый подход, и нужно ими пользоваться одновременно. Объединять m a, m b и m c в m (a, b, c) - реальная, но зело непродуктивная задача.

В общем, основная претензия - TLS переменная не может быть инкапсулирована, и это решение является неудобным в использовании.

P.S. В asm выхлопе много буков и нет привязки к названиям функций. :) Зато постоянно используются black holes. Подозреваю, что они нужны как раз для реализации put / get. А black holes и всякие там «call newCAF» - штуки не быстрые. Быстро это что-то типа «глянуть по извесному адресу таблицу TLS, взять там адрес переменной и работать с ней. Причем если она - unboxed, то не мутить ничего с boxing».

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

Сигнатура foo явным образом показывает, что она работает со скрытым состоянием определенного типа.

Потому что так и задумывалось - с mt обычно так делают. Например, IORefEnvT явно выделяет слой в стеке приложения в котором существует локальная для потока IORef, вне этого слоя её не существует, поэтому спутать слои нельзя (типы не позволят). Так же как IO выделяет слой приложения на котором возможны любые IO операции, а вне его - не возможны. Можно предъявить претензии к IO, мол, почему явным образом показывается, что его функции работают с императивными конструкциями возвращающими значения определённого типа, и что IO хочется делать «просто так». Просто так в хаскеле нельзя (это будет unsafePerformIO).

1. Про значение IORef знают все в данном потоке в данном слое IORefEnvT.

2. Это да. Тут одна IORef. Можно помещать в неё Dynamic, массив, кортеж или таблицу (Map Var x) (это уже медленно). То есть это специальное решение, не полный аналог top level mutable state да ещё и с thread-local storage.

3. Я не вполне понимаю проблему. (>>=) :: Monad m => m a -> (a -> m b) -> m b и может комбинировать m a и m b, как обычно и бывает в do блоке. newM позволяет комбинировать m a и m' b, а newT - t m a и t' m' b.

Зато постоянно используются black holes

В hello worde они тоже используются.

Быстро это что-то типа «глянуть по извесному адресу таблицу TLS, взять там адрес переменной и работать с ней. Причем если она - unboxed, то не мутить ничего с boxing».

Судя по вики про явные top level mutable state и thread-local storage думали не раз, но так ничего пока не придумали.

Было бы проще если бы можно было написать в файле как в GHCi:

args :: [String]
args <- getArgs

x :: IORef Int
x <- newIORef 0

y :: TLSRef Int
y <- newTLSRef 0

...

main :: IO ()
main = ...
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Потому что так и задумывалось - с mt обычно так делают. Например, IORefEnvT явно выделяет слой в стеке приложения в котором существует локальная для потока IORef, вне этого слоя её не существует, поэтому спутать слои нельзя (типы не позволят). Так же как IO выделяет слой приложения на котором возможны любые IO операции, а вне его - не возможны. Можно предъявить претензии к IO, мол, почему явным образом показывается, что его функции работают с императивными конструкциями возвращающими значения определённого типа, и что IO хочется делать «просто так». Просто так в хаскеле нельзя (это будет unsafePerformIO).

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

3. Я не вполне понимаю проблему. (>>=) :: Monad m => m a -> (a -> m b) -> m b и может комбинировать m a и m b, как обычно и бывает в do блоке. newM позволяет комбинировать m a и m' b, а newT - t m a и t' m' b.

ОК, буду думать дальше. Может это как-то и будет работать.

В hello worde они тоже используются.

Да, но это не делает чести GHC runtime. Потому что black holes там вообще не нужны.

Судя по вики про явные top level mutable state и thread-local storage думали не раз, но так ничего пока не придумали.

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

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

Интересно, что проблему можно было решить. Во-первых, ещё до принятия стандарта, в начале 90-ых, когда вводили монадическое IO, можно было расширить сам язык монадической связкой «<-» в top-level, это никак не ломает чистоту. И, во-вторых, когда вводилась конкурентность и писались соответствующие части рантайма, можно было ввести TLSRef, аналогично IORef. При наличии x <- newSomeRef для чистого кода x представляет собой чистое значение (адрес глобальной переменной), оно не ломает ссылочной прозрачности, так как остаётся одним и тем же, при попытке читать или писать этот адрес код автоматически попадает в IO.

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

Интересно, что проблему можно было решить. Во-первых, ещё до принятия стандарта, в начале 90-ых, когда вводили монадическое IO, можно было расширить сам язык монадической связкой «<-» в top-level, это никак не ломает чистоту. И, во-вторых, когда вводилась конкурентность и писались соответствующие части рантайма, можно было ввести TLSRef, аналогично IORef. При наличии x <- newSomeRef для чистого кода x представляет собой чистое значение (адрес глобальной переменной), оно не ломает ссылочной прозрачности, так как остаётся одним и тем же, при попытке читать или писать этот адрес код автоматически попадает в IO.

Можно было. Но удобство практического применения - не приоритет для развития haskell. Не их ли принцип «avoid success at all costs»? :-)

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

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

там нету потрохов модуля (во всяком случае в решении приведённом quasimoto), там есть интерфейс доступный на данном уровне.

П

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

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

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

1). бенчмарки в студию,

Бенчмарки чего?

Если это бенчмарк лишь возможных сейчас реализаций, то какой с этого толк?

Если это еще и бенчмарк оптимального варианта реализации TLS, то её сначала надо сделать. И это, мягко говоря, немало работы. Особенно для человека, что не знает потроха GHC как свои пять пальцев.

И главное ради чего? Чтобы показать очевидное, что пара MOV инструкций работает быстрее чем несколько MOV, callы и jmpы по заранее непредсказуемым адресам и прочее?

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

Спасибо. Действительно не так прочитал. ОК. Тогда что имеется в виду под O(1) по памяти? Если это просто оценка суммарного объема живых объектов - одно дело. Если это оценка количества раз, когда выделяется и освобождается объект - ситуация другая. У меня нет сомнений, что в нормально написанной библиотеке для работы с потоками потребление памяти будет O(1) в смысле суммарно используемой памяти. Но я не верю, что эти суперумные библиотеки не создают объектов на куче. А это создание объектов, что бы там не говорили адепты haskell, стоит очень дорого.

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

Если это бенчмарк лишь возможных сейчас реализаций, то какой с этого толк?

можно сравнить с аналогичными по функциональности сишными реализациями. Можно даже с более слабыми по функциональности.

Тогда что имеется в виду под O(1) по памяти?

_насколько я понимаю_ выделенной памяти будет не более O(1) не считая gc. Реально больше, но нужно помнить, что runtime тоже не дурак, и то, что выделение памяти под буффер в haskell это не обязательно тяжелые системные вызовы, плюс благодаря иммутабельности не происходит копирование данных туда-сюда как в тех же c/c++. Ещё есть Олеговские regions, которые вроде тоже в решение в этом направлении.

И ещё blackholes используется, для того, чтобы в многопоточном (имеются ввиду потоки OS) окружении одни и те же thunk-и не выполнялись несколько раз.

И последнее, ты вроде приводил ссылки на то, где реализованы те TLS, которые тебя устраивают, можешь привести ссылки на работы и/или реализацию?

P.S. ещё ты так и не сказал нафига TLS (для лёгких потоков нужно), я пока видел только статьи с эрланговыми lock-free структурами данных, которые явно использовали TLS.

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

runtime тоже не дурак, и то, что выделение памяти под буффер в haskell это не обязательно тяжелые системные вызовы

Кстати

$ ghc -main-is HelloWorld -o HelloWorld HelloWorld.hs
[1 of 1] Compiling HelloWorld       ( HelloWorld.hs, HelloWorld.o )
Linking HelloWorld ...
$ strace ./HelloWorld 2>&1 | wc -l
145
$ ./STraceTest
usage: ./STraceTest <number-of-buffers>
$ time strace ./STraceTest 1 -RTS 2>&1 | wc -l
145

real	0m0.016s
user	0m0.002s
sys	0m0.012s
$ time strace ./STraceTest 10 2>&1 | wc -l
145

real	0m0.016s
user	0m0.005s
sys	0m0.009s
$ time strace ./STraceTest 100 2>&1 | wc -l
145

real	0m0.018s
user	0m0.005s
sys	0m0.009s
$ time strace ./STraceTest 1000 2>&1 | wc -l
415

real	0m0.083s
user	0m0.037s
sys	0m0.037s
$ time strace ./STraceTest 5000 2>&1 | wc -l
6788

real	0m1.958s
user	0m1.260s
sys	0m0.558s
$ time strace ./STraceTest 10000 2>&1 | wc -l
27281

real	0m10.799s
user	0m7.760s
sys	0m2.356s
$ time strace ./STraceTest 1 +RTS -H150M -A2M -RTS 2>&1 | wc -l
264

real	0m0.027s
user	0m0.005s
sys	0m0.018s
$ time strace ./STraceTest 10 +RTS -H150M -A2M -RTS 2>&1 | wc -l
264

real	0m0.027s
user	0m0.004s
sys	0m0.019s
$ time strace ./STraceTest 100 +RTS -H150M -A2M -RTS 2>&1 | wc -l
264

real	0m0.028s
user	0m0.007s
sys	0m0.017s
$ time strace ./STraceTest 1000 +RTS -H150M -A2M -RTS 2>&1 | wc -l
324

real	0m0.105s
user	0m0.036s
sys	0m0.065s
$ time strace ./STraceTest 5000 +RTS -H150M -A2M -RTS 2>&1 | wc -l
734

real	0m1.009s
user	0m0.766s
sys	0m0.224s
$ time strace ./STraceTest 10000 +RTS -H150M -A2M -RTS 2>&1 | wc -l
7468

real	0m5.279s
user	0m4.068s
sys	0m1.017s
$ time strace ./STraceTest 10000 +RTS -H500M -A64M -RTS 2>&1 | wc -l
1554

real	0m3.645s
user	0m2.819s
sys	0m0.732s
$ ./STraceTest 1000 +RTS -H150M -A2M -sstderr -RTS
167167000
      36,462,352 bytes allocated in the heap
       1,346,296 bytes copied during GC
         649,832 bytes maximum residency (1 sample(s))
       1,199,696 bytes maximum slop
             156 MB total memory in use (1 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0         2 colls,     0 par    0.00s    0.00s     0.0025s    0.0033s
  Gen  1         1 colls,     0 par    0.00s    0.00s     0.0038s    0.0038s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    0.02s  (  0.06s elapsed)
  GC      time    0.00s  (  0.01s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    0.03s  (  0.07s elapsed)

  %GC     time      16.7%  (13.0% elapsed)

  Alloc rate    1,458,727,476 bytes per MUT second

  Productivity  83.3% of total user, 36.8% of total elapsed

$ ./STraceTest 10000 +RTS -H150M -A2M -sstderr -RTS
166716670000
   3,604,066,872 bytes allocated in the heap
       9,306,680 bytes copied during GC
     286,349,568 bytes maximum residency (7 sample(s))
      19,792,128 bytes maximum slop
             434 MB total memory in use (23 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1457 colls,     0 par    1.38s    1.41s     0.0010s    0.0034s
  Gen  1         7 colls,     0 par    0.02s    0.03s     0.0037s    0.0054s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    2.68s  (  3.10s elapsed)
  GC      time    1.40s  (  1.44s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    4.09s  (  4.54s elapsed)

  %GC     time      34.3%  (31.6% elapsed)

  Alloc rate    1,342,005,393 bytes per MUT second

  Productivity  65.7% of total user, 59.2% of total elapsed

$ ./STraceTest 10000 +RTS -H500M -A64M -sstderr -RTS
166716670000
   3,604,066,872 bytes allocated in the heap
       5,558,104 bytes copied during GC
     368,689,560 bytes maximum residency (3 sample(s))
      19,789,000 bytes maximum slop
             594 MB total memory in use (17 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0        27 colls,     0 par    0.07s    0.07s     0.0025s    0.0090s
  Gen  1         3 colls,     0 par    0.02s    0.03s     0.0095s    0.0101s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    2.71s  (  3.27s elapsed)
  GC      time    0.09s  (  0.10s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    2.80s  (  3.37s elapsed)

  %GC     time       3.2%  (2.9% elapsed)

  Alloc rate    1,328,155,516 bytes per MUT second

  Productivity  96.8% of total user, 80.5% of total elapsed
{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}

module STraceTest where

import Prelude hiding ( catch )
import Data.Maybe
import Data.Array.IO
import Control.Exception
import Control.Applicative
import System.Environment
import System.Exit

foldMArray :: (Num i, Ix i, MArray a e m) => Maybe i -> Maybe i -> r -> (r -> e -> r) -> a i e -> m r
foldMArray a_ b_ z f arr = getBounds arr >>= go where
  go (m, n) = go_ 0 z where
    a = fromMaybe m a_
    b = fromMaybe n b_
    go_ !i !acc | i > n || i > b || i < m || i < a = return acc
                | otherwise = readArray arr i >>= go_ (i + 1) . f acc
-- ^
--   !i !acc
-- 
-- makes it x5 faster and concise.
--

unfoldMArray :: (Num i, Ix i, MArray a e m) => i -> i -> (i -> e) -> m (a i e)
unfoldMArray m n f = newArray_ (m, n) >>= go m where
  go !i !arr | i > n = return arr
             | otherwise = writeArray arr i (f i) >> go (i + 1) arr

newBuf :: Int -> IO (IOUArray Int Int)
newBuf m = unfoldMArray 0 m id

newBufs :: Int -> IO [IOUArray Int Int]
newBufs = mapM newBuf . enumFromTo 1

sumBuf :: IOUArray Int Int -> IO Integer
sumBuf = foldMArray Nothing Nothing 0 (\acc e -> acc + toInteger e)

sumBufs :: [IOUArray Int Int] -> IO Integer
sumBufs = fmap sum . mapM sumBuf
-- ^
--   sumBufs = fmap (sum . map sum) . mapM getElems
-- 
-- creates TOO much intermediate lists.
-- 

main :: IO ()
main = tolerant (failed "usage: ./STraceTest <number-of-buffers>") $
  read . head <$> getArgs >>= newBufs >>= sumBufs >>= print

tolerant :: IO a -> IO a -> IO a
tolerant g f = catch f $ \(_ :: SomeException) -> g

failed :: String -> IO a
failed message = putStrLn message >> exitFailure

VM сама себе ОС со своим MM (аллокатор и GC), IO менеджером и планировщиком, так что хаскельные аллокации, сборки и форки могут вообще не делать системных вызовов (но IO должно). С другой стороны, должна быть причина по которой при большом количестве буферов начинает расти количество этих вызовов.

благодаря иммутабельности не происходит копирование данных туда-сюда как в тех же c/c++.

А это в каком смысле?

quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto
$ strace ./STraceTest 1 +RTS -H1G -A128M -RTS 2>&1 | wc -l
959
$ strace ./STraceTest 10 +RTS -H1G -A128M -RTS 2>&1 | wc -l
959
$ strace ./STraceTest 100 +RTS -H1G -A128M -RTS 2>&1 | wc -l
957
$ strace ./STraceTest 1000 +RTS -H1G -A128M -RTS 2>&1 | wc -l
970
$ strace ./STraceTest 2000 +RTS -H1G -A128M -RTS 2>&1 | wc -l
1006
$ strace ./STraceTest 3000 +RTS -H1G -A128M -RTS 2>&1 | wc -l
1311
$ strace ./STraceTest 4000 +RTS -H1G -A128M -RTS 2>&1 | wc -l
1394
$ strace ./STraceTest 5000 +RTS -H1G -A128M -RTS 2>&1 | wc -l
1485
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

благодаря иммутабельности не происходит копирование данных туда-сюда как в тех же c/c++.

А это в каком смысле?

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

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

_насколько я понимаю_ выделенной памяти будет не более O(1) не считая gc.

Ну так в GC-то и 99% тормозов.

Реально больше, но нужно помнить, что runtime тоже не дурак, и то, что выделение памяти под буффер в haskell это не обязательно тяжелые системные вызовы,

Я скажу даже более, это почти никогда не системные вызовы. Ну и что? Вы смотрели на реализацию? Можете сходу сказать как она работает? А я могу. Сначала смотрят, есть ли место в активном сегменте под данные (арифметика + ветвление). Если все хорошо, то смещают указатель и заполняют память. Если не очень - выделяют новый сегмент (в 4К обычно) из мегасегмента (где-то порядка мегабайта) и проверяют - не сменить ли контекст, не сделать ли GC, и т.д. Если нет мегасегмента - выделяют новый (тут уже идёт системный вызов). Если Вам кажется, что даже в оптимальном случае оно работает быстро, то пока уже креститься.

плюс благодаря иммутабельности не происходит копирование данных туда-сюда как в тех же c/c++.

Ага, щас. Но не забывайте о том, что из-за этого, там где можно сделать in-place update, хаскель весело создает реплику с дополнительными изменениями. Так что «те же яйца, только сбоку».

Ещё есть Олеговские regions, которые вроде тоже в решение в этом направлении.

Где можно почитать?

И ещё blackholes используется, для того, чтобы в многопоточном (имеются ввиду потоки OS) окружении одни и те же thunk-и не выполнялись несколько раз.

Ага. И они очень нужны даже в Hello World. Просто GHC настолько умен, что а) не понимает, что вычисление все равно произойдет, и лучше его сделать сходу б) не понимает, что некоторые величины локальны по отношению к потоку, и не надо извращаться с black holes.

И последнее, ты вроде приводил ссылки на то, где реализованы те TLS, которые тебя устраивают, можешь привести ссылки на работы и/или реализацию?

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

Вообще было бы здорово, чтобы TLS в haskell были. Но у меня есть подозрение, что их нельзя выразить в его системе типов.

P.S. ещё ты так и не сказал нафига TLS (для лёгких потоков нужно), я пока видел только статьи с эрланговыми lock-free структурами данных, которые явно использовали TLS.

Это-то как раз я говорил. Можно держать «черновики» типа небольших блоков памяти для форматирования чисел или приёма/отправки данных, при этом не долбая GC, и не заморачиваясь с синхронизацией.

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

Если Вам кажется, что даже в оптимальном случае оно работает быстро, то пока уже креститься.

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

Где можно почитать?

где-то тут (http://okmij.org/ftp/), я с этим в рассылке сталкивался, но не стал копать глубже за ненадобностью.

Ага. И они очень нужны даже в Hello World. Просто GHC настолько умен, что а) не понимает, что вычисление все равно произойдет, и лучше его сделать сходу б) не понимает, что некоторые величины локальны по отношению к потоку, и не надо извращаться с black holes.

ух-ты мне кажется, что для нетривиальных случаев «понимать, что вычисление всё равно произойдёт», окажется сложнее самой программы :). Тут гораздо проще повесить всё на программиста, который использует bang pattern или par pseq, там, где это нужно. Б). формально никто не запрещает вычислять созданные санки всеми процессорами, даже в случае если основной поток один (тут есть проблема в обеспечении достаточной гранулярности)

Вообще было бы здорово, чтобы TLS в haskell были. Но у меня есть подозрение, что их нельзя выразить в его системе типов.

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

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

Ну так в GC-то и 99% тормозов.

Это только если GC работает много в процентном отношении ко времени работы программы (чего быть не должно).

Можете сходу сказать как она работает?

Хуже чем ядерный аллокатор?

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

Он же не знает - одна там ссылка на объект или не одна, чтобы сделать обновление in-place. Мне вот интересно, как работает обновление поля BigStruct в IORef BigStruct.

Где можно почитать?

Олеговские это http://okmij.org/ftp/Haskell/regions.html, ещё регионы используются в MLKit и Cyclone, почитать можно в ATTAPL (есть некая связь между регионами и линейной логикой/субструктурными типами, самая неограниченная по типам форма приводит к необходимости организации памяти в куче с GC, самая ограниченная - к организации памяти на стеке (что намного проще), линейная это что-то посередине - в куче но с поддержкой всегда только одной ссылки на объект, в таких случаях можно обойтись без GC).

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

С самыми простыми зависимыми типами можно просто индексировать IO с помощью ThreadId, то есть индексировать тип числами (термами), для этого нужны type level числа.

Например, в агде:

Type = Set

ThreadId = ℕ

record TLSRef (_ : ThreadId) (A : Type) : Type where

record IO (_ : ThreadId) (A : Type) : Type where

writeTLSRef : ∀ {tid A} → TLSRef tid A → A → IO tid A
writeTLSRef _ _ = record {}

readTLSRef : ∀ {tid A} → TLSRef tid A → IO tid A
readTLSRef _ = record {}

-- writeTLSRef {5} : TLSRef 5 _36 → _36 → IO 5 _36
-- readTLSRef {7} : TLSRef 7 _39 → IO 7 _39

С типами проблем никаких. В хаскеле:

import Data.TypeLevel.Num
import Data.IORef

newtype TLSRef tid a = TLSRef (IORef a)

newtype IIO tid a = IIO (IO a) -- deriving ( Functor, Monad, etc.)

writeTLSRef :: Nat tid => TLSRef tid a -> a -> IIO tid a
writeTLSRef _ _ = undefined

readTLSRef :: Nat tid => TLSRef tid a -> IIO tid a
readTLSRef _ = undefined

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

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

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

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

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

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

может ты мне, дураку, объяснишь, зачем TLS на greenthread реально нужен.

За тем же зачем глобальные переменные в других языках и, например, специальные переменные в Common Lisp. Теоретически в них нет ничего плохого, у них хорошая семантика и т.п. Практически они удобны в структурировании программ (тут уже без разницы, лёгкие потоки или нет).

Цитируя хаскельную вики:

The idea of mutable global variables is theoretically sound, so shouldn't there be a theoretically sound way to create them?

и перефразируя:

The idea of thread-local storage is theoretically sound, so shouldn't there be a theoretically sound way to create them?

если выделять много объектов, то это ещё и какой-то словарь будет

Вот нужен не словарь в IORef (эмуляция переменных времени выполнения), а обычные переменные:


import Data.IORef
import System.IO.Unsafe
import Control.Monad
import Control.Concurrent

-- * Simplified interface.

type TLSRef a = IORef a

new :: a -> IO (TLSRef a)
new = newIORef

unsafeNew :: a -> TLSRef a
unsafeNew = unsafePerformIO . newIORef

(=:) :: TLSRef a -> a -> IO ()
(=:) = writeIORef

get :: TLSRef a -> IO a
get = readIORef

copy :: TLSRef a -> IO (TLSRef a)
copy ref = get ref >>= new

-- * Example.

myParamA :: TLSRef Int
-- 
-- pseudocode:
-- 
--   myParamA <- 3
--
-- generates:
-- 
{-# NOINLINE myParamA #-}
myParamA = unsafeNew 3

myParamB :: TLSRef Int
-- 
-- pseudocode:
-- 
--   myParamB <- 5
--
-- generates:
-- 
{-# NOINLINE myParamB #-}
myParamB = unsafeNew 5

foo :: IO ()
foo = do
  forkIO $ do
    print =<< liftM2 (+) (get myParamA) (get myParamB)
    myParamA <- copy myParamA -- generated, copy-on-write + lexical shadowing
    myParamA =: 4
    myParamB <- copy myParamB -- generated, again
    myParamB =: 6
    print =<< liftM2 (+) (get myParamA) (get myParamB)
  threadDelay 1000000
  print =<< liftM2 (+) (get myParamA) (get myParamB)

-- > foo
-- 8
-- 10
-- 8

TLS + глобальное мутабельное состояние.

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

Ну, глобальное мутабельное окружение уже работает в GHCi, я не думаю что это трудно сделать в *.hs/*.lhs в виде очередного расширения компилятора. TLS можно пытаться эмулировать на основе IORef в compile-time.

вышеприведённая прослойка видится мне отличным решением

Которая State/Reader? Во-первых, это обвёртка - обычные переменные должны жить в IO. Во-вторых, можно делать put someThing, someThing <- get, но не put var1 someThing1, put var2 someThing2, ..., someThing1 <- get var1, someThing2 <- get var2, ...

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

Пример с индексированным IO в агде:

module IIO where

module Haskell/Data/Unit where

  postulate
    Unit : Set
    unit : Unit

  {-# COMPILED_TYPE Unit () #-}
  {-# COMPILED unit () #-}

module Haskell/Data/Integer where

  postulate
    Int : Set
    Integer : Set
    z : Integer
    s : Integer → Integer
    toInt : Integer → Int
    nfold : {A : Set} → A → (A → A) → Integer → A

  {-# COMPILED_TYPE Integer Integer #-}
  {-# COMPILED_TYPE Int Int #-}
  {-# COMPILED z 0 #-}
  {-# COMPILED s (+ 1) #-}
  {-# COMPILED toInt fromIntegral #-}
  {-# IMPORT IIO #-}
  {-# COMPILED nfold (const IIO.nfold) #-}

module Haskell/System/IO where

  open Haskell/Data/Unit
  open Haskell/Data/Integer

  postulate
    IO : Set → Set
    return : {A : Set} → A → IO A
    _>>=_ : {A B : Set} → IO A → (A → IO B) → IO B
    print : Integer → IO Unit

  {-# BUILTIN IO IO #-}
  {-# COMPILED_TYPE IO IO #-}
  {-# COMPILED return (\_ a -> return a) #-}
  {-# COMPILED _>>=_ (\_ _ a f -> a >>= f) #-}
  {-# COMPILED print print #-}

module Haskell/Data/IORef where

  open Haskell/Data/Unit
  open Haskell/System/IO

  postulate
    IORef : Set → Set
    newIORef : {A : Set} → A → IO (IORef A)
    writeIORef : {A : Set} → IORef A → A → IO Unit
    readIORef : {A : Set} → IORef A → IO A

  {-# IMPORT Data.IORef #-}
  {-# COMPILED_TYPE IORef Data.IORef.IORef #-}
  {-# COMPILED newIORef (const Data.IORef.newIORef) #-}
  {-# COMPILED writeIORef (const Data.IORef.writeIORef) #-}
  {-# COMPILED readIORef (const Data.IORef.readIORef) #-}

module Haskell/Control/Concurrent where

  open Haskell/Data/Unit
  open Haskell/Data/Integer
  open Haskell/System/IO

  postulate
    ThreadId : Set
    forkIO : IO Unit → IO ThreadId
    threadDelay : Int → IO Unit
    threadIdToInteger : ThreadId → Integer

  {-# IMPORT Control.Concurrent #-}
  {-# COMPILED_TYPE ThreadId Control.Concurrent.ThreadId #-}
  {-# COMPILED forkIO Control.Concurrent.forkIO #-}
  {-# COMPILED threadDelay Control.Concurrent.threadDelay #-}
  {-# IMPORT IIO #-}
  {-# COMPILED threadIdToInteger IIO.threadIdToInteger #-}

open import Function
open import Data.Nat

open Haskell/Data/Unit
open Haskell/Data/Integer

fromInteger : Integer → ℕ
fromInteger = nfold 0 suc

integer : ℕ → Integer
integer 0 = z
integer (suc m) = s $ integer m

ThreadId : Set
ThreadId = ℕ

record IO {tid : ThreadId} (A : Set) : Set where
  constructor io
  field run : Haskell/System/IO.IO A

open IO

Main : Set → Set
Main = IO {0}

return : {tid : ThreadId} {A : Set} → A → IO {tid} A
return = io ∘ Haskell/System/IO.return

infixl 1 _>>=_
_>>=_ : {tid : ThreadId} {A B : Set} → IO {tid} A → (A → IO {tid} B) → IO {tid} B
io a >>= f = io $ Haskell/System/IO._>>=_ a $ run ∘ f

infixl 1 _,_
_,_ : {tid : ThreadId} {A B : Set} → IO {tid} A → IO {tid} B → IO {tid} B
a , b = a >>= const b

bind : {tid : ThreadId} {A B : Set} → IO {tid} A → (A → IO {tid} B) → IO {tid} B
bind = _>>=_

syntax bind e₁ (λ x → e₂) = x ← e₁ ! e₂

print : {tid : ThreadId} → ℕ → IO {tid} Unit
print = io ∘ Haskell/System/IO.print ∘ integer

record Ref {tid : ThreadId} (A : Set) : Set where
  constructor ref
  field getIORef : Haskell/Data/IORef.IORef A

open Ref

new : {tid : ThreadId} {A : Set} → A → IO {tid} (Ref {tid} A)
new x = io $ Haskell/System/IO._>>=_ (Haskell/Data/IORef.newIORef x) $ Haskell/System/IO.return ∘ ref

write : {tid tid′ : ThreadId} {A : Set} → Ref {tid} A → A → IO {tid′} Unit
write (ref r) = io ∘ Haskell/Data/IORef.writeIORef r

writeLocal : {tid : ThreadId} {A : Set} → Ref {tid} A → A → IO {tid} Unit
writeLocal = write

read : {tid tid′ : ThreadId} {A : Set} → Ref {tid} A → IO {tid′} A
read = io ∘ Haskell/Data/IORef.readIORef ∘ getIORef

readLocal : {tid : ThreadId} {A : Set} → Ref {tid} A → IO {tid} A
readLocal = read

copy : {tid tid′ : ThreadId} {A : Set} → Ref {tid} A → IO {tid′} (Ref {tid′} A)
copy (ref r) = io $ Haskell/System/IO._>>=_ (Haskell/System/IO._>>=_ (Haskell/Data/IORef.readIORef r) Haskell/Data/IORef.newIORef) $ Haskell/System/IO.return ∘ ref

fork : {tid : ThreadId} → IO {suc tid} Unit → IO {tid} ThreadId
fork (io a) = io $ Haskell/System/IO._>>=_ (Haskell/Control/Concurrent.forkIO a) $ Haskell/System/IO.return ∘ fromInteger ∘ Haskell/Control/Concurrent.threadIdToInteger

delay : {tid : ThreadId} → ℕ → IO {tid} Unit
delay = io ∘ Haskell/Control/Concurrent.threadDelay ∘ toInt ∘ integer
{-# LANGUAGE UnliftedFFITypes, MagicHash #-}

module IIO where

import GHC.Base
import GHC.Conc.Sync
import Foreign.C.Types

foreign import ccall unsafe "rts_getThreadId" getThreadId :: ThreadId# -> CInt

threadIdToInteger :: ThreadId -> Integer
threadIdToInteger tid = toInteger $ getThreadId (id2TSO tid) where
  id2TSO :: ThreadId -> ThreadId#
  id2TSO (ThreadId t) = t

nfold :: a -> (a -> a) -> Integer -> a
nfold z _ 0 = z
nfold z s n = z `seq` nfold (s z) s (n - 1)

То есть IO и IORef тут не просто * -> *, а ThreadId -> Type -> Type - каждый слой IO «знает» номер своего треда, так же как и каждая IORef. Получается, что все вычисления в IO и все переменные привязаны к тредам на уровне типов, поэтому разные вещи касающиеся локальности можно в типах же контролировать. Тип Main создаёт тип IO с номером 0, функции return и _>>=_ могут комбинировать вычисления только с постоянным tid, так что вычисления разных по задумке тредов не смогут смешаться. Функция new создаёт переменную привязанную ровно к тому же треду, что и слой IO в котором эта переменная будет существовать. write и read могут писать и читать как в местные для треда переменные, так и в переменные других тредов доступные из скопа. writeLocal и readLocal - только в переменные того треда в котором они вызываются (так как установлено равенство для tid и tid'). copy может копировать локальную переменную одного треда, создавая локальную переменную в другом. Наконец, fork в данном слое IO создаёт новый слой IO номер которого на единицу больше.

Пример (do нотации в агде нету, так что не очень вменяемо):

main : Haskell/System/IO.IO Unit
main = run subMain where
  subMain : Main Unit
  subMain =
    r ← new 42
    ! read r >>= print -- 42
    , fork
      ( r′ ← copy r
        ! read r′ >>= print -- 42
        , write r′ 77
        , writeLocal r′ 77 -- Ok
     -- , writeLocal r 77 -- No
        , readLocal r′ >>= print -- Ok, 77
     -- , readLocal r >>= print -- No
        , read r′ >>= print -- 77
        , read r >>= print -- 42
      )
    , fork
      ( r ← copy r -- shadowing, maybe "local r" where "local" is syntactic form
        ! delay 500000
        , read r >>= print -- 42
        , writeLocal r 88
        , write r 88
        , readLocal r >>= print -- 88
        , read r >>= print -- 88
      )
    , delay 1000000
    , readLocal r >>= print -- 42

(тут в IORef хранятся агдовские ℕ). Важно, что ThreadId у типов это неявный (implicit) аргумент, поэтому правильные значения выводятся автоматически, на самом деле это эквивалентно

main : Haskell/System/IO.IO Unit
main = run subMain where
  subMain : IO {0} Unit
  subMain =
    r ← new {0} 42
    ! read {0} r >>= print {0}
    , fork {0}
      ( r′ ← copy {0} r
        ! read {1} r′ >>= print {1}
        , write {1} r′ 77
        , writeLocal {1} r′ 77
        , readLocal {1} r′ >>= print {1}
        , read {1} r′ >>= print {1}
        , read {0} r >>= print {1}
      )
    , fork {0}
      ( r ← copy {0} r
        ! delay {1} 500000
        , read {1} r >>= print {1}
        , writeLocal {1} r 88
        , write {1} r 88
        , readLocal {1} r >>= print {1}
        , read {1} r >>= print {1}
      )
    , delay {0} 1000000
    , readLocal {0} r >>= print {0}

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

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

тут можно делать someThing <- var1 <$> get, точнее чуть сложнее:

data ThreadVars = ThreadVars 
            {  var1 :: IORef ..
            ,  var2 :: IORef ..
            }

и readIORef <$> var1 <$> get 
qnikst ★★★★★
()
Ответ на: комментарий от quasimoto

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

на самом деле можно и хитрее: http://blog.sigfpe.com/2010/02/tagging-monad-transformer-layers.html.

и в методах требовать instance MonadTSL ConcreteDataType, что получиться haskell-way, т.к. уровни явно отделены.

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

на самом деле можно и хитрее

Да, там даже можно написать deriving Monad для T, вроде бы. Пример с агдой выше примерно о том же - индексированные / тегированные типы.

что получиться haskell-way, т.к. уровни явно отделены.

Тем не менее, обычные переменные (IORef, MVar и т.п.) можно вводить «обычно» - просто ref <- newIORef или ref = unsafePerfromIO . newIORef и дальше использовать эти переменные. Без необходимости каждый раз «перешивать» модель, добавлять новые типы или дописывать инстансы. Только они глобальные по смыслу. Локальные переменные по смыслу ничем не хуже, только их нет в хаскеле. Вот в Эрланге, при всей чистоте, есть такие вещи (и там ведь тоже лёгкие процессы).

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