6.10.3. Вид Constraint

ConstraintKinds

Версия:

7.4.1

Статус:

Включено в GHC2024, GHC2021

Разрешает использовать типы вида Constraint в контекстах.

Обычно ограничения (которые появляются в типах слева от стрелки =>) имеют очень ограниченный синтаксис. Они могут быть только:

• Ограничениями классов, например Show a
• Implicit parameter-ограничениями, например ?x::Int (при включённом расширении ImplicitParams)
• Ограничениями равенства, например a ~ Int (при включённом расширении TypeFamilies или GADTs)

Расширение ConstraintKinds позволяет GHC менее строго ограничивать допустимые в вашей программе ограничения. Точнее, при включённом этом флаге в качестве ограничения можно использовать любой тип нового вида Constraint. Следующие элементы имеют вид Constraint:

• Всё, что и без этого флага допустимо в качестве ограничения: насыщенные применения классов типов, ограничения неявных параметров и ограничения равенства.
• Кортежи, все типы-компоненты которых имеют вид Constraint. Например, тип (Show a, Ord a) имеет вид Constraint.
• Элементы с пока ещё неизвестной формой, для которых пользователь объявил вид Constraint (для этого их нужно импортировать из Data.Kind). Например, type Foo (f :: Type -> Constraint) = forall b. f b => b -> b допускается.

Однако обратите внимание: расширения TypeFamilies и GADTs также позволяют работать с элементами вида Constraint, при этом расширение ConstraintKinds может и не требоваться:

-- With -XTypeFamilies -XNoConstraintKinds
type T :: Type -> (Type -> Constraint)
type family T a where
  T Int    = Num
  T Double = Floating

-- With -XGADTs -XNoConstraintKinds
type Dict :: Constraint -> Type
data Dict c where
  MkDict :: c => Dict c

При включённом расширении ConstraintKinds ограничения рассматриваются просто как типы определённого вида. Это позволяет создавать синонимы типов для ограничений:

type Stringy a = (Read a, Show a)
foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)

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

type family Clsish u a
type instance Clsish () a = Cls a
class Clsish () a => Cls a where

class OkCls a where

type family OkClsish u a
type instance OkClsish () a = OkCls a
instance OkClsish () a => OkCls a where

Вы можете писать программы, использующие экзотические виды ограничений в контекстах экземпляров и суперклассах, но для этого необходимо включить UndecidableInstances, чтобы сообщить, что вы допускаете возможность незавершения работы проверяющей типы системы.