Haskell / GHC: Как писать предикаты для натуральных объектов типа

Question

Я мог бы поклясться, что недавно видел статью по этому вопросу, но не могу ее найти.

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

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Modulo where

-- (pseudo-)binary representation of 
-- numbers mod n
--
--  e.g. Mod Seven contains
--    Zero . Zero . Zero $ Stop
--    Zero . Zero . One  $ Stop
--    Zero . One . Zero $ Stop
--    Zero . One . One  $ Stop
--    One . Zero . Zero $ Stop
--    One . Zero . One  $ Stop
--    One . One $ Stop 
data Mod n where
  Stop :: Mod One
  Zero :: Split n => Mod (Lo n) -> Mod n
  One  :: Split n => Mod (Hi n) -> Mod n

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- predicate to allow us to compare 
-- natural numbers
class Compare n n' b | n n' -> b

-- type-level ordering
data LT
data EQ
data GT

-- base cases
instance Compare One One EQ
instance Compare One (Succ n) LT
instance Compare (Succ n) One GT

-- recurse
instance Compare n n' b => Compare (Succ n) (Succ n') b

-- predicate to allow us to break down
-- natural numbers by their bit structure
--
-- if every number mod n can be represented in m bits, then
class Split n where
  type Lo n -- number of values mod n where the m'th bit is 0
  type Hi n -- number of values mod n where the m'th bit is 1

-- base case, n = 2
-- for this, we only need m=1 bit
instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

-- recurse
--  if (Lo n) == (Hi n), then n = 2^m, so
--  the values mod (n+1) will require one extra bit
instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) where
  type Lo (Succ n) = n    -- all the numbers mod n will be prefixed by a 0
  type Hi (Succ n) = One  -- and one extra, which will be 10...0

-- recurse
--  if (Lo n) > (Hi n), then n < 2^m, so
--  the values mod (n+1) still only require m bits
instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) where
  type Lo (Succ n) = Lo (n)       -- we've got the same number of lower values
  type Hi (Succ n) = Succ (Hi n)  -- and one more higher value

Моя текущая реализация выдает кучу ошибок компилятора:

Nat.hs:60:8:
    Conflicting family instance declarations:
      type Lo Two -- Defined at Nat.hs:60:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:61:8:
    Conflicting family instance declarations:
      type Hi Two -- Defined at Nat.hs:61:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Nat.hs:66:10:
    Duplicate instance declarations:
      instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n)
        -- Defined at Nat.hs:66:10-62
      instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n)
        -- Defined at Nat.hs:73:10-62

Nat.hs:67:8:
    Conflicting family instance declarations:
      type Lo (Succ n) -- Defined at Nat.hs:67:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:68:8:
    Conflicting family instance declarations:
      type Hi (Succ n) -- Defined at Nat.hs:68:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Что заставляет менямне кажется, что я пишу свои предикаты неправильно, если они считают, что они противоречат друг другу.

Как я могу сделать их правильно?

Answer 1

Проблема конфликта достаточно проста.Правила для перекрывающихся семейств типов довольно просты:

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

Обратите внимание, что синтаксически указывает равно.Рассмотрим эти два случая:

instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

instance Split (Succ n) where
  type Lo (Succ n) = Lo (n)  
  type Hi (Succ n) = Succ (Hi n)

Two определяется как Succ One, и синонимы простого типа расширяются в целях синтаксического равенства, поэтому они равны с левой стороны;но это не правая часть, отсюда и ошибка.

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

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

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- type-level ordering
data LT
data EQ
data GT

Перепишите функцию Compare как семейство типов:

type family Compare n m :: *
type instance Compare One One = EQ
type instance Compare (Succ n) One = GT
type instance Compare One (Succ n) = LT
type instance Compare (Succ n) (Succ m) = Compare n m

Теперь для обработки условныхнам понадобится какое-то семейство типа «управление потоком».Я определю здесь что-то более общее для назидания и вдохновения;специализируюсь по вкусу.

Мы дадим ему предикат, вход и две ветви на выбор:

type family Check pred a yes no :: * 

Нам понадобится предикат для тестирования Compare 's результат:

data CompareAs a
type instance (CompareAs LT) LT yes no = yes 
type instance (CompareAs EQ) LT yes no = no
type instance (CompareAs GT) LT yes no = no
type instance (CompareAs LT) EQ yes no = no 
type instance (CompareAs EQ) EQ yes no = yes
type instance (CompareAs GT) EQ yes no = no
type instance (CompareAs LT) GT yes no = no
type instance (CompareAs EQ) GT yes no = no
type instance (CompareAs GT) GT yes no = yes

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

В этом случае проще было бы просто определить функцию анализа случая по результатам сравнения:

type family CaseCompare cmp lt eq gt :: *
type instance CaseCompare LT lt eq gt = lt
type instance CaseCompare EQ lt eq gt = eq
type instance CaseCompare GT lt eq gt = gt

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

В любом случае.Мы можем разделить класс ... er, Split на семейства несвязанных типов:

data Oops

type family Lo n :: *
type instance Lo Two = One
type instance Lo (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  (Succ n)
                  (Lo (Succ n))

type family Hi n :: *
type instance Hi Two = One
type instance Hi (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  One
                  (Succ (Hi (Succ n)))

Наиболее важным моментом здесь является (на первый взгляд, избыточность) использование (Succ (Succ n)) - причина этого заключается в том, чточто два Succ конструктора необходимы для того, чтобы отличить аргумент от Two, что позволяет избежать ошибок конфликта, которые вы видели.

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