Математическое (категориальное) описание классов типов

14

Функциональный язык можно рассматривать как категорию, где его объектами являются типы и функции морфизмов между ними.

Как классы типов вписываются в эту модель?

Я предполагаю, что мы должны рассматривать только те реализации, которые удовлетворяют ограничению, которое имеет большинство классов типов, но которые не выражены в Haskell. Например, мы должны рассматривать только те реализации, Functorдля которых fmap id ≡ idи fmap f . fmap g ≡ fmap (f . g).

Или есть какие-то другие теоретические основы для классов типов (например, основанные на типизированных лямбда-исчислениях)?

Петр Пудлак
источник
1
Возможно, вы захотите быть более точным о том, для чего вы хотите модель. Если вы хотите что-то, что может строго описать допущение открытого мира, поведение разрешения экземпляра, взаимодействие различных расширений GHC и т. Д., Это гораздо сложнее, чем идеализированная версия. Точно так же обратите внимание, что основания часто игнорируются при обсуждении Hask.
CA McCann
4
Классы типов можно рассматривать как сигнатуры (в смысле универсальной алгебры). Коллекция всех сущностей, имеющих одну и ту же сигнатуру (элементы одного и того же типа), является разновидностью .
Дэйв Кларк
1
@DaveClarke: Для меня не сразу очевидно, как таким образом описать классы типов для высших видов, но я не очень знаком с универсальной алгеброй и, возможно, неправильно понимаю соответствие, которое вы имеете в виду ...
CA McCann
1
@camccann: я не уверен, как далеко заходит переписка. Это, конечно, казалось хорошей отправной точкой.
Дэйв Кларк
2
@camccann: просто измените базовую категорию, по которой вы определяете свою алгебру: базовые классы типов, такие как num, являются сигнатурами над категорией типов haskell (или объектами категории Hsk), классы типов над конструкторами типов являются алгебрами над категорией функторов. из Хаск в Хаск. Отметим, что универсальная алгебра полностью включена в понятие алгебры в теории категорий. Также: Дэйв: вы должны превратить свой комментарий в ответ.
Коди

Ответы:

18

Как классы типов вписываются в эту модель?

Короткий ответ: они этого не делают.

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

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

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

В зависимости от выбора экземпляра, который делает компилятор, blah vможет равняться либо либо, "Hello"либо "Goodbye". Следовательно, смысл программы не будет полностью определяться синтаксисом программы, а скорее может зависеть от произвольного выбора, который делает компилятор.

Решение этой проблемы в Haskell состоит в том, чтобы каждый тип имел не более одного экземпляра для каждого класса типов. Чтобы обеспечить это, он разрешает объявления экземпляров только на верхнем уровне и, кроме того, делает все объявления глобально видимыми. Таким образом, компилятор всегда может сообщить об ошибке, если сделано неоднозначное объявление экземпляра.

Однако объявление глобально видимым нарушает композиционную семантику. Что вы можете сделать для восстановления, так это дать семантику разработки для языка программирования - то есть вы можете показать, как переводить программы на Haskell в язык с хорошим поведением и композиционным языком.

На самом деле это также дает вам возможность компилировать классы типов - обычно это называется «преобразованием доказательств» или «преобразованием словаря» в кругах Haskell и является одним из ранних этапов большинства компиляторов Haskell.

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

Нил Кришнасвами
источник
что бегун кандидата , который действительно имеет денотационную семантику iyswim?
Охад Каммар
1
Я понятия не имею, увы.
Нил Кришнасвами
Это заслуживает дополнительного вопроса?
Охад Каммар
@NeelKrishnaswami: У вас есть идеи, как модули ML вписываются в это? А что насчет модулей Agda (которые мне кто-то упомянул, «первого класса»)?
Лий
1
@Lii: Модули ML и записи Agda гораздо лучше себя ведут, но это слишком сложно объяснить в комментарии - задайте вопрос о них, и я (или кто-то еще) объясню.
Нил Кришнасвами