При проверке типов проверяющая система создаёт метапеременные, обозначающие ещё неизвестные типы. Если проверяющая система не может вывести конкретный тип для метапеременной (или квантифицировать её), она подставляет для переменной типа конкретный тип, например Int или String.
Основной принцип подстановки типов по умолчанию состоит в том, что она используется как наиболее подходящее предположение для переменных типов, которые остаются неопределёнными в самом конце вывода типов.
Например:
-- Ambiguity:
u :: String
u = show 4.12
-- The type of 4.12 is ambiguous; default it to Double
-- Monomorphism restriction:
k = 6
-- Due to the monomorphism restriction, we must infer a monomorphic type, not:
--
-- k :: forall a. Num a => a
--
-- GHC defaults the type of k to Integer.
-- NoPolyKinds:
f Proxy = ()
-- With -XNoPolyKinds, we cannot infer the poly-kinded type
--
-- forall {k} (a :: k). Proxy a -> ()
--
-- GHC defaults (k := Type), thus inferring
--
-- f :: forall (a :: Type). Proxy a -> ()
-- Representation polymorphism:
g x = x
-- Should not quantify over the representation, as we cannot infer
-- a representation-polymorphic type for 'x':
--
-- forall {r} (a :: TYPE r). a -> a
--
-- Default r := LiftedRep, thus inferring
--
-- g :: forall (a :: Type). a -> a
-- Multiplicity polymorphism
{-# LANGUAGE LinearTypes #-}
h x = x
-- Do not infer multiplicity polymorphism:
--
-- h :: forall {m} a. a %m -> a
--
-- GHC defaults (m := Many), thus inferring
--
-- h :: forall (a :: Type). a %Many -> a
В оставшейся части этого раздела объясняется, как GHC выбирает типы для подстановки по умолчанию.
6.4.6.1. Подстановка типов классов по умолчанию
Основной механизм подстановки — подстановка типов классов по умолчанию. Он используется в таких ситуациях, как:
u :: String u = show 4.12 -- (4.12 :: a), with constraints (Fractional a, Show a). v :: [Int] -> [Char] -> Bool v xs ys = genericLength xs > genericLength ys -- Recall that (genericLength :: Num i => [x] -> i). Here, the return type -- of the two calls to genericLength are ambiguous; we get -- (genericLength xs :: a) with constraints (Num a, Ord a).
Идея состоит в том, что, поскольку переменная типа a встречается как аргумент неразрешённого числового ограничения, например Num a или Fractional a, естественно подставить для a числовой тип, например Double или Integer соответственно.
Исходные правила для подстановки значения по умолчанию в незаполненную метапеременную a из (Отчёта о Haskell, раздел 4.3.4) таковы:
- Переменная типа
aвстречается только в ограничениях видаC vдля классаC. (Небольшое примечание: невидимые параметры типа не учитываются, например параметр рода дляTypeable.) - Все классы, в которых встречается
a, являются стандартными (то есть определены в Prelude или стандартной библиотеке). - По крайней мере один из классов является числовым (например, это
Numили подразумеваетNum).
В такой ситуации GHC попытается выбрать тип по умолчанию для a, учитывая объявления типов по умолчанию, видимые в модуле, например:
default (Int, Integer, Double)
означает: сначала попытаться подставить для a тип Int. Если это не удастся, попробовать Integer, а если и это не удастся — Double. Отчёт о Haskell требует, чтобы все типы, перечисленные в объявлении default, были экземплярами Num.
Если модуль не содержит объявления default, GHC ведёт себя так, словно присутствует следующее резервное объявление типов по умолчанию:
default (Integer, Double)
6.4.6.2. Расширения подстановки типов классов по умолчанию
Доступно несколько расширений этих правил. Описанный выше базовый механизм указывает, что классами, для которых можно задавать типы по умолчанию, могут быть только числовые классы, причём все классы должны быть стандартными.
6.4.6.2.1. Перегруженные строки
OverloadedStrings расширяет набор классов, для которых можно задавать типы по умолчанию, и набор стандартных классов, добавляя в них IsString. Это позволяет использовать в объявлениях типов по умолчанию типы, являющиеся экземплярами IsString, и добавляет String в резервное объявление типов по умолчанию, если объявление не задано.
6.4.6.2.2. Именованные типы по умолчанию
NamedDefaults позволяет задавать объявления типов по умолчанию для отдельных классов, например default Show (Int, Bool), при условии, что указанные типы являются экземплярами соответствующего класса. В наборы классов, для которых можно задавать типы по умолчанию, и стандартных классов добавляется любой класс с именованным объявлением типа по умолчанию.
6.4.6.2.3. Расширенные правила подстановки по умолчанию
ExtendedDefaultRules, включённое по умолчанию в приглашении GHCi, значительно расширяет правила:
- Оно расширяет набор классов, для которых можно задавать типы по умолчанию, добавляя интерактивные классы:
Show,Eq,Ord,Foldable,Traversable. Тогда в объявлениях типов по умолчанию разрешается использовать типы, являющиеся экземплярами любого из этих классов. - В начало резервного объявления типов по умолчанию добавляются единичный тип
()и тип списка[]. - Правила подстановки по умолчанию изменяются следующим образом:
- Найти ограничения вида
C a, гдеa— переменная типа, и разбить эти ограничения на группы с общей переменной типаa. - Оставить только те группы, в которых хотя бы один класс допускает подстановку типа по умолчанию. (Как пояснялось выше, к ним относятся интерактивные классы,
IsStringпри использованииOverloadedStrings, а также любой класс с именованным объявлением типа по умолчанию при использованииNamedDefaults.) - Для каждой оставшейся группы G по очереди проверить каждый тип
tyиз списка типов по умолчанию. Если подстановкаa = tyпозволит полностью разрешить ограничения в G, подставить дляaтипty; в противном случае проверить следующий тип в списке.
Иными словами, пункт (3) означает, что мы отфильтровываем все ограничения, не имеющие вида C a для класса C, допускающего подстановку по умолчанию. Такие ограничения не участвуют в этом процессе (ни помогая, ни мешая), но, разумеется, должны быть разрешимы после завершения подстановки типов по умолчанию. В частности, сюда относятся все ограничения с несколькими параметрами, например D a b или E [a] Int.
6.4.6.3. Другие механизмы подстановки по умолчанию
Помимо основного механизма подстановки типов классов по умолчанию, описанного в разделе Подстановка типов классов по умолчанию, в GHC есть ещё несколько (более специализированных) механизмов подстановки по умолчанию.
6.4.6.3.1. Подстановка по умолчанию на основе рода
Для переменных типов рода RuntimeRep или Levity GHC подставит типы LiftedRep и Lifted соответственно. Это объясняется в разделе Вывод и подстановка по умолчанию.
Для переменных типов рода Multiplicity GHC подставит Many, как объясняется в разделе Линейные типы: стрелки с линейностью и полиморфизмом по кратности всегда объявляются, а не выводятся.
Для переменных рода (рода Type) GHC подставит Type, если расширение PolyKinds не включено; см. раздел Подстановка рода по умолчанию без PolyKinds.
6.4.6.3.2. Подстановка для стеков вызовов по умолчанию
Для реализации механизмов HasCallStack и ExceptionContext GHC подставит EmptyCallStack для любых неразрешённых ограничений HasCallStack, а emptyExceptionContext — для любых неразрешённых ограничений ExceptionContext соответственно.
6.4.6.3.3. Подстановка равенства по умолчанию
Обычно, когда GHC встречает ограничение равенства alpha ~ ty, в котором alpha — незаполненная метапеременная, GHC немедленно унифицирует alpha с ty. Однако в некоторых случаях GHC не спешит выполнять унификацию alpha := ty, чтобы сохранить возможность вывести главные типы. Например:
{-# LANGUAGE GADTs #-}
data T a where
MkT :: T Bool
h x = case x of { MkT -> True }
Внутри сопоставления с образцом case GHC создаёт новую метапеременную beta для возвращаемого типа, но эта метапеременная «застревает» внутри ограничения равенства, введённого сопоставлением с образцом GADT:
forall a. a ~ Bool => beta ~ Bool
Здесь GHC может унифицировать либо beta := a, либо beta := Bool, что приведёт соответственно к следующим сигнатурам типов для h:
forall a. T a -> a T Bool -> Bool
Ни один из этих типов не является более общим, чем другой, поэтому GHC не выполняет унификацию beta := Bool — даже несмотря на наличие неразрешённого ограничения равенства beta ~ Bool. Поскольку мы находимся не на верхнем уровне (а внутри сопоставления с образцом GADT), GHC отклонит эту программу (исправление: добавить сигнатуру типа для h).
Однако в случаях, когда проверка типов всё же доходит до верхнего уровня, имеет смысл подставлять типы по умолчанию для незаполненных метапеременных, встречающихся в неразрешённых номинальных ограничениях равенства. Например:
f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int g :: Int g = f id
В этом случае при инстанцировании f в теле g GHC создаст новую метапеременную alpha для внешнего forall в f. Эта метапеременная, в свою очередь, встречается в импликации под другим ограничением равенства:
forall t. (F t ~ Int) => alpha ~ Int
Однако, в отличие от предыдущего примера с GADT, здесь мы находимся на верхнем уровне и не можем квантифицировать alpha. Поэтому GHC подставляет для alpha тип Int; это не угрожает сохранению главных типов.
