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

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

10 голосов
/ 23 декабря 2010

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

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

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

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

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

Ответы [ 4 ]

11 голосов
/ 23 декабря 2010

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

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 }.

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

7 голосов
/ 24 декабря 2010

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

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

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

В Haskell (+ расширения) вы можете представить эквивалентность, как в приведенном выше коде 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

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

<code>wrong :: a :=: b
wrong = Refl

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

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

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

3 голосов
/ 24 декабря 2010

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

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

2 голосов
/ 23 декабря 2010

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

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

...