Haskell - Как определить зависимый тип Remainder (т. Е. Rmndr modulo)?

Question

Я понимаю, что остаточный тип является зависимым типом (в зависимости от модуля). Я читал о продлении DataKinds и был в состоянии определить его как следующее:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs #-} 
data Nat = Zero | Succ Nat 

data Rmndr modulo where 
    Nil :: Rmndr Zero 
    Rmndr :: Integer -> Rmndr modulo 

Но тогда, когда я предваряюсь реализовать класс Eq, я застрял в состоянии

Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo) 

потому, что по модулю не значение, но тип. Даже если мы можем написать функцию следующим образом:

decat :: Nat -> Integer 
decat Zero = 0 
decat (Succ nat) = decat nat + 1 

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

instance Eq (Rmndr modulo) where 
    Nil == Nil = True 
    Rmndr x == Rmndr y = 
     x `mod` (decat modulo) == y `mod` (decat modulo) 

потому, что «по модулю» в этом синтаксисе, не является переменной.

Может ли кто-нибудь помочь в этой головоломке? Большое спасибо!

Answer 1

Фокус в том, чтобы использовать класс типа, чтобы связать каждый натуральный номер с singleton. Мы делаем это, создавая экземпляр для Zero, связанный с 0, и рекурсивный экземпляр для Succ x. Чтобы получить доступ к самому типу, нам нужно взять аргумент прокси-сервера. Идиомой для аргументов прокси является использование переменной типа, называемой proxy a; когда вы идете позвонить, вы чаще всего используете Proxy от Data.Proxy.

Вот соответствующий класс:

class SingNat n where 
    sing :: proxy n -> Integer 

и экземпляры:

instance SingNat Zero where sing _ = 0 

instance SingNat n => SingNat (Succ n) where 
    sing _ = 1 + sing (Proxy :: Proxy n) 

Чтобы сделать всю эту работу, вы должны также включить ScopedTypeVariables который обеспечивает n в :: Proxy n это то же самое, один в SingNat (Succ n).

Хорошая интуиция заключается в том, что два экземпляра typelcass похожи на два случая вашей функции decat, но на уровне уровня. Typeclasses использовались как эта функция как немного логический язык программирования на уровне языка, мало чем отличающийся от мини-Prolog.

Теперь вы можете использовать sing получить по модулю, переплетенного в вашем определении Eq (и других):

instance SingNat n => Eq (Rmndr n) where 
    Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo) 
    where modulo = sing (Proxy :: Proxy n) 

Этот вид кода является отличным способом, чтобы получить навык программирования на уровне типа. Однако в реальном коде вы, вероятно, не хотите откатывать свой собственный натуральный номер, потому что GHC имеет один встроенный с DataKinds. Помимо стандартного, это также дает вам синтаксический сахар на уровне шрифта, позволяющий писать такие типы, как Rmndr 10. Если вам интересно об этом подходе, взгляните на мой пакет modular-arithmetic, который реализует ваш тип напоминания, но использует встроенные номера уровней типов и некоторые более сильные синтаксисы. Код короткий, поэтому просто прочитайте источник.