Наблюдение, что предыдущие семейные пункты типа не соответствовали - PullRequest
Новая
       66

Наблюдение, что предыдущие семейные пункты типа не соответствовали

4 голосов
/ 04 февраля 2020

У меня есть следующее семейство закрытых типов: 

type family IsSpecialSize (n :: Nat) :: Bool where
    IsSpecialSize 8 = True
    IsSpecialSize 16 = True
    IsSpecialSize _ = False

Я хотел бы написать одноэлементного свидетеля и решающее лицо для этого семейства типов: 

data SSpecial (n :: Nat) where
    SSpecial8 :: SSpecial 8
    SSpecial16 :: SSpecial 16
    SNotSpecial :: (IsSpecialSize n ~ False) => SSpecial n

class DecideSSpecial (n :: Nat) where
    specialSize :: SSpecial n

Особые случаи тривиально, чтобы покрыть: 

instance {-# OVERLAPPING #-} DecideSSpecial 8 where
    specialSize = SSpecial8

instance {-# OVERLAPPING #-} DecideSSpecial 16 where
    specialSize = SSpecial16

Однако у нас возникают проблемы с экземпляром generi c. Мы не можем просто написать 

instance {-# OVERLAPPABLE #-} (KnownNat n) => DecideSSpecial n where
    specialSize = SNotSpecial

, поскольку нет ничего, что могло бы доказать, что IsSpecialSize n ~ False. Мы можем попробовать добавить его в контекст последнего экземпляра: 

instance {-# OVERLAPPABLE #-} (KnownNat n, IsSpecialSize n ~ False) => DecideSSpecial n where
    specialSize = SNotSpecial

, но тогда мы не сможем использовать его абстрагирование над n; Например, следующее определение не может проверить: 

instance forall n. (KnownNat n, DecideSSpecial n) => Num (Unsigned n) where

но я очень хочу этого избежать; в конце концов, морально я должен быть в состоянии сказать, равно ли любое данное KnownNat 8, 16 или ни одному.

1 Ответ

1 голос
/ 04 февраля 2020

В настоящее время нет способа сделать это безопасно.

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

Вы все еще может создать такой способ небезопасно (вы можете использовать GHC.TypeNats.sameNat и unsafeCoerce a Refl в случае Nothing): 

-- (==) and (:~:) from Data.Type.Equality
eqNat :: forall n m. (KnownNat n, KnownNat m) => Either ((n == m) :~: 'False) (n :~: m)
eqNat =
  case GHC.TypeNats.sameNat @n @m Proxy Proxy of
    Just r -> Right r
    Nothing -> Left (unsafeCoerce (Refl :: 'False :~: 'False))
-- The only piece of unsafe code in this answer.

Обратите внимание, что он не такой мощный, как вы можно ожидать. В частности, неравенство не является симметричным c: ((n == m) ~ 'False) не означает ((m == n) ~ 'False). Поэтому вы должны быть осторожны с порядком аргументов eqNat.

Поскольку для этого используется универсальный c тест на равенство, тест IsSpecialSize также должен использовать его: 

type IsSpecialSize n = (n == 8) || (n == 16)

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

specialSize :: forall n. KnownNat n => SSpecial n
specialSize =
  case eqNat @n @8 of
    Right Refl -> SSpecial8
    Left Refl ->
      case eqNat @n @16 of
        Right Refl -> SSpecial16
        Left Refl -> SNotSpecial
...