Введите принудительное "строгое / непереносимое" подмножество / версию Haskell
Мне очень нравится Haskell, однако одна из главных вещей, которые касаются меня в Haskell, заключается в сложности рассуждений об использовании пространства. По сути, возможность использования thunks и рекурсии создает некоторые хитрые ситуации, когда кажется, что нужно быть очень осторожным, добавляя правильную строгость, чтобы программа не исчерпала память на определенных входах.
Что мне нравится в C/C++, так это то, что я могу быстро быть уверенным в верхних границах использования пространства программ, особенно если избегать рекурсии. Переменные ясно видеть.
Мне было интересно, есть ли способ создать безопасное "императивное" подмножество Haskell, которое не имеет thunks и является строгим.
Я понимаю, что Data.STRef предоставляет изменяемые ячейки, но, насколько я понимаю, сами эти ячейки все еще ленивы и могут содержать громоздкие звуки. Я думал о том, чтобы заставить данные в таких ячейках быть строгими, но я не уверен, как это сделать способом, предписанным системой типов.
Я думал о чем-то вроде "Строгой монады", но, возможно, это неправильная форма для этого.
3 ответа
Я вполне уверен, что реализовать это в Haskell будет практически невозможно, что по умолчанию предполагает лень. Например, во всей стандартной библиотеке есть функции, которые на строгом языке бесполезны, потому что на самом деле они гарантированно не прекратят работу, если вы запросите их весь вывод. Поэтому, если бы у вас было "строгое подмножество" Haskell, было бы сложно взаимодействовать с любым другим кодом на Haskell, и вы все равно эффективно программировали бы на другом языке.
Кроме того, я думаю, что вы ищете не в том месте, думая о монадах. Data.STRef на самом деле не имеет ничего общего с избеганием громов и лени. Фактически, то, что вы хотите (строгость), не имеет ничего общего с необходимостью, и вам не нужны изменчивость или монады, чтобы получить это. Есть языки программирования, которые так же чисты, как Haskell, но везде строги. Например, я работал с Меркурием.
Я думал об этом кучу. Так что есть другие люди:
Теперь мои собственные предположения.
В приведенных выше обсуждениях основная идея в большинстве случаев заключается в том, что ! для любого типа, чтобы получить строго определенную версию WHNF этого типа. Так Int может быть гром, а !Int определенно не один. Это поднимает интересные вопросы для проверки типов. Есть ли !Int ~ Int держать? Если этого не произойдет - это два совершенно разных несовместимых типа, то работа с ними будет очень болезненной. С другой стороны, если это действительно так, ничто не помешает пройти неоцененную Int где !Int ожидается - в конце концов, они одного типа. В идеале вы хотели бы иметь возможность !Int где Int ожидается, но не наоборот. Это звучит как отношение подтипа: !a <: a, !a это подтип a, a населены как оцененными, так и неоцененными значениями (thunks), в то время как !a только оцененными. Система типов GHC не имеет подтипов и, вероятно, не может, потому что другие части системы типов не взаимодействуют с ней хорошо. Однако это строго ограниченный конкретный пример подтипирования: программист не может объявлять произвольные отношения подтипов, а существует одно жестко закодированное отношение: forall a. !a <: a, Я понятия не имею, делает ли это более разумным для реализации.
Предположим, это можно сделать. Вы получаете дополнительные вопросы. Что делать, если вы попытаетесь поставить Int где !Int ожидается? Ошибка типа? В идеале, я думаю, это было бы не так, вместо этого компилятор вставлял бы код для его оценки и продолжал. Хорошо. Как насчет поставки [Int] где [!Int] ожидается, или f a а также f !a в общем случае? Как мог компилятор знать, как обойти любую данную структуру, чтобы найти те точки, где она содержит a, чтобы оценить тех, и только тех? Так будет ли это ошибка типа? Скажем так. Как программист выполняет преобразование вручную - получить f !a из f a? Возможно, путем сопоставления функции eval :: a -> !a? Но это бессмысленно. Хаскелл очень ленив. Если вы примените его к аргументу, eval x, тогда, пока его значение не понадобится, это будет гром. Так eval x не может иметь тип !a, Примечания строгости в позиции возвращаемого типа не имеют никакого смысла. Так что насчёт: data Wrap a = Wrap { unwrap :: a }, eval' :: a -> Wrap !a с семантикой Wrap !a это может быть громом, но компилятор вставляет код так, чтобы при его оценке !a внутри точно тоже будет оцениваться? На самом деле, вот более простая формулировка: data Wrap' a = Wrap' { unwrap' :: !a } (eval' = Wrap'). Который является существующим легальным Haskell, подчиняется нашей новой строгости печатания. Это хорошо, я думаю. Но как только вы пытаетесь использовать его, у вас снова возникают проблемы. Как бы вы получили от f a в f !a, снова -- fmap unwrap . fmap Wrap? Но unwrap имеет точно такую же проблему, как eval, Так что все это кажется не таким тривиальным. А как насчет, казалось бы, безобидного обратного случая: поставка f !a где f a ожидается? Это работает? (Другими словами, f !a <: f a?) Это зависит от того, как a используется внутри f, Компилятор должен обладать знаниями о ковариантных, контравариантных и инвариантных позициях аргументов типа - еще одна вещь, которая поставляется с подтипами.
Это, насколько я думал, до конца. Это кажется сложнее, чем кажется.
Еще одна интересная вещь. Возможно, вы слышали или не слышали о понятии "неснятые типы": типы, которые не населены дном. Это, насколько я могу сказать, то же самое, что и это. Типы, которые гарантированно будут оценены в WHNF; типы, которые гарантированно не будут низами. Нет разницы, верно? GHC на самом деле уже имеет в качестве примитивов целую кучу неподнятых типов (Int# и т. д.), но они подключены (вы не можете добавлять новые), а также распакованы в дополнение к тому, что не были подняты, поэтому они имеют другой вид (# вместо *) и не может смешиваться с обычными типами. В то время как !a был бы не поднятым, но в штучной упаковке, типа, вида *, Я заметил, что в теоретико-контекстных контекстах несколько раз упоминались неснятые типы, поэтому, возможно, было проведено некоторое исследование того, что потребуется для их реализации в более общем виде. Я еще не смотрел.
Возможно, вам будет интересно узнать о расширении языка BangPatterns и о типах / операциях Unboxed. Но вы также должны знать, что любая функция всегда будет иметь значение в штучной упаковке. Это ответственность оптимизации за устранение любых значений ref-kind путем компиляции кода в соответствии с "взрывами" и других вещей в функции.