[обратите внимание, что переполнение стека, к сожалению, не поддерживает mathjax, но, как вы, кажется, уже получили степень по математике, я предполагаю, что вы можете прочитать ее]
Вы хотите, чтобы:
m (m x y) z = m x (m y z) -- (1)
Но для этого вам нужен способ проверить это. Таким образом, вы или ваш компилятор (или помощник по проверке) должны создать доказательство этого. И вопрос в том, какой тип является доказательством (1)?
Можно представить себе некоторый тип Proof, но тогда, возможно, вы могли бы просто построить доказательство того, что 0 = 0 вместо доказательства (1) и оба будут иметь тип Proof. Так что вам нужен более общий тип. Я не могу решить, как разбить остальную часть вопроса, поэтому я пойду за кратким объяснением изоморфизма Карри-Ховарда, за которым последует объяснение того, как доказать, что две вещи равны, и затем, как зависимые типы релевантны.
Изоморфизм Карри-Говарда говорит, что пропозиции изоморфны типам, а доказательства изоморфны программам: тип соответствует предложению, а доказательство этого предложения соответствует программе, создающей значение, населяющее этот тип. Игнорируя, сколько может быть выражено в виде типов, примером может быть то, что тип A * B (записан (A, B) на Хаскеле) соответствует предложению «A и B», тогда как тип A + B (написано Either A B в Хаскеле) соответствует предложению «A или B». Наконец, тип A -> B соответствует «A подразумевает B», поскольку доказательством этого является программа, которая принимает доказательства A и дает вам свидетельство B. Следует отметить, что нет способа выразить not A, но можно представить добавление типа Not A со встроенными типами Either a (Not a) для закона исключенного среднего, а также Not (Not a) -> a и a * Not a -> Void (где Void - это тип, который не может быть обитаемым и, следовательно, соответствует false), но тогда невозможно действительно запустить эти программы, чтобы получить конструктивистские доказательства.
Теперь мы проигнорируем некоторые реалии Хаскелла и представим, что не существует способов обойти эти правила (в частности undefined :: a говорит, что все верно, а unsafeCoerce :: a -> b говорит, что что-либо подразумевает что-то еще, или просто другие функции, которые не не возвращайтесь туда, где их существование не подразумевает соответствующего доказательства).
Итак, мы знаем, как объединять предложения, но каким может быть предложение? Ну, можно сказать, что два типа равны. В Haskell это соответствует GADT
data Eq a b where Refl :: Eq c c
Где этот конструктор соответствует рефлексивному свойству равенства.
[примечание: если вы все еще заинтересованы, вам может быть интересно посмотреть на однолистные основы Воеводского в зависимости от того, насколько вас интересует идея «теории гомотопического типа»]
Так что мы можем доказать что-то сейчас? Как насчет переходного свойства равенства:
trans :: Eq a b -> Eq b c -> Eq a c
trans x y =
case x of
Refl -> -- by this match being successful, the compiler now knows that a = b
case y of
Refl -> -- and now b = c and so the compiler knows a = c
Refl -- the compiler knows that this is of type Eq d d, and as it knows a = c, this typechecks as Eq a c
Такое ощущение, что кто-то ничего не доказал (особенно потому, что это в основном полагается на то, что компилятор знает транзитивные и симметричные свойства), но такое же чувство возникает и при доказательстве простых вещей в логике.
Итак, как бы вы могли доказать исходное утверждение (1)? Хорошо, давайте представим, что мы хотим, чтобы тип c был моноидом, тогда мы также должны доказать, что $ \ forall x, y, z: c, m (mxy) z = mx (myz). $ Итак, нам нужен способ выразить m (m x y) z как тип. Строго говоря, это не зависимые типы (это можно сделать с помощью DataKinds для продвижения значений и семейств типов вместо функций). Но вам нужны зависимые типы, чтобы типы зависели от значений. В частности, если у вас есть тип Nat натуральных чисел и семейство типов Vec :: Nat -> * (* - это тип (тип чтения) всех типов) векторов фиксированной длины, можно определить функцию зависимых типов mkVec :: (n::Nat) -> Vec n. Обратите внимание, как тип вывода зависит от значения входа.
Таким образом, ваш закон должен иметь функции, переведенные на уровень типов (пропуская вопросы о том, как определить равенство типов и равенство значений), а также зависимые типы (составленный синтаксис):
class Monoid c where
e :: c
(*) :: c -> c -> c
idl :: (x::c) -> Eq x (e * x)
idr :: (x::c) -> Eq x (x * e)
assoc :: (x::c) -> (y::c) -> (z::c) -> Eq ((x * y) * z) (x * (y * z))
Наблюдайте, как типы имеют тенденциюстать большим с зависимыми типами и доказательствами.В языке, в котором отсутствуют классы типов, можно занести такие значения в запись.
Заключительное замечание по теории зависимых типов и тому, как они соответствуют изоморфизму Карри Говарда.
Зависимые типы могутможно считать ответом на вопрос: какие типы соответствуют предложениям $ \ forall x \ in S \ quad P (x) $ и $ \ Существует y \ in T \ quad Q (y)? $
Ответ заключается в том, что вы создаете новые способы создания типов: зависимый продукт и зависимая сумма (побочный продукт).Зависимый продукт выражает «для всех значений $ x $ типа $ S, $ есть значение типа $ P (x). $». Нормальным продуктом будет зависимый продукт с $ S = 2, $ типом, населеннымдва значения.Зависимый продукт может быть написан (x:T) -> P x.Зависимая сумма говорит «некоторое значение $ y $ типа $ T $ в сочетании со значением типа $ Q (y). $», Это можно записать как (y:T) * Q y.
. Можно думать о них какобобщение произвольно проиндексированных (со) произведений из множества Set в общие категории, где можно разумно написать, например, $ \ prod_ \ Lambda X (\ lambda), $, а иногда такие обозначения используются в теории типов.