Нормальная форма Haskells Weak Head

Question

Я наткнулся на некоторые раздражающие вещи. Я знаю, что haskell работает со слабой нормальной формой головы (WHNF), и я знаю, что это такое. Набираю следующий код в ghci (я использую команду: sprint, которая сокращает выражение до WHNF, насколько мне известно.):

let intlist = [[1,2],[2,3]]
:sprint intlist

дает intlist = _ для меня это имеет смысл.

let stringlist = ["hi","there"]
:sprint stringlist 

дает stringlist = [_,_] Это меня уже смущает. Но потом:

let charlist = [['h','i'], ['t','h','e','r','e']]
:sprint charlist

удивительно дает charlist = ["hi","there"]

Насколько я понял Haskell, строки - это не что иное, как списки символов, что, кажется, подтверждается проверкой типов "hi" :: [Char] а также ['h','i'] :: [Char].

Я смущен, потому что, как я понимаю, все три приведенных выше примера более или менее одинаковы (список списков) и, следовательно, должны сводиться к одному и тому же WHNF, а именно _. Что мне не хватает?

Благодарность

Answer 1

Обратите внимание, что :sprintникак не уменьшить выражение WHNF. Если бы это было так, то следующее дало бы4 скорее, чем _:

Prelude> let four = 2 + 2 :: Int
Prelude> :sprint four
four = _

Скорее, :sprint принимает имя привязки, просматривает внутреннее представление значения привязки и показывает уже "оцененные части" (т. е. части, которые являются конструкторами) при использовании _как заполнитель для неоцененных преобразователей (т. е. приостановленных ленивых вызовов функций). Если значение полностью неоценено, оценка выполняться не будет, даже для WHNF. (И если значение будет полностью оценено, вы получите это, а не только WHNF.)

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

Если вы действительно хотите понять, что :sprint выполняется, вы можете включить несколько флагов в GHCi, чтобы увидеть, как на самом деле обрабатываются выражения и, таким образом, в конечном итоге компилируются в байт-код:

> :set -ddump-simpl -dsuppress-all -dsuppress-uniques

После этого мы сможем увидеть причину вашего intlist дает _:

> let intlist = [[1,2],[2,3]]
==================== Simplified expression ====================
returnIO
  (: ((\ @ a $dNum ->
         : (: (fromInteger $dNum 1) (: (fromInteger $dNum 2) []))
           (: (: (fromInteger $dNum 2) (: (fromInteger $dNum 3) [])) []))
      `cast` <Co:10>)
     [])

Вы можете игнорировать returnIO и внешний : звоните и сосредоточьтесь на той части, которая начинается с ((\ @ a $dNum -> ...

Вот $dNum это словарь для Numограничение. Это означает, что сгенерированный код еще не разрешил фактический типa в типе Num a => [[a]], поэтому все выражение по-прежнему представляется как вызов функции, использующий (словарь) соответствующий Numтип. Другими словами, это неоцененный преобразователь, и мы получаем:

> :sprint intlist
_

С другой стороны, укажите тип как Int, а код совершенно другой:

> let intlist = [[1::Int,2],[2,3]]
==================== Simplified expression ====================
returnIO
  (: ((: (: (I# 1#) (: (I# 2#) []))
         (: (: (I# 2#) (: (I# 3#) [])) []))
      `cast` <Co:6>)
     [])

и так :sprint выход:

> :sprint intlist
intlist = [[1,2],[2,3]]

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

> let stringlist = ["hi", "there"]
==================== Simplified expression ====================
returnIO
  (: ((: (unpackCString# "hi"#) (: (unpackCString# "there"#) []))
      `cast` <Co:6>)
     [])

> let charlist = [['h','i'], ['t','h','e','r','e']]
==================== Simplified expression ====================
returnIO
  (: ((: (: (C# 'h'#) (: (C# 'i'#) []))
         (: (: (C# 't'#)
               (: (C# 'h'#) (: (C# 'e'#) (: (C# 'r'#) (: (C# 'e'#) [])))))
            []))
      `cast` <Co:6>)
     [])

и различия в :sprint вывод представляет артефакты того, какие части выражения GHCi считает оцененными (явное : конструкторы) по сравнению с неоцененными (unpackCString# thunks).