Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Типотеоретическое

В контексте текущих исследований МакБрайда (Орнаменты) я задумался над тем, является ли размер конечного множества его индуктивным свойством. Да, является.

Напомню, что такое орнаменты и орнаментированные типы. Каноничным примером является List T, тип конечных списков. У списков l: List T есть свойство length l: Nat. Так вот, можно сформировать ограничение типа List T — тип не любых списков, а списков фиксированной длины n. Этот тип (называемый Vec n T) можно определить как зависимую пару: Vect n T = (l: List T, Eq(length l, n)). Но на самом деле это свойство является индуктивным, т.е. Vect n T можно задать как индуктивное семейство типов:
Nil: {T: Type} -> Vect 0 T
Cons: {T: Type} -> {{n: Nat}} -> T-> Vect n T -> Vect (succ n) T

Так вот, у конечных множеств есть свойство size, и оно тоже индуктивно, что позволяет нам создать тип множеств фиксированного размера. Множества мы будем кодировать как пару (T: Type, isMember: T -> Prop). Множество является пустым, если для каждого e: T верно что Not (isMember e). Во множестве не более одного элемента, если для каждой пары а != b верно либо Not (isMember a), либо Not (isMember b). В общем случае во множестве не более n элементов, если для любого v: DistinctVect (n + 1) T по меньшей мере один элемент вне множества. Сперва покажем, как определить для списков свойства forall и notforall
forall: {T: Type} -> {list: List T} -> {predicate: T -> Prop} -> Prop
forall T Nil = True
forall T (Cons a b) = if (predicate a) then (forall T b) else False

notforall: {T: Type} -> {list: List T} -> {predicate: T -> Prop} -> Prop
notforall T Nil p = False
notforall T (Cons a b) p = if (p a) then (forall T b) else True

Теперь определим тип DistinctVect, сразу будем пользоваться тем, что из него есть забывающий функтор в List:
Nil: {T: Type} -> DistinctVect 0 T
Cons: {T: Type} -> {{n: Nat}} -> {head: T} -> {tail: Vect n T} -> (forall T tail (\e: T. Not (Eq(e, head)))) -> Vect (succ n) T

Ну и соответственно
sizeLess: {set: (T: Type, isMember: T -> Prop)} -> {n: Nat} -> Prop
sizeLess (T, isMember) n = ({dv: DistinctVect n T} -> notForall T dv isMember)

sizeEq: {set: (T: Type, isMember: T -> Prop)} -> {n: Nat} -> Prop
sizeEq set 0 = SizeLess set 1
sizeEq set (succ n) = (SizeLess set n, Not(SizeLess set (succ n)))

FiniteSet: {T: Type} -> {size: Nat} -> Type
FiniteSet n T = (isMember: T -> Prop, sizeEq (T, isMember) n)

Collection (nontraversable finite multiset) является контейнером в стандартном смысле S ◁ F тогда и только тогда, когда система типов допускает построение универсальных объектов. Тогда Collection = Nat ◁ (\n. Universal(FiniteSet n))

Collection очень важный тип в категории контейнеров Cont. Из любого другого контейнера в него существует одно и только одно отображение, shape forgetting functor. Во всех известных мне ЯП (хоть функциональных, хоть нет) задать технически точно тип этого родителя всех коллекций невозможно. А меж тем наличие такого типа позволяет формулировать очень общие вещи вроде sort: {T: Type} -> Ord T -> Collection T -> List Collection T.
Если у нас есть такое отображение f: Vect n A -> B, что f = f.p для любой перестановки p: Perm n (то есть отображение не зависит на самом деле от порядка аргумента), то оно порождает отображение lift f: FiniteMultiSet n A. Конструктивные отображения из коллекций исчерпываются отображениями, построенными таким способом. Все операции над коллекциями выражаются через три следующих:
– extract извлекает элемент из коллекции, где все элементы равны (то есть коллекции из одного элемента, который, однако может иметь любую положительную кратность);
– обобщённый map, который принимает пару (элемент A, кратность), а возвращает Collection B.
– reduce коммутативной и ассоциативной операцией.
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments