6.2.19. Типизированные дыры

Типизированные дыры — это функция GHC, позволяющая использовать в качестве выражений специальные заполнители, записанные с начальным символом подчёркивания (например, «_», «_foo», «_bar»). При компиляции такие дыры приводят к сообщению об ошибке, в котором описывается ожидаемый тип в месте расположения дыры, приводится информация о происхождении свободных переменных типов, а также список локальных связей, которые могут помочь заполнить дыру, и связей в области видимости, соответствующих типу дыры и способных помочь заполнить её настоящим кодом. Типизированные дыры всегда включены в GHC.

Цель типизированных дыр — помочь при написании кода на Haskell, а не изменить систему типов. Типизированные дыры можно использовать для получения дополнительной информации от проверки типов, которую иначе может быть сложно получить. Обычно в GHCi пользователи могут просматривать (выведенные) сигнатуры типов всех связей верхнего уровня. Однако этот способ менее удобен для терминов, которые не определены на верхнем уровне или находятся внутри сложных выражений. Дыры позволяют пользователю проверить тип термина, который он собирается написать.

Например, компиляция следующего модуля с помощью GHC:

f :: a -> a
f x = _

завершится следующей ошибкой:

hole.hs:2:7:
    Found hole `_' with type: a
    Where: `a' is a rigid type variable bound by
               the type signature for f :: a -> a at hole.hs:1:6
    In the expression: _
    In an equation for `f': f x = _
    Relevant bindings include
      x :: a (bound at hole.hs:2:3)
      f :: a -> a (bound at hole.hs:2:1)
    Valid hole fits include x :: a (bound at hole.hs:2:3)

Вот дополнительные сведения:

• Ошибка «Found hole» обычно прерывает компиляцию, как и любая другая ошибка типов. В конце концов, вы пропустили часть кода в программе. Тем не менее фрагмент кода с дырами можно запустить и протестировать, используя флаг -fdefer-typed-holes. Этот флаг откладывает ошибки, вызванные типизированными дырами, до времени выполнения и преобразует их в предупреждения времени компиляции. Эти предупреждения, в свою очередь, можно полностью отключить с помощью -Wno-typed-holes.

  Для ошибок «Variable out of scope» действует то же поведение: по умолчанию они прерывают компиляцию. Такие ошибки можно отложить с помощью флага -fdefer-out-of-scope-variables. Этот флаг откладывает до времени выполнения ошибки, вызванные переменными вне области видимости, и преобразует их в предупреждения времени компиляции. Эти предупреждения, в свою очередь, можно полностью отключить с помощью -Wno-deferred-out-of-scope-variables.

  В результате дыра или переменная ведёт себя как undefined, но с тем преимуществом, что во время компиляции выводится предупреждение, а при вычислении во время выполнения появляется то же сообщение. Это поведение соответствует параметру -fdefer-type-errors, который подразумевает -fdefer-typed-holes и -fdefer-out-of-scope-variables. См. раздел Откладывание ошибок типов до времени выполнения.

• Все несвязанные идентификаторы рассматриваются как типизированные дыры, независимо от того, начинаются ли они с символа подчёркивания. Отличается только сообщение об ошибке:

  cons z = z : True : _x : y
  

  вызывает следующие ошибки:

  Foo.hs:3:21: error:
     Found hole: _x :: Bool
     Or perhaps ‘_x’ is mis-spelled, or not in scope
     In the first argument of ‘(:)’, namely ‘_x’
     In the second argument of ‘(:)’, namely ‘_x : y’
     In the second argument of ‘(:)’, namely ‘True : _x : y’
     Relevant bindings include
       z :: Bool (bound at Foo.hs:3:6)
     cons :: Bool -> [Bool] (bound at Foo.hs:3:1)
     Valid hole fits include
       z :: Bool (bound at mpt.hs:2:6)
       otherwise :: Bool
         (imported from ‘Prelude’ at mpt.hs:1:8-10
         (and originally defined in ‘GHC.Base’))
       False :: Bool
         (imported from ‘Prelude’ at mpt.hs:1:8-10
         (and originally defined in ‘GHC.Types’))
       True :: Bool
         (imported from ‘Prelude’ at mpt.hs:1:8-10
         (and originally defined in ‘GHC.Types’))
       maxBound :: forall a. Bounded a => a
         with maxBound @Bool
         (imported from ‘Prelude’ at mpt.hs:1:8-10
         (and originally defined in ‘GHC.Enum’))
       minBound :: forall a. Bounded a => a
         with minBound @Bool
         (imported from ‘Prelude’ at mpt.hs:1:8-10
         (and originally defined in ‘GHC.Enum’))
  
  Foo.hs:3:26: error:
      Variable not in scope: y :: [Bool]
  

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

• Несвязанные идентификаторы с одинаковыми именами никогда не объединяются, даже внутри одной функции, а отображаются отдельно. Например:

  cons = _x : _x
  

  приводит к следующим ошибкам:

  unbound.hs:1:8:
      Found hole '_x' with type: a
      Where: `a' is a rigid type variable bound by
                 the inferred type of cons :: [a] at unbound.hs:1:1
      In the first argument of `(:)', namely `_x'
      In the expression: _x : _x
      In an equation for `cons': cons = _x : _x
      Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
  
  unbound.hs:1:13:
      Found hole: _x :: [a]
      Where: ‘a’ is a rigid type variable bound by
              the inferred type of cons :: [a]
              at unbound.hs:3:1-12
      Or perhaps ‘_x’ is mis-spelled, or not in scope
      In the second argument of ‘(:)’, namely ‘_x’
      In the expression: _x : _x
      In an equation for ‘cons’: cons = _x : _x
      Relevant bindings include cons :: [a] (bound at unbound.hs:3:1)
      Valid hole fits include
        cons :: forall a. [a]
          with cons @a
          (defined at mpt.hs:3:1)
        mempty :: forall a. Monoid a => a
          with mempty @[a]
          (imported from ‘Prelude’ at mpt.hs:1:8-10
          (and originally defined in ‘GHC.Base’))
  

  Обратите внимание на два разных типа, указанных для двух вхождений _x.

• Для использования типизированных дыр не требуется расширение языка. Лексема «_» ранее была недопустима в Haskell, но теперь для неё выводится более информативное сообщение об ошибке. Лексема «_x» является вполне допустимой переменной, и её поведение не меняется, когда она находится в области видимости. Например:

  f _x = _x + 1
  

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

• Несвязанные конструкторы данных, используемые в выражениях, обрабатываются точно так же, как описано выше. Однако несвязанные конструкторы данных, используемые в образцах, нельзя откладывать, и они приводят к прерыванию компиляции. (С точки зрения реализации, о них сообщает переименователь, а не проверка типов.)

• Список допустимых вариантов заполнения дыр формируется путём проверки того, какие связи в области видимости можно подставить в дыру. Например, компиляция следующего модуля с помощью GHC:

  import Data.List (inits)
  
  g :: [String]
  g = _ "hello, world"
  

  выдаёт следующие ошибки:

  • Found hole: _ :: [Char] -> [String]
  • In the expression: _
    In the expression: _ "hello, world"
    In an equation for ‘g’: g = _ "hello, world"
  • Relevant bindings include g :: [String] (bound at mpt.hs:6:1)
    Valid hole fits include
      lines :: String -> [String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      words :: String -> [String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      inits :: forall a. [a] -> [[a]]
        with inits @Char
        (imported from ‘Data.List’ at mpt.hs:4:19-23
         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      repeat :: forall a. a -> [a]
        with repeat @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘GHC.List’))
      fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
        with fail @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘GHC.Base’))
      return :: forall (m :: * -> *). Monad m => forall a. a -> m a
        with return @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘GHC.Base’))
      pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
        with pure @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘GHC.Base’))
      read :: forall a. Read a => String -> a
        with read @[String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘Text.Read’))
      mempty :: forall a. Monoid a => a
        with mempty @([Char] -> [String])
        (imported from ‘Prelude’ at mpt.hs:3:8-9
         (and originally defined in ‘GHC.Base’))
  

Для управления объёмом контекстной информации, отображаемой для типизированных дыр, предусмотрено несколько флагов:

-fshow-hole-constraints

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

f :: Eq a => a -> Bool
f x = _

выводит следующее сообщение:

show_constraints.hs:4:7: error:
    • Found hole: _ :: Bool
    • In the expression: _
      In an equation for ‘f’: f x = _
    • Relevant bindings include
        x :: a (bound at show_constraints.hs:4:3)
        f :: a -> Bool (bound at show_constraints.hs:4:1)
      Constraints include Eq a (from show_constraints.hs:3:1-22)
      Valid hole fits include
        otherwise :: Bool
        False :: Bool
        True :: Bool
        maxBound :: forall a. Bounded a => a
          with maxBound @Bool
        minBound :: forall a. Bounded a => a
          with minBound @Bool

f :: [Integer] -> Integer
f = _

Valid hole fits include
  f :: [Integer] -> Integer
  head :: forall a. [a] -> a
    with head @Integer
  last :: forall a. [a] -> a
    with last @Integer
  maximum :: forall (t :: * -> *).
              Foldable t =>
              forall a. Ord a => t a -> a
    with maximum @[] @Integer
  minimum :: forall (t :: * -> *).
              Foldable t =>
              forall a. Ord a => t a -> a
    with minimum @[] @Integer
  product :: forall (t :: * -> *).
              Foldable t =>
              forall a. Num a => t a -> a
    with product @[] @Integer
  sum :: forall (t :: * -> *).
          Foldable t =>
          forall a. Num a => t a -> a
    with sum @[] @Integer

Valid refinement hole fits include
  foldl1 (_ :: Integer -> Integer -> Integer)
    with foldl1 @[] @Integer
    where foldl1 :: forall (t :: * -> *).
                    Foldable t =>
                    forall a. (a -> a -> a) -> t a -> a
  foldr1 (_ :: Integer -> Integer -> Integer)
    with foldr1 @[] @Integer
    where foldr1 :: forall (t :: * -> *).
                    Foldable t =>
                    forall a. (a -> a -> a) -> t a -> a
  const (_ :: Integer)
    with const @Integer @[Integer]
    where const :: forall a b. a -> b -> a
  ($) (_ :: [Integer] -> Integer)
    with ($) @GHC.Types.LiftedRep @[Integer] @Integer
    where ($) :: forall a b. (a -> b) -> a -> b
  fail (_ :: String)
    with fail @((->) [Integer]) @Integer
    where fail :: forall (m :: * -> *).
                  Monad m =>
                  forall a. String -> m a
  return (_ :: Integer)
    with return @((->) [Integer]) @Integer
    where return :: forall (m :: * -> *). Monad m => forall a. a -> m a
  (Some refinement hole fits suppressed;
    use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)