Как я могу указать, что две операции коммутируют в классе типов?

Question

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

То, что я не могу понять, - это как сформулировать контракт, который операции должны коммутировать в спецификации класса типов.

Для простого примера:

class Direction a where
  turnLeft :: a -> a
  turnRight :: a -> a

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

Answer 1

Вам нужен класс типов, который включает в себя проверочную нагрузку, что-то вроде псевдо-Хаскелла ниже:

class Direction a where
    turnLeft  :: a -> a
    turnRight :: a -> a
    proofburden (forall a. turnLeft (turnRight a) === turnRight (turnLeft a))

Здесь все экземпляры должны предоставлять функции и доказательства для проверки типа компилятором. Это желаемое за действительное (для Haskell), поскольку Haskell не имеет (ну, ограниченно) понятия доказательства.

OTOH, Coq является корректным помощником для зависимо типизированного языка, который можно извлечь в Haskell. Хотя я никогда раньше не использовал классы типов Coq, быстрый поиск полезен, например:

Class EqDec (A : Type) := {
   eqb : A -> A -> bool ;
   eqb_leibniz : forall x y, eqb x y = true -> x = y }.

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

Answer 2

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

record Direction (a : Set) : Set₁ where
  field
    turnLeft  : a → a
    turnRight : a → a
    commLaw   : ∀ x → turnLeft (turnRight x) ≡ turnRight (turnLeft x)

---

Я решил отредактировать пост и ответить на вопрос, почему вы не можете сделать это в Хаскеле.

В Haskell (+ extensions) вы можете представить эквивалентность, использованную в коде Agda выше.

{-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}

data (:=:) a :: * -> * where
  Refl :: a :=: a  

Это представляет теоремы о равенстве двух типов. Например a эквивалентно b является a :=: b,

Там, где мы эквивалентны, мы можем использовать конструктор Refl, Используя это, мы можем выполнять функции по доказательствам (значениям) теорем (типов).

-- symmetry
sym :: a :=: b -> b :=: a
sym Refl = Refl

-- transitivity
trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl

Все они корректны по типу и, следовательно, верны. Однако это;

wrong :: a :=: b
wrong = Refl

явно неправильно и действительно не проходит проверку типов.

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

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

Answer 3

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

Что-то в этом роде уже можно найти в пакете шашек; Вы можете проконсультироваться с ним для вдохновения.

Answer 4

То, что я не могу понять, - это как сформулировать контракт, который операции должны коммутировать в спецификации класса типов.

Причина, по которой вы не можете понять это, заключается в том, что это невозможно. Вы не можете закодировать этот тип свойства в типах - по крайней мере, в Haskell.