Обобщение экспоненциального типа

Как (если вообще) экспоненциальная интерпретация (->) (a -> b как ba) распространяется на категории, отличные от Hask/Set? Например, может показаться, что интерпретация категории недетерминированных функций примерно Kliesli [] a b как 2a * b (a -> b -> Bool).


haskell category-theory category-abstractions
person David Harrison    schedule 26.12.2014    source источник
comment
Я не уверен, что понимаю, о чем вы спрашиваете. Экспоненты можно найти в любой декартовой замкнутой категории. en.wikipedia.org/wiki/Cartesian_closed_category   -  person chi    schedule 26.12.2014
comment
Экспоненциальная интерпретация a -> b есть b^a. Рассмотрим a -> (), в котором проживает только 1^a=1 жителей, а именно const (). С другой стороны, в () -> b проживает b^1=b жителей, по одному на каждого жителя b.   -  person Cirdec    schedule 26.12.2014
comment
@chi Расширьте это чуть-чуть - просто скопируйте некоторые определения из Википедии - и я проголосую за ваш ответ.   -  person Daniel Wagner    schedule 26.12.2014
comment
@Cirdec - Знаете ли вы о существующем ответе SO на этот счет? Я хочу добавить перекрестную ссылку на мой несвязанный ответ, который затрагивает эту тему. (Этот комментарий не по теме будет самоуничтожаться всякий раз, когда я вспомню его уничтожить.)   -  person Christian Conkle    schedule 27.12.2014
comment
@ChristianConkle Этот ответ содержит аналогичное объяснение stackoverflow.com/a/9197803/414413   -  person Cirdec    schedule 27.12.2014

Ответы (1)


arrow_upward
4
arrow_downward

Понятие экспоненты может быть определено в общих чертах, за исключением Hask/Set. Категория с экспонентами и произведениями называется декартовой закрытой категорией. Это ключевое понятие в теоретической информатике, поскольку каждый c.c. категория по сути является моделью типизированного лямбда-исчисления.

Грубо говоря, в декартовой замкнутой категории для любой пары объектов a,b существуют:

  • объект продукта (a * b) и
  • экспоненциальный объект (b^ab)

с морфизмами

  • eval : (b^a)*a -> b (в Haskell: \(f,x) -> f x, применяется AKA)
  • для любого f : (a*b)->c существует Lf : a -> (c^b) (в Haskell: curry f)

удовлетворяющие уравнению «они пользуются в лямбда-исчислении», т. е. если f : (a*b)->c, то:

  • f = (Lf * id_a) ; eval

В Haskell последнее уравнение выглядит так:

  • f = \(x :: (a,b), y :: a) -> apply (curry f x, id y) where apply (g,z) = g z

или, используя стрелки,

  • f = (curry f *** id) >>> apply where apply (g,z) = g z
person chi    schedule 27.12.2014