Я думал об этом связку. Так есть другие люди:
Теперь мои собственные спекуляции.
В приведенных выше рассуждениях, основная идея большой части времени является то, что вы могли бы придерживаться ! на любого типа, чтобы получить строгую, определенно, оцененный WHNF версию этого типа. Таким образом, Int может быть громким, а !Int определенно не один. Это вызывает интересные вопросы для typechecker. Выполняется !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# и т. Д.), Но они подключены (вы не можете добавлять новые), а также unboxed в дополнение к тому, чтобы быть развязанным, поэтому они имеют различный вид (# вместо *) и не может смешиваться с обычными типами. Принимая во внимание, что !a будет несимметричным, но коробчатым, типа *.Нераскрытые типы - это то, о чем я уже упоминал несколько раз в теоретико-типологических контекстах, поэтому, возможно, было проведено некоторое исследование того, что потребуется для их реализации более общим образом. Я еще не смотрел.
Вы видели [язык учеников] (http://disciple.ouroborus.net/)? –
Спасибо. Я искал способ сжать это в текущий Haskell (ну, GHC, который есть), но это интересно. – Clinton
Распространенность утечек памяти в программах с ручным управлением памятью вызывает опровержение вашего тезиса о том, что легко установить верхние границы использования пространства программ на C/C++. Тем не менее, отличный вопрос! – Ben