These are chat archives for groupoid/exe

13th
Feb 2016
Zeit Raffer
@zraffer
Feb 13 2016 09:06
This message was deleted
Zeit Raffer
@zraffer
Feb 13 2016 09:11
если везде в основе та же лямбда, то и результат похожий
Zeit Raffer
@zraffer
Feb 13 2016 16:13

пример, как Lean выводит уровень универсума для определения "категория имеет всякие пределы":

definition HaveAllLim (D : CatType) : Type := Π (C : CatType), Lim C D

=>

definition HaveAllLim : CatType.{l_1 l_2} →
Type.{max
        (imax (max 1 (imax l_3 l_1) (imax l_4 l_2) l_3) l_1)
        (imax (max 1 (imax l_3 l_2)) l_2)
        (imax l_3 l_4)
        (imax l_3 l_1)
        (imax l_3 l_2)
        (imax l_4 l_2)
        (imax l_1 l_2)
        (l_3+1)
        (l_4+1)
        l_3} :=
λ (D : CatType.{l_1 l_2}), Π (C : CatType.{l_3 l_4}), Lim.{l_3 l_4 l_1 l_2} C D
Namdak Tonpa
@5HT
Feb 13 2016 17:13
структура вселенных :-)
Zeit Raffer
@zraffer
Feb 13 2016 17:30

кстати, ошибка Леан

Initial.lean:53:14: error: invalid local context when tried to assign
  c
containing 'c', to placeholder '?M_1', in the local context
  C lim

это про мою ошибку типов или про его внутренний баг?
файлы этого коммита: https://github.com/groupoid/exe/blob/e22e86ce893a4093af8d1a33d314963c51ae8519/prelude/lean/Initial.lean

Namdak Tonpa
@5HT
Feb 13 2016 17:31
эта терминал конструкция на шести вселенных типа описана?
Zeit Raffer
@zraffer
Feb 13 2016 17:32
оно само выводит сколько ему надо универсумов
Namdak Tonpa
@5HT
Feb 13 2016 17:32
ну там у тебя шесть переменных
Zeit Raffer
@zraffer
Feb 13 2016 17:32
а - это на всякий случай
для произведения двух функторов надо три категории, у каждой есть универсум объектов и морфизмов - всего шесть
в тьюториале это сообщение названо "странным":
A good rule of thumb is that if you are using some or epsilon, and you are presented with a strange error message, trying changing have to assert.
а я вообще тактиками здесь не пользуюсь
Namdak Tonpa
@5HT
Feb 13 2016 18:35
а у меня кстати с дефинишинами тоже такое было
типа когда ты делаешь дефинишин ты определяешь свой локальный контекст, который может отличатся от того, где ты его используешь, не?
Namdak Tonpa
@5HT
Feb 13 2016 18:49
Флориас ван Дорн блюдет чтобы все кто пишет на Lean пробелы расставляли правильно :-) гг
Zeit Raffer
@zraffer
Feb 13 2016 19:10
вобщем я сделал вручную подстановку нескольких определений и оно работает теперь, но все равно неприятно
Namdak Tonpa
@5HT
Feb 13 2016 19:11
я тоже не понимаю зачем они напридумывали синтаксиса который не работает
лучше иметь одно но работающее, чем много но наполовину )
вот мне нравится как у нас все в рекордах
понятно как переносить на другие языки сразу, тривиальное понимание
Zeit Raffer
@zraffer
Feb 13 2016 19:12
у них есть какие-то ограничения на этот элаборатор
Namdak Tonpa
@5HT
Feb 13 2016 19:12
а там же секции неймспейсы и дефинишины
Zeit Raffer
@zraffer
Feb 13 2016 19:13
у меня часто при попытке определить секцию вылазит этот "контекст еррор", так что я на них забил
Namdak Tonpa
@5HT
Feb 13 2016 19:13
я думал элаборатор — это просто алгоритм тайпчекинга ихнего так называется
Zeit Raffer
@zraffer
Feb 13 2016 19:13
не, это его часть - которая занимается частичной нормализацией термов
Namdak Tonpa
@5HT
Feb 13 2016 19:14
ну это в тайпчекере тоже есть
в морте
Zeit Raffer
@zraffer
Feb 13 2016 19:14
ну вот часть тайпчекера
Namdak Tonpa
@5HT
Feb 13 2016 19:14
хотя там не частичная
а полная
ну типа без фикспойнтов просто
Zeit Raffer
@zraffer
Feb 13 2016 19:14
морте агрессивный на счет нормализации )
Namdak Tonpa
@5HT
Feb 13 2016 19:14
хотя я и в Lean фикспойнтов в ядре не видел
разве что Meta или Local, вот Local — это твой локальный контекст который сбоит помоему
а эти все notation и [class] это Macro стопудняк
Zeit Raffer
@zraffer
Feb 13 2016 19:16
а ты возьми какой-нибудь терм из моего кода побольше и вставь его в eval ... - фиг оно что посчитает, вылетит с ограничением по памяти
Namdak Tonpa
@5HT
Feb 13 2016 19:16
а я понял
Local — это let
или не?
Zeit Raffer
@zraffer
Feb 13 2016 19:16
может и ЛЕТ, они в тьюториале говорят "загадочное сообщение", не обяъсняют
Namdak Tonpa
@5HT
Feb 13 2016 19:17
закидаем их вопросами на гитхабе
пусть видят что люди работают )
Zeit Raffer
@zraffer
Feb 13 2016 19:17
они же уже третью версию делают? вот ее надо тестировать. но у меня на тот момент не собралась с ошибкой в С++
Namdak Tonpa
@5HT
Feb 13 2016 19:17
та оно еще в альфе я думаю
так шо "приплыли"?
Zeit Raffer
@zraffer
Feb 13 2016 19:18
это ж майкрософт финансирует?
Namdak Tonpa
@5HT
Feb 13 2016 19:18
:-) хотели хакнуть кодировку пространства, но не получилось )
ну да, он же в майкрософт работает
Namdak Tonpa
@5HT
Feb 13 2016 19:58
у меня в Adjunction вот такое:
type mismatch at application
  Cat.MulFF.{o2 h1 o1 o2} R
term
  R
has type
  C⟶D
but is expected to have type
  ?M_1⟶?M_2