dacha

HHKB

Happy Hacking Keyboard Professional 2 Type-S

Сегодня мне на день рождения мой учитель информатики подарили культовую клавиатуру для Хакеров, о чем и будет этот пост. Она настолько охуенная, что раздумывать не пришлось, все расскажу сразу вам без утайки, все что скрыто покажу.



Но прежде чем, начать историю, хочу отметить, что началась она с нашей украинской зрадоньки, прямо в отделении Укрпочты клавиатуру спиздили (думали, раз посылка из Японии, то точно можно будет на кардачах толкнуть за дорого) и вернули только после жестких наездов. Но речь не об этом, она у меня и это главное.

Начнем с клавиатуры, это одна из самых трушных, я не специалист в механике (но хотел бы стать), но судя по всему спроектирована грамотно, так как напоминает IBM Model M, а также клаву от Symbolics. Названием Happy Hacking Keyboard Type-S в американской версии (длинный Return, вместо японского большого Enter) подчеркивает спортивность Type-S (готовьтесь разминать пальцы) и принадлежность к хакерской культуре, убирая с клавиатуры все надписи — трушным хакерам они не нужны. Клавиатура настолько мимимишная что все страницы приходится переводить с японского на английский, но зато в этой клавиатуре идут сканкоды в PDF и хакерском TXT форматах. Документация, понятное дело, на японском. Признак трушного продукта — отсутствие локализации в документации!

Все предупреждения описаны в нотисах перед покупкой (например одним из пунктов идет, что ее нельзя дизассемблировать), что очень круто, но клавиатура действительно клевая, привыкаешь к ней быстро.

Когда прикасаешься к клаве, сразу вспоминаешь IBM PS/2 (первый мой комп в школе), шум дискеток с Borlang Pascal 7.0, которых было больше 10 со всеми исходниками Turbo Vision, и Object Library. Еще был Turbo Pascal 5.5, который был черно-сине-красным, а не зеленово-красно-песочным как в старших версиях. Я отвлекся.

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

Немного поклацав по клавиатуре, в игровом режиме определил курсоры. На верхнем рисунке функциональная клавиша — синяя. Курсоры с Fn — белые. Alt — зеленый. Pg-down, Pg-up - желтые. Остальное — очеивдное. Backspace и Delete имеет хардварный свитч. Mac/PC тоже одним свичем переключается. Есть свитч для переключения между Left-Alt и Left-Fn. Всего свичей пять. Полный дзен. Привожу раскладку клавиатуры для Mac режима (но в вдругих цветах). Остальные режимы можно посмотреть тут.



Я думал хуйня начнется, когда я подключу эту клавиатуру к UNIX-терминалу, но проблем не произошло, все заработало без каких либо перенастроек, Mac, mc, lynx-like motion — все работает как и должно работать, только иногда дабл-эскейп (кстати дичь полнейшая, в FAR такого нет) смазывается при конфликте с fn. На Air клаве пока минимум миссов и фастест моде у меня эвер. Но я считаю, что полезно иногда свою нейронную сеточку заставить поучиться новым клавам, новым раскладкам. Это как в игрушки играть на Playstation, только этим можно играться непосредственно зарабатывая деньги — вбивая строки кода за кровные доллары в чужие репозитории.

Вообщем часик посидел, поползал по файловой системе, пока приучил к lynx-like моушину, он должен быть быстрый и до автоматизма иначе ты улитка. Потом к текстовому редактору. Основные упражнения это: вперед/вконец строки (левые правый курсор, Alt, Fn), двигать исхдоник "под собой" как pg-up/pg-down (верхний нижний курсор, Alt, Fn), pg-up/pg-down — просто желтые с Fn. Теперь вы знаете редактор. Пока еще текст не редакторировал, так чтобы постоянно, но уже понятно как будет все выглядеть.

Клавиатура находится за пределами оценок, так как авторы хотели сделать шедевр. Продукт действительно хороший, все работает ожидаемо. Жалко, что у меня нет стационарного компьютера, такая клавиатура стоит того, чтобы его купить. Только не десктоп или тауэр, а Blade 1U к такой клаве надо, и Hercules монитор. Делают сейчас интересно монохромные желтые под старину аля Геркулесы? Именнно такой нужен к этой клавиатуре.
sea

Програмологія: Розслідування фальшивих академіків НАН

Поки ми готуємо документи, якими ми намагатимемось бомбардувати наші корумповані прикордонні служби, прокуратуру та інші установи, на які тільки у нас вистачить грошей, у зв'язку з недопуском в Україну видатного математика-педагога, дійсного члена комітету по стандартизації мови Haskell, я вирішив поцікавитися, а які у Українців є опції, якщо не Брагілєвскьий, то хто в Україні претендує на звання спеціаліста з поєднання логіки та математики? Результати мене надзвичайно здивували, виявляється у нас є академік НАН України, який є прямим конкурентом Хаскеля Карі, Філіпа Вадлера, Стівена Кліні, Хенка Барендрехта та інших. Однак, що дивно, у списку його праць жодним чином немає згадок про його закордонних колег. Я вирішив провести розслідування і детальний аналіз цього академіка разом з його працями, аби з'ясувати, яке майбутнє чекає Україну в контексті приходу алгебраїчних мов програмування у повсякденну інженерну практику (перш за все я маю на увазі функціональні мови програмування, які ви всі добре знаєте: ML, Haskell, Scala, Erlang, Clojure).

Редько Володимир Никифорович

Граматика

Почнему з базової елементарної освіти 1—9 класів. Зайдемо на сайт Кафедра теорії та технології програмування, читаємо:

"Повні класи вичіслімих функцій різних рівнів абстракції були описані." — формулювання речень у стилі магістра Йоди з граматичними помилками.
"Мета проекту: автоматизації математичних відрахувань до різних областях" — взагалі незрозуміло про що йде мова.
"Деякі програми САД є:
розподілених автоматизованих докази теорем
верифікації математичних текстів
дистанційного навчання в математичних дисциплін
будівництво баз даних для математичних теорій
" — таке враження, що перекладали translate.google.com, але якщо подумати над суттю, то вийде, що максимально, що тут можна собі уявити — це "блокчейн з теоремами", рівень магістерських робіт на заході.

"Розробка програмних засобів для Склад називному Мови (CNL)
Короткий опис: Є розробки програмних засобів для підтримки не менше трьох CNL:
Бекон (Основні CNL)
DECON (Описова CNL = Бекон + описові вирази нових складів через основні з них)
Recon (Рекурсивні CNL = DECON + рекурсивного вираження нових складів через основні з них)
" — тут я так розумію Бекон, Декон та Рекон, це щось накшталт Relux, Redux та React, торгові марки університету, які вочевидь є темами захисту докторських дисертації в Національному Університеті України ім. Тараса Шевченка. Направді абсолютно синтетичні, надумані теорії які немають жодного зв'язку з реальністю.
"беконом і DECON знаходяться в бета-версії стадії тестування" — речення побудоване роботами-дибілами.
"Хід об’єкту: перша версія готова" — посилання не працює, в rar файлах вірогідність відшукати щось працююче хоча б на Delphi дорівнює нулю.

Аналіз програмології, як конкретної науки

Я буду називати це спробою аналізу, тому, що заглиблюватися в цей божевільний світ маразму у мене немає часу та можливостей. Почнемо зі списку праць нешанованого академіка, та вікіпедії.

"Неоклассические логики предикатов" — неокласичні, ну добре, про Хаскеля Карі забули, а вже в неокласики.
"Композиционно-номинативный подход к уточнению понятия программы" — 1999 рік, у той час коли на заході вже верифікували процесори за допомогою ACL2, Coq та HOL.
"Композитционные базы данных" — орфографія збережена, учень цього академіка Буй полюбляє бази даних, тому наукові роботи пестрять CASE системами та SQL моделями на Delphi.

Ось ці теми дуже вражають своєю теоретичністю:
"Базы данных и информационные системы" — тут вчать писати INNER JOIN.
"Введение в операционные системы" — цікаво чи інститут Шевченко зробив хоч одну операційну систему, яка була проваджена виробництво (відповідь очевидна, ні)
"Неподвижные точки и операторы замыкания: программологические аспекты" — тут йдеться мова очевидно про фікспойнти, F-алгебри, однак згадки про Філіпа Вадлера, та Вармо Вене ви там не знайдете. А коли відриєте дисертацію на цю тему то у вас випаде останнє волосся.

Наукові зв'язки
"Кафедра теорії та технології програмування має наукові зв’язки з провідними учбовими та науковими установами у багатьох країнах світу: Данія, Макао, Молдова, Латвія, Нідерланди, Німеччина, Польща, Росія, США, Фінляндія, Франція, Чехія" — очевидно ніяких посилань, я впевнений якщо запитати з ким вони там зв'язуються то виявиться що половина неправда, а інша половина це їхні студенти які влаштувалися там з "програмологією" в Макао.

Приклади робіт учнів цього академіка

Омельчук Людмила Леонідівна УДК 681.3 АКСІОМАТИЧНІ СИСТЕМИ СПЕЦИФІКАЦІЙ ПРОГРАМ НАД НОМІНАТИВНИМИ ДАНИМИ



Дослідження декартових добутків, транзитивності. Нагадую — це не реферат, а дисертація на здобуття кандидата! Ви думаеєте, що це одна стаття така? Будь-яку берете, розбираєте на атоми і впевнюєтеся, що це якшо не шизофренія, то просто балаболство і накидання математичних термінів для вигляду у журнал "Мурзілка".

УДК 681.3.06 Бойко Б. I. СТРУКТУРА ІМЕНУВАНЬ У ПРОГРАМУВАННІ



Робота Бойко присвячена тому, як називати змінні в мові програмування Delphi, і приклад як роботи запити на мові Delphi в базу даних SQL.

Список людей які захищалися

Однак сам академік, який придумав "Програмологію" це гідра, яка генерує своїх клонів: Редько, Нікітченко, Буй, син Редька (очевидно, що корупція), та інші менш значущі доцентіки. Усі вони начебто займаються математичною логікою та відносять себе до мінжародної школи "Програмології" яку вигадав Редько і про яку більше ніхто крім цього гадюшніка не знає.

http://science.univ.kiev.ua/research/scientific_school/programologiya-ta-yiyi-zastosuvannya/

P.S. Стаття буде наповнюватися новими прикладами математичного аферизму та шизофренії в КНУ ім. Шевченка та академіків НАН.

Список літератури для аналізу

[1] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/86588/08-Redko.pdf?sequence=1
[2] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/1530/08-Redko.pdf?sequence=1
[3] http://knutd.edu.ua/publications/pdf/Visnyk/2012-5/34_42.pdf
[4] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/1454/%E2%84%962-3_2008_Zybenko.pdf?sequence=1

Прошу долучатися та додавати ті дисертації які заслуговують Фрунзе 103 на вашу думку. Фактично будь-яка робота, якщо детально її проаналізувати це мімікрія під головного Програмолога України.
sea

binnat.ctt

nponeccop импортнул, я померял.

data binN = binN0 | binNpos (p : pos)

NtoBinN : nat -> binN = split
  zero  -> binN0
  suc n -> binNpos (NtoPos (suc n))

doublesN : nat -> nat -> nat = split
  zero  -> \(m:nat) -> m
  suc n -> \(m:nat) -> doublesN n (doubleN m)


Это мгновенно (транспортная decode):

> let a: binN = NtoBinN (doublesN n10 n10) in a
Checking: a
EVAL: binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x1 (x0 pos1)))))))))))))


Это долго (минуты, через isoPath):

> let a: binN = transNeg binN nat PathbinNN (doublesN n10 n10) in a
Checking: a
EVAL: binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x1 (x0 pos1)))))))))))))


Доказательство, что 2^20 * e = 2^5 * (2^15 * e), мгновенно.

data Double =
  D (A : U)            -- carrier
    (double : A -> A)  -- doubling function computing 2 * x
    (elt : A)          -- element to double

carrier : Double -> U = split D c _ _ -> c

iter (A : U) : nat -> (A -> A) -> A -> A = split
  zero  -> \(f:A->A) (z:A) -> z
  suc n -> \(f:A->A) (z:A) -> f (iter A n f z)

double : (D : Double) -> (carrier D -> carrier D)
 = split D _ op _ -> op

doubles (D : Double) (n : nat) (x : carrier D) : carrier D =
  iter (carrier D) n (double D) x

propDouble (D : Double) : U
 = Path (carrier D) (doubles D n20 (elt D))
                    (doubles D n5 (doubles D n15 (elt D)))

bin1024 : binN = binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))

doublesBinN : nat -> binN -> binN = split
  zero  -> \(m:binN) -> m
  suc n -> \(m:binN) -> doublesBinN n (doubleBinN m)

DoubleBinN : Double = D binN doubleBinN bin1024

propBin : propDouble DoubleBinN = <_> doublesBinN n20 (elt DoubleBinN)

> :n propDouble
NORMEVAL: \(D : Double) -> PathP ( carrier D) (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (elt D))))))))))))))))))))) (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (elt D)))))))))))))))))))))

> :n propBin
NORMEVAL:  binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))))))))))))))))))))))
sea

Cubical Parser in Erlang

Сделано все, кроме гомотопических прититивов <> @ []. Вернулись на позапрошлогодний уровень EXE. Пришлось сделать case аналисис в стиле ML языков (с палками), так как, говорят 2D синтаксис голым эрланговским LALR не возьмешь. С where тоже проблемы, пришлось делать карированую версию where. Оно и логично — в минималистичных ядрах должно быть все карированое. YECC файл занимает ровно 50 строчек, в отличие от 261 строки для EXE. В примере показан Хрономирфизм и Категорная Семантика односвязного списка

module lam1 where

listCategory (A: U) (o: listObject A): U = undefined

histo (A:U) (F: U -> U) (X: functor F) (f: F (cofree F A) -> A) (z: fix F): A
  = extract A F ((cata (cofree F A) F X (\(x: F (cofree F A)) -> CoFree (Fix (CoBindF (f x) ((X.1 (cofree F A) (fix (cofreeF F A)) (uncofree A F) x)))))) z) where
  extract (A: U) (F: U -> U): cofree F A -> A = split
    | CoFree f -> unpack_fix f where
  unpack_fix: fix (cofreeF F A) -> A = split
    | Fix f -> unpack_cofree f where
  unpack_cofree: cofreeF F A (fix (cofreeF F A)) -> A = split
    | CoBindF a -> a

futu (A: U) (F: U -> U) (X: functor F) (f: A -> F (free F A)) (a: A): fix F
  = Fix (X.1 (free F A) (fix F) (\(z: free F A) -> w z) (f a)) where
  w: free F A -> fix F = split
    | Free x -> unpack x where
  unpack_free: freeF F A (fix (freeF F A)) -> fix F = split
    | ReturnF x -> futu A F X f x
    | BindF g -> Fix (X.1 (fix (freeF F A)) (fix F) (\(x: fix (freeF F A)) -> w (Free x)) g) where
  unpack: fix (freeF F A) -> fix F = split
    | Fix x -> unpack_free x

chrono (A B: U) (F: U -> U) (X: functor F)
       (f: F (cofree F B) -> B)
       (g: A -> F (free F A))
       (a: A): B = histo B F X f (futu A F X g a)

listAlg (A : U) : U
    = (X: U)
    * (nil: X)
    * (cons: A -> X -> X)
    * Unit

listMor (A: U) (x1 x2: listAlg A) : U
    = (map: x1.1 -> x2.1)
    * (mapNil: Path x2.1 (map (x1.2.1)) (x2.2.1))
    * (mapCons: (a:A) (x: x1.1) -> Path x2.1 (map (x1.2.2.1 a x)) (x2.2.2.1 a (map x)))
    * Unit

listObject (A: U) : U
    = (point: (x: listAlg A) -> x.1)
    * (map: (x1 x2: listAlg A)
            (m: listMor A x1 x2) ->
            Path x2.1 (m.1 (point x1)) (point x2))
    * Unit


{module,{id,1,"lam1"},
        {where,1},
        [],
        [{def,{id,5,"listCategory"},
              {tele,[{id,5,"A"}],
                    {id,5,"U"},
                    {tele,[{id,5,"o"}],{app,{id,5,"listObject"},{id,5,"A"}},[]}},
              {id,5,"U"},
              {id,5,"undefined"}},
         {def,{id,7,"histo"},
              {tele,[{id,7,"A"}],
                    {id,7,"U"},
                    {tele,[{id,7,"F"}],
                          {pi,{id,7,"U"},{id,7,"U"}},
                          {tele,[{id,7,"X"}],
                                {app,{id,7,"functor"},{id,7,"F"}},
                                {tele,[{id,7,[...]}],
                                      {pi,{app,...},{...}},
                                      {tele,[...],...}}}}},
              {id,7,"A"},
              {app,{app,{app,{id,8,"extract"},{id,8,"A"}},{id,8,"F"}},
                   {app,{app,{app,{app,{app,{id,8,[...]},{app,{...},...}},
                                       {id,8,"F"}},
                                  {id,8,"X"}},
                             {app,{lam,{tele,[{id,...}],{app,...},[]},{id,8,[...]}},
                                  {app,{id,8,[...]},{app,{...},...}}}},
                        {id,8,"z"}}},
              {def,{id,9,"extract"},
                   {tele,[{id,9,"A"}],
                         {id,9,"U"},
                         {tele,[{id,9,"F"}],{pi,{id,9,[...]},{id,9,...}},[]}},
                   {pi,{app,{app,{id,9,"cofree"},{id,9,"F"}},{id,9,"A"}},
                       {id,9,"A"}},
                   {split,[{br,[{id,10,"CoFree"},{id,10,[...]}],
                               {app,{id,10,...},{id,...}}}]},
                   {def,{id,11,"unpack_fix"},
                        [],
                        {pi,{app,{id,...},{...}},{id,11,...}},
                        {split,[{br,...}]},
                        {def,{id,...},[],...}}}},
         {def,{id,16,"futu"},
              {tele,[{id,16,"A"}],
                    {id,16,"U"},
                    {tele,[{id,16,"F"}],
                          {pi,{id,16,"U"},{id,16,"U"}},
                          {tele,[{id,16,"X"}],
                                {app,{id,16,"functor"},{id,16,[...]}},
                                {tele,[{id,16,...}],{app,{...},...},{tele,...}}}}},
              {app,{id,16,"fix"},{id,16,"F"}},
              {app,{id,17,"Fix"},
                   {app,{app,{app,{app,{fst,{id,17,...}},{app,{app,...},{...}}},
                                  {app,{id,17,[...]},{id,17,...}}},
                             {lam,{tele,[{id,17,...}],{app,{...},...},[]},
                                  {app,{id,17,...},{id,...}}}},
                        {app,{id,17,"f"},{id,17,"a"}}}},
              {def,{id,18,"w"},
                   [],
                   {pi,{app,{app,{id,18,"free"},{id,18,[...]}},{id,18,"A"}},
                       {app,{id,18,"fix"},{id,18,"F"}}},
                   {split,[{br,[{id,19,[...]},{id,19,...}],
                               {app,{id,...},{...}}}]},
                   {def,{id,20,"unpack_free"},
                        [],
                        {pi,{app,{...},...},{app,...}},
                        {app,{split,...},{...}},
                        {def,{...},...}}}},
         {def,{id,26,"chrono"},
              {tele,[{id,26,"B"},{id,26,"A"}],
                    {id,26,"U"},
                    {tele,[{id,26,"F"}],
                          {pi,{id,26,"U"},{id,26,"U"}},
                          {tele,[{id,26,"X"}],
                                {app,{id,26,[...]},{id,26,...}},
                                {tele,[{id,...}],{pi,...},{...}}}}},
              {id,29,"B"},
              {app,{app,{app,{app,{app,{id,29,"histo"},{id,29,[...]}},
                                  {id,29,"F"}},
                             {id,29,"X"}},
                        {id,29,"f"}},
                   {app,{app,{app,{app,{app,{id,...},{...}},{id,29,...}},
                                  {id,29,"X"}},
                             {id,29,"g"}},
                        {id,29,"a"}}}},
         {def,{id,31,"listAlg"},
              {tele,[{id,31,"A"}],{id,31,"U"},[]},
              {id,31,"U"},
              {sigma,{tele,[{id,32,"X"}],{id,32,"U"},[]},
                     {sigma,{tele,[{id,33,"nil"}],{id,33,"X"},[]},
                            {sigma,{tele,[{id,34,...}],{pi,{...},...},[]},
                                   {id,35,"Unit"}}}}},
         {def,{id,37,"listMor"},
              {tele,[{id,37,"A"}],
                    {id,37,"U"},
                    {tele,[{id,37,"x2"},{id,37,"x1"}],
                          {app,{id,37,"listAlg"},{id,37,"A"}},
                          []}},
              {id,37,"U"},
              {sigma,{tele,[{id,38,"map"}],
                           {pi,{fst,{id,38,[...]}},{fst,{id,38,...}}},
                           []},
                     {sigma,{tele,[{id,39,"mapNil"}],
                                  {app,{app,{...},...},{fst,...}},
                                  []},
                            {sigma,{tele,[{id,...}],{app,...},[]},{id,41,[...]}}}}},
         {def,{id,43,"listObject"},
              {tele,[{id,43,"A"}],{id,43,"U"},[]},
              {id,43,"U"},
              {sigma,{tele,[{id,44,"point"}],
                           {pi,{tele,[{id,...}],{app,...},[]},{fst,{id,...}}},
                           []},
                     {sigma,{tele,[{id,45,[...]}],{app,{app,...},{...}},[]},
                            {id,48,"Unit"}}}}]}


В тред приглашаются специалисты по LALR парсерам.
_______________
[1]. https://github.com/groupoid/infinity/blob/master/src/cub_parser.yrl
sea

List Eliminator and Case Analysis in Pure Functions

-- List/@
  λ (A : *)
→ ∀ (List: *)
→ ∀ (Cons: A → List → List)
→ ∀ (Nil: List)
→ List

-- List/Cons
  λ (A: *)
→ λ (Head: A)
→ λ (Tail:
    ∀ (List: *)
  → ∀ (Cons: A -> List -> List)
  → ∀ (Nil: List)
  → List)
→ λ (List: *)
→ λ (Cons: A -> List -> List)
→ λ (Nil: List)
→ Cons Head (Tail List Cons Nil)

-- List/Nil
  λ (A: *)
→ λ (List: *)
→ λ (Cons: A -> List -> List)
→ λ (Nil: List)
→ Nil

-- List/cond
   \ (a : *)
-> \ (x: \/ (r : *) -> (a -> r -> r) -> r -> r)
-> x

-- List/match
   \ (A: *)
-> \ (value: #List/@ A)
-> \ (ret: *)
-> \ (cons_branch: ret)
-> \ (nil_branch: ret)
-> #List/cond A value ret
              (\(_:A)->\(_:ret)-> cons_branch)
              nil_branch

-- List/match.test
#List/match #Nat/@ (#List/Nil #Nat/@)
            #Nat/@ #Nat/Two #Nat/Five

-- List/match.test2
#List/match #Nat/@ (#List/Cons #Nat/@ #Nat/Zero (#List/Nil #Nat/@))
            #Nat/@ #Nat/Two #Nat/Five

> ch:unnat('List':'match.test2'()).
2
> ch:unnat('List':'match.test'()).
5

sea

Доказательство коммутативности в кубике

Если кратно, то индукция, индуктивные типы с приходом гомотопических пруверов кажутся уж не таким и сильными инструментами. Покажем на примере коммутативности сложения для двух и трех аргументов.

Доказательство коммутативности сложения курильщика

Theorem plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' Sn' ].
  - simpl. rewrite <- plus_n_0. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite <- Sn'. reflexivity.
Qed.

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n as [| n' Sn' ].
  - simpl. reflexivity.
  - simpl. rewrite <- Sn'. reflexivity.
Qed.


Доказательство коммутативностит сложения нормального человека

add_comm (a : nat) : (n : nat) -> Path nat (add a n) (add n a) = split
  zero  -> <i> add_zero a @ -i
  suc m -> <i> comp (<_> nat) (suc (add_comm a m @ i))
                    [ (i = 0) -> <j> suc (add a m)
                    , (i = 1) -> <j> add_suc m a @ -j ]

add_comm3 (a b c : nat) : Path nat (add a (add b c)) (add c (add b a)) =
 let r: Path nat (add a (add b c)) (add a (add c b)) = <i> add a (add_comm b c @ i)
  in <i> comp (<_> nat) ((add_comm a (add c b)) @ i)
              [ (i = 0) -> <j> r @ -j,
                (i = 1) -> (<z> assocAdd c b a @ -z) ]
sea

Pure Sigma

Кто-то на гиттер канале просил год назад, чтобы ему Сигму закодировали в чистых функциях. Я тогда не смог это сделать, но вот недавно формировал домашки и решил поставить такое задание в качестве домашки. Мне вроде говорили, что Альтенкирх где-то писал что это невозможно или по крайней мере это не обладает достаточно хорошими вычислительными характеристиками.

-- Sigma/@
   \ (A: *)
-> \ (P: A -> *)
-> \ (n: A)
-> \/ (Exists: *)
-> \/ (Intro: A -> P n -> Exists)
-> Exists

-- Sigma/Intro
   \ (A: *)
-> \ (P: A -> *)
-> \ (x: A)
-> \ (y: P x)
-> \ (Exists: *)
-> \ (Intro: A -> P x -> Exists)
-> Intro x y

-- Sigma/fst
   \ (A: *)
-> \ (B: A -> *)
-> \ (n: A)
-> \ (S: #Sigma/@ A B n)
-> S A ( \(x: A) -> \(_: B n) -> x )

-- Sigma/snd
   \ (A: *)
-> \ (B: A -> *)
-> \ (n: A)
-> \ (S: #Sigma/@ A B n)
-> S (B n) ( \(_: A) -> \(y: B n) -> y )

-- Sigma/test
-- P: nat -> U = (\(_:nat) -> list nat)
-- mk nat P n5 nil
#Sigma/Intro #Nat/@
             (\(n: #Nat/@) -> #List/@ #Nat/@)
             #Nat/Five
             (#List/replicate #Nat/@ #Nat/Five #Nat/Zero)

-- Sigma/test.fst
-- fst nat P zero test
#Sigma/fst #Nat/@
           (\(n: #Nat/@) -> #List/@ #Nat/@)
           #Nat/Zero
           #Sigma/test

-- Sigma/test.snd
-- snd nat P zero test
#Sigma/snd #Nat/@
           (\(n: #Nat/@) -> #List/@ #Nat/@)
           #Nat/Zero
           #Sigma/test


В тестах создание тапла (nat, list nat) = (5, [0,0,0,0,0]) и взятие у него первой и второй проекции:

1> om:fst(om:erase(om:norm(om:a("#Sigma/test.snd"))))
== om:fst(om:erase(om:norm(om:a("(#List/replicate #Nat/@ #Nat/Five #Nat/Zero)")))).
true
2> om:fst(om:erase(om:norm(om:a("#Sigma/test.fst"))))
== om:fst(om:erase(om:norm(om:a("#Nat/Five")))).
true
3> om:type(om:type(om:a("#Sigma/snd"))).
{star,1}
4> om:type(om:type(om:a("#Sigma/fst"))).
{star,1}


Трюк заключается в протаскивании первого элемента в базу, все равно конструктор один и он же принимает его. Т.е. классическое индуктивное определение

data Sigma (A: Type) (P: A -> Type): Type
   = (intro: (x:A) (y:P x) -> Sigma A P)


сменяется на следующее:

data Sigma (A: Type) (P: A -> Type) (x:A): Type
   = (intro: (y:P x) -> Sigma A P)


Наверн проблемы начнутся как с pred, когда придется закодировать N-тапл из сигм и переносить все кроме последнего в базу, но тоже вроде все законно. Единственное к чему тут можно предъявить претензии — это дополнительный параметр пустышка #Nat/Zero который передается в примерах в качестве (x:A) при вызове элиминаторов, он нужен для совместимости типов, но как видно из примера, экстрактятся из сконструированного тапла #Sigma/Intro настоящие значения (fst test = 5 и snd test = [0,0,0,0,0]). Другими словами это означает что первый элемент типовой пары должен быть как минимум стягиваемым пространством, что в принципе в духе Сигмы и квантора существования. Что думают по этому поводу типовые теоретики?

P.S. Модель в cubicaltt, для тех, кто не доверяет Ом.

module puresigma where
import nat
import list

P: nat -> U = (\(_:nat) -> list nat)
sig (A:U)(P:A->U)(x:A): U = (e:U)->(i:A->P x->e)->e
mk  (A:U)(P:A->U)(x:A)(y:P x)(e:U)(i:A->P x->e):e=i x y
fst (A:U)(P:A->U)(x:A)(s:sig A P x):A=s A(\(z:A)(y:P x)->z)
snd (A:U)(P:A->U)(x:A)(s:sig A P x):P x=s(P x)(\(z:A)(y:P x)->y)

test: sig nat P n5 = mk nat P n5 nil
test_pr1: nat = fst nat P zero test
test_pr2: list nat = snd nat P zero test

> test_pr2
EVAL: nil
> test_pr1
EVAL: suc (suc (suc (suc (suc zero))))

Тут мне подсказывают, что писал Thorsten Altenkirch:

Ok, when we think of homogenous tuples AxA then this can also be understood as a function 2 -> A. This also works for heterogenous tuples like AxB using dependent functions Pi x:2.if x then A else B. However the next logical step is Sigma x:A.B x, which have no good representations as functions (unless we accept very dependent functions which in my mind goes against the spirit of type theory). For this reason it seems to me that the generalisation from -> to Pi and from x to Sigma is the primary one, and the fact that tuples can be represented as functions is secondary.

Позволю себе не согласиться с Торстеном,Альтенкирхом: на мой взгляд, именно Черч кодировка и показывает скрытую категорную стркутуру теории типов обнажая ее самантику, она ни как не может идти в разрез духа тетории типов, которым как раз и является теория категорий.

Существует и другая более общая связь между Пи и Сигмой. Сигму можно интерпретировать как тотальное пространство расслоения B -> A над A. Где расслоение — это терм
section (A B : U) (p : A -> B) (s : B -> A) : U = (y : B) -> Path B (p (s y)) y
А элементы Пи или лямбды — это сечения тривиального расслоения A -> A x B. Симметричной функцией является ретракт:
retract (A B : U) (f : A -> B) (g : B -> A) : U = (a : A) -> Path A (g (f a)) a
Не могу к сожалению (пока) понять, как устроены йоги Гротендика, но это устройство связи Пи и Сигмы помоему две из них и есть.

Надо переписать на кубикал, кто возьмется?
Prerequisites:

_⋔_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
_⋔_ A B = A → B

_⊗_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
_⊗_ A B = A × B

∫↓ : ∀ {a b} {X : Set a} → (X → X → Set b) → Set (a ⊔ b)
∫↓ {X = X} P = ∀ {x} → P x x

∫↑ : ∀ {a b} {X : Set a} → (X → X → Set b) → Set (a ⊔ b)
∫↑ {X = X} P = ∐ [ x ∶ X ] P x x
Левое и правое расширения Кана:
Ran : ∀ {x c v u p} {𝔵 : Set x} {𝔠 : Set c} {𝔳 : Set v}
  → (𝒸 : 𝔠 → 𝔠 → Set u)
  → (_⋔_ : Set u → 𝔳 → Set p)
  → (G : 𝔵 → 𝔠)
  → (H : 𝔵 → 𝔳)
  → (𝔠 → Set (p ⊔ x)) = 𝒸 _⋔_ G H A = ∫↓ λ x y → 𝒸 A (G x) ⋔ H y

Lan : ∀ {x c v u p} {𝔵 : Set x} {𝔠 : Set c} {𝔳 : Set v}
  → (𝒸 : 𝔠 → 𝔠 → Set u)
  → (_⊗_ : 𝔳 → Set u → Set p)
  → (G : 𝔵 → 𝔠)
  → (H : 𝔵 → 𝔳)
  → (𝔠 → Set (p ⊔ x)) = 𝒸 _⊗_ G H A = ∫↑ λ x y → H x ⊗ 𝒸 (G y) A


По сигнатуре видно, что Пи и Сигма — элементы одного пространства.
Sigma: ∀ {x y} {X : Set x} {Y : Set y} → (X → Y) → 𝒫 x X → 𝒫 (x ⊔ y) Y = Ran _≡_ _⋔_ f

Pi:    ∀ {x y} {X : Set x} {Y : Set y} → (X → Y) → 𝒫 x X → 𝒫 (x ⊔ y) Y = Lan _≡_ _⊗_ f






___________
[1]. Расширения Кана Бартоша https://henrychern.files.wordpress.com/2017/10/27.pdf
sea

Swift Model Generator from Erlang Types

-module(roster_swift).
-export([parse_transform/2]).
-compile(export_all).
-define(SRC, "apps/roster/priv/macbert/").

parse_transform(Forms, _Options) -> switch(directives(Forms)), Forms.
directives(Forms) -> lists:flatten([ form(F) || F <- Forms ]).

switch(List) ->
    file:write_file(?SRC++"Source/Decoder.swift",
    iolist_to_binary(lists:concat([
       "func parseObject(name: String, body:[Model], tuple: BertTuple) -> AnyObject?\n"
       "{\n    switch name {\n",
       [case_rec(X) || X <- List],
       "    default: return nil\n"
       "    }\n}"
    ]))).

act(List,union,Args,Field,I) -> act(List,union,Args,Field,I,simple);
act(List,Name,Args,Field,I) -> act(List,Name,Args,Field,I,keyword).

act(List,Name,Args,Field,I,Fun) ->
%    io:format("Keyword: ~p~n",[{Name,Args}]),
    lists:concat([tab(1),List,".",Field,
    " = body[",I,"].parse(bert: tuple.elements[",I+1,"]) as? ",
    ?MODULE:Fun(Name,Args,{Field,Args}),"\n"]).

case_rec({Atom,T}) ->
    List = atom_to_list(Atom),
    Lower = string:to_lower(List),
    Var = "a" ++ List,
    lists:concat([ "    case \"", List, "\":\n"
    "        if body.count != ", integer_to_list(length(T)), " { return nil }\n",
    io_lib:format("        let ~s = ~s()\n",[Var,List]),
    [ tab(2) ++ act(Var,Type,Args,Field,I-1) ||
         {{_,{_,_,{atom,_,Field},Value},{type,_,Type,Args}},I} <- lists:zip(T,lists:seq(1,length(T))) ],
    "        return " ++ Var ++ "\n" ]).

form({attribute,_,record,{List,T}})  ->
   [X|Rest]=atom_to_list(List),
   case X >= $A andalso X =< $Z andalso List /= 'Client'
                                orelse List == io
                                orelse List == error
                                orelse List == ok2
                                orelse List == error2
                                orelse List == ok of true
      -> spec(List,T),
         class(List,T),
         {List,T};
    _ -> [] end;
form(Form) ->  [].

class(List,T) ->
   file:write_file(?SRC++"/Model/"++atom_to_list(List)++".swift",
   iolist_to_binary(case lists:concat([ io_lib:format("\n    var ~s",
                [ infer(Name,Args,atom_to_list(Field))])
               || {_,{_,_,{atom,_,Field},Value},{type,_,Name,Args}} <- T ]) of
               [] -> [];
               Fields -> lists:concat(["\nclass ",List," {", Fields, "\n}"]) end)).

spec(List,T) ->
    file:write_file(?SRC++"/Spec/"++atom_to_list(List)++"_Spec.swift",
    iolist_to_binary("func get_"++atom_to_list(List) ++ "() -> Model {\n  return " ++ premodel(List,T) ++ "}\n")).

premodel(List,T) ->
    D = 1,
    Model = tab(D) ++ string:join([ model({type,X,Type,Args},D+1) || {_,_,{type,X,Type,Args}} <- T ],",\n"++tab(D)),
    erlang:put(List,Model),
    io_lib:format("Model(value:Tuple(name:\"~s\",body:[\n~s]))",[atom_to_list(List), Model]).

tab(N) -> lists:duplicate(4*N,$ ).

model({type,_,nil,Args},D)     -> "Model(value:List(constant:\"\"))";
model({type,_,binary,Args},D)  -> "Model(value:Binary())";
model({type,_,atom,Args},D)    -> "Model(value:Atom())";
model({type,_,list,[{type,_,atom,[]}]},D)    -> "Model(value:List(constant:nil, model:Model(value:Atom())))";
model({type,_,list,[{type,_,binary,[]}]},D)  -> "Model(value:List(constant:nil, model:Model(value:Binary())))";
model({type,_,list,[{type,_,integer,[]}]},D) -> "Model(value:List(constant:nil, model:Model(value:Number())))";
model({_,_,list,[{_,_,record,[{_,_,Name}]}]},D) -> lists:concat(["Model(value:List(constant:nil,model:get_",Name,"()))"]);
model({type,_,list,[Union]},D)    -> "Model(value:List(constant:nil, model:"++ model(Union,D) ++ "))";
model({type,_,record,[{atom,_,Name}]},D)        -> lists:concat(["get_",Name,"()"]);
model({type,_,list,Args},D)    -> "Model(value:List(constant:nil))";
model({type,_,boolean,Args},D) -> "Model(value:Boolean())";
model({atom,_,Name},D)         -> lists:concat(["Model(value:Atom(constant:\"",Name,"\"))"]);
model({type,_,term,Args},D)    -> "Model(value:nil)";
model({type,_,integer,Args},D) -> "Model(value:Number())";
model({type,_,tuple,any},D)    -> "Model(value:Tuple())";

model({type,_,union,Args},D)   -> io_lib:format("Model(value:Chain(types:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,tuple,Args},D)   -> io_lib:format("Model(value:Tuple(name:\"\",body:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,Name,Args},D)    -> io_lib:format("Model(~p): Args: ~p~n",[Name,Args]).

keyword(X,Y,_Context) -> keyword(X,Y).
keyword(record, [{atom,_,Name}]) -> lists:concat([Name]);
keyword(list, [{type,_,record,[{atom,_,Name}]}]) -> lists:concat(["[",Name,"]"]);
keyword(list, [{type,_,atom,[]}]) -> lists:concat(["[","String","]"]);
keyword(list, Args)   -> "[AnyObject]";
keyword(tuple,any)    -> "[AnyObject]";
keyword(term,Args)    -> "AnyObject";
keyword(integer,Args) -> "Int";
keyword(boolean,Args) -> "Bool";
keyword(atom,Args)    -> "StringAtom";
keyword(binary,Args)  -> "String";
keyword(union,Args)   -> "AnyObject";
keyword(nil,Args)     -> "AnyObject".

infer(union,Args,Field) -> Field ++ ": " ++ simple(union,Args,{Field,Args}) ++ "?";
infer(Name,Args,Field)  -> Field ++ ": " ++ keyword(Name,Args,{Field,Args}) ++ "?".

simple(A,[{type,_,nil,_},{type,_,Name,Args}],Context) -> keyword(Name,Args,Context);
simple(A,[{type,_,Name,Args},{type,_,nil,_}],Context) -> keyword(Name,Args,Context);
simple(_,_,_) -> "AnyObject".