ЕО
ну вы говорите что должен быть экзистс, я говорю что в оригинальной формулировке он там есть, просто неявный, потому что все переменные для которых не объявили явно forall полагаются exists
Это где такое?
Size: a a a
2019 December 23
Oℕ
переменные, которые явно не объявили forall полагаются forall
ЕО
Квантор по умолчанию — квантор всеобщности
AZ
Квантор по умолчанию — квантор всеобщности
если не включен ExplicitForAll, насколько я понял
Oℕ
вот так это выражается в хошкеле
https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Coyoneda.html
собственно изоморфизм - это пара функций liftCoyoneda и lowerCoyoneda
https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Coyoneda.html
собственно изоморфизм - это пара функций liftCoyoneda и lowerCoyoneda
Oℕ
если не включен ExplicitForAll, насколько я понял
из названия следует, что forall подставляется, а не exists
AZ
переменные, которые явно не объявили forall полагаются forall
если там два forall то почему на шарпике такой код не компилируется?
AZ
из названия следует, что forall подставляется, а не exists
из названия следует что forall надо явно включать. Можно предположить, что это меняет дефолт forall (который теперь надо явно писать) на exists
Oℕ
если там два forall то почему на шарпике такой код не компилируется?
вот это вообще вопрос, непонятно как относится к теме обсуждения, и как я должен на него ответить
Oℕ
из названия следует что forall надо явно включать. Можно предположить, что это меняет дефолт forall (который теперь надо явно писать) на exists
нет, в системе выражений haskell нет exists
Oℕ
ни явно, ни неявно
AZ
вот это вообще вопрос, непонятно как относится к теме обсуждения, и как я должен на него ответить
на шарпе генерики это forall. На них не компиляется такой же код. Следоавательно, это не два forall.
Oℕ
вот тут я как раз выполнил подобное преобразрвание https://t.me/ru_catheory/9312
Oℕ
на шарпе генерики это forall. На них не компиляется такой же код. Следоавательно, это не два forall.
у вас очень сложная доказательная база
ЕО
на шарпе генерики это forall. На них не компиляется такой же код. Следоавательно, это не два forall.
Что-то я сомневаюсь, что на C# полноценный System F
ЕО
Скорее всего там хиндли-милнер какой-нибудь, ну или System F2
Oℕ
не думаю, что можно делать вывод о том, что значат выражения на haskell на основании того, какой код компилится в F#
в любом случае, это вне темы этого чата
в любом случае, это вне темы этого чата
AZ
Что-то я сомневаюсь, что на C# полноценный System F
но для того чтобы запилить форолл сильной системы типов вроде не надо
Oℕ
но для того чтобы запилить форолл сильной системы типов вроде не надо
Алекс, пожалуйста, давайте это в хаскель чат