Докажите идемпотентность дизъюнкции типа

Ответ 1

То, что вы просите, невозможно, но что-то совсем похожее на это может сделать. Это невозможно, потому что для доказательства требуется анализ случая на уровне Booleans, но у вас нет данных, которые позволяют сделать такое событие. Исправление состоит в том, чтобы включать только такую ​​информацию через одноэлемент.

Прежде всего, позвольте мне заметить, что ваш тип для idemp немного запутан. Ограничение a ~ b просто одно и то же. Следующие typechecks:

idemq :: p (Or b b) -> p b
idemq = undefined
idemp :: a ~ b => p (Or a b) -> p a
idemp = idemq

(Если у вас есть ограничение a ~ t, где t не содержит a, обычно полезно заменить t на a. Исключение составляет instance declarations: a a in глава экземпляра будет соответствовать чему-либо, поэтому экземпляр будет срабатывать, даже если эта вещь еще не стала явно t. Но я отвлекаюсь.)

Я утверждаю, что idemq не определено, потому что у нас нет полезной информации о b. Единственные доступные данные обитают p -of-something, и мы не знаем, что такое p.

Нам нужно рассуждать по случаям на b. Имейте в виду, что с общими рекурсивными типами мы можем определить булевы уровня типа, которые не являются ни True, ни False. Если я включу UndecidableInstances, я могу определить

type family Loop (b :: Bool) :: Bool
type instance Loop True = Loop False
type instance Loop False = Loop True

поэтому Loop True нельзя свести к True или False, а локально хуже, нет способа показать, что

Or (Loop True) (Loop True) ~ Loop True     -- this ain't so

Там нет выхода. Нам нужны данные времени выполнения, что наш b является одним из хорошо управляемых логических элементов, который как-то вычисляет значение. Итак, петь

data Booly :: Bool -> * where
  Truey   :: Booly True
  Falsey  :: Booly False

Если мы знаем Booly b, мы можем провести анализ случая, который скажет нам, что такое b. Каждый случай будет проходить хорошо. Здесь, как бы я играл, используя тип равенства, определенный с помощью PolyKinds, чтобы собрать факты, а не абстрагироваться от использования p b.

data (:=:) a b where
  Refl :: a :=: a

Наш ключевой факт теперь четко сформулирован и доказан:

orIdem :: Booly b -> Or b b :=: b
orIdem Truey   = Refl
orIdem Falsey  = Refl

И мы можем развернуть этот факт при строгом анализе случаев:

idemp :: Booly b -> p (Or b b) -> p b
idemp b p = case orIdem b of Refl -> p

Анализ дел должен быть строгим, чтобы проверить, что доказательства не являются какой-то зацикленной ложью, а скорее честной по отношению к доброте Refl, которая молча закрывает только доказательство Or b b ~ b, необходимое для исправления типов.

Если вы не хотите четко указывать все эти значения Singleton, вы можете, как предлагает kosmikus, скрыть их в словаре и извлечь их только тогда, когда они вам понадобятся.

У Ричарда Эйзенберга и Стефани Вайрих есть библиотека Template Haskell, которая объединяет эти семьи и классы для вас. SHE также может создавать их и позволяет писать

orIdem pi b :: Bool. Or b b :=: b
orIdem {True}   = Refl
orIdem {False}  = Refl

где pi b :: Bool. расширяется до forall b :: Bool. Booly b ->.

Но это такой лабиринт. Вот почему моя банда работает над добавлением фактического pi в Haskell, являющегося непараметрическим квантификатором (отличным от forall и ->), который может быть создан экземпляром в текущем нетривиальном пересечении между типами Haskell и языками терминов, Этот pi также может иметь "неявный" вариант, где аргумент по умолчанию остается скрытым. Эти два соответственно соответствуют использованию одноэлементных семейств и классов, но нет необходимости определять типы данных три раза, чтобы получить дополнительный набор.

Возможно, стоит упомянуть, что в теории полного типа нет необходимости передавать дополнительную копию логического b во время выполнения. Дело в том, что b используется только для доказательства того, что данные могут переноситься с p (Or b b) в p b, не обязательно для переноса данных. Мы не вычисляем под связующими во время выполнения, поэтому нет возможности приготовить нечестное доказательство уравнения, поэтому мы можем стереть компонент доказательства и копию b, которая его доставляет. Как говорит Рэнди Поллак, лучше всего работать в сильно нормализующем исчислении не нужно нормализовать вещи.

Ответ 2

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

Типичным решением является отражение структуры вида Bool на уровне термина с использованием одноэлементных типов:

data SBool :: Bool -> * where
  SFalse :: SBool False
  STrue  :: SBool True

Для любого b :: Bool существует только один житель SBool b (по модулю undefined, конечно).

С SBool теорема легко доказать (я не знаю, почему вы добавили дополнительное ограничение равенства, я собираюсь удалить ее):

idemp' :: SBool a -> proxy (Or a a) -> proxy a
idemp' SFalse x = x
idemp' STrue  x = x

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

class CBool (b :: Bool) where
  sBool :: SBool b

instance CBool True  where sBool = STrue
instance CBool False where sBool = SFalse

Тогда:

idemp :: CBool a => proxy (Or a a) -> proxy a
idemp = idemp' sBool

Я не думаю, что вы можете избавиться от ограничения CBool, но это тривиально верно для любого a :: Bool, поэтому это не очень сильное предположение.