А что будет с 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 не применим потому что нельзя построить соответсвующее доказательство, то ли можно как-то выкрутиться.

он же физически всё ещё в России?

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

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

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

вкупе с

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

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

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

толсто

можно с какой-то натяжкой интерпретировать, как если в 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 #-}

Теперь понял, спасибо.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Никак :) В хаскеле это невыразимые в языке / тулзах чисто умозрительные построения (например, можно ожидать, что 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 - бразильская. А если нет, и нужно бразильскую найти? Скажем, у тебя работает сервер, к котором подключаются со всего мира. А в случае Китая у них не грегорианский календарь, а китайский. Что делать будешь?

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

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

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

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

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

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

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

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

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

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

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

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

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

Rank2 types + ExistentialQuantification

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

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

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

Поэтому классических 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). С какого ресурса - не знаю, нужно поискать, либо самому написать ресурс используя уже готовые библиотеки для форматирования времени (с такими тоже не сталкивался).

Смешно

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

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

http://en.wikipedia.org/wiki/Tz_database#Use_in_software_systems

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

Конечно же, в C/C++ этого всего нет, а autotools мне приснились в страшном сне.

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

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

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

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

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

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

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

?

:-)

Ну-ну.

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 боилерплейта.

• Проблему форматирования времени и даты так как это принято в данном регионе это не решает.

Да, ошибся.

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

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

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

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

*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

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

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

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

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

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

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

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

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

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

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

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

И?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

не считая bounded threads.

И?

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 действительно выглядят как набор костылей. Вообщем, можно много к чему придираться. Но хороших вещей в языке и вокруг тоже много.

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

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

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

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

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

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

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

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

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

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

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

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

get :: IO a

put :: a -> IO ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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