Блог

Я пытаюсь использовать семейство типов для создания ограничений, которые зависят от некоторого натурального числа уровня типа. Вот такая функция:

 type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)
 

Тогда у меня есть функция, которая имеет это ограничение.

 f :: forall n m. (KnownNat n, KnownNat m, m ~ 0) => ()
f = ()
 

Когда я пытаюсь использовать эту функцию в сопоставлении с шаблоном, где мое семейство типов
должно создавать это ограничение, ghc сообщает, что он не может вывести ограничение

Вот пример:

 g :: forall n m. (KnownNat n, KnownNat m, F n m) => ()
g =
  case (natVal (Proxy @n)) of
    0 -> ()
    n -> f @n @m

 

Это приводит к ошибке

 • Could not deduce: m ~ 0 arising from a use of ‘f’
      from the context: (KnownNat n, KnownNat m, F n m)
        bound by the type signature for:
                   g :: forall (n :: Nat) (m :: Nat).
                        (KnownNat n, KnownNat m, F n m) =>
                        ()
    ‘m’ is a rigid type variable bound by
        the type signature for:
          g :: forall (n :: Nat) (m :: Nat).
               (KnownNat n, KnownNat m, F n m) =>
               ()
 • In the expression: f @n @m
      In a case alternative: n -> f @n @m
      In the expression:
        case (natVal (Proxy @n)) of
          0 -> ()
          n -> f @n @m
    |
168 |     n -> f @n @m
    |          ^^^^^^^
 

Основная причина, по которой ваше сопоставление с шаблоном не приводит к каким-либо ограничениям, заключается в том, что вы сопоставляете регистр natVal (Proxy @n) :: Integer , который не является GADT. Согласно ответу @chi, вам необходимо сопоставить GADT, чтобы получить информацию о типе в области видимости.

Для слегка измененной версии вашего семейства типов:

 type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = (m ~ 0)
  F n m = ()
 

способ, которым вы могли бы добиться этого, был бы следующим:

 f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @0) of
  Just Refl -> f @n @m
  Nothing -> ()
 

Этот случай совпадает с GADT, чтобы ввести ограничение n ~ 0 в Just Refl ветку. Это позволяет разрешить семейство типов F n m m ~ 0 . Обратите внимание, что я удалил посторонние KnownNat ограничения; это несколько важно, поскольку ответ @chi показывает, что ваша проблема легко решается, если у вас есть KnownNat m ограничение, доступное в g сигнатуре типа. В конце концов, если m известно, то вы можете напрямую определить, является ли это 0 или нет, и F m n ограничение является избыточным, независимо от значений m и n .

К сожалению, для вашего исходного семейства типов с измененным условием:

 type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)
 

все гораздо сложнее. Семейства типов разрешаются с помощью довольно простого «прямого решателя», из-за отсутствия лучшего термина, поэтому для вашей версии F выражение типа F n m может быть разрешено только для определенного n , например 0 , или 5 . Нет никакого ограничения, выражающего тот факт, что n это неопределенный тип, отличный 0 от того, который вы могли бы каким- то образом использовать для разрешения F n m = (m ~ 0) . Итак, вы могли бы написать:

 g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @1) of
      Just Refl -> f @n @m
      Nothing -> ()
 

который использует тот факт, что в Just Refl -> ветке ограничение n ~ 1 находится в области видимости, которая позволяет F n m быть разрешенной. Но, похоже, нет способа заставить его работать для произвольного ненулевого n значения.

Есть несколько подходов, которые могли бы сработать. Переход на Peano naturals решил бы эту проблему:

 data Nat = Z | S Nat
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
class KnownNat n where
  natSing :: SNat n
instance KnownNat Z where natSing = SZ
instance KnownNat n => KnownNat (S n) where natSing = SS natSing

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F Z m = ()
  F (S n) m = (m ~ Z)

f :: forall n m. (m ~ Z) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case natSing @n of
  SZ -> ()
  SS n -> f @n @m
 

Здесь ветвь SS n case вводит в область действия ограничение n ~ S n1 , которое действительно выражает тот факт , что n является неопределенным естественным , отличным от Z , что позволяет нам разрешить семейство типов F n m = (m ~ Z) .

Вы также можете представить F ограничение, используя условие уровня типа:

 type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)
 

и писать:

 import Data.Kind
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import GHC.TypeLits
import Unsafe.Coerce

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case leqNat (Proxy @1) (Proxy @n) of
  Just Refl -> f @n @m
  Nothing -> ()

leqNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe ((a <=? b) :~: True)
leqNat x y | natVal x <= natVal y = Just (unsafeCoerce Refl)
           | otherwise            = Nothing
 

Здесь функция leqNat предоставляет соответствующие доказательства на уровне типа о том, что одно значение меньше или равно другому. Вероятно, это выглядит как мошенничество, но если вы сравните это с определением sameNat , вы увидите, что это обычный вид мошенничества.