Size: a a a

2020 December 04

DB

Danil Berestov in haskell_blah
Nick Ivanych
Ой вей. Всего-то фактор-группы...
Кто его знает, что будет дальше
источник

AG

Alex Gryzlov in haskell_blah
Danil Berestov
Это как
ну вот очевидное следствие: https://github.com/gallais/potpourri/blob/master/agda/cubical/list0.agda#L14
источник

AG

Alex Gryzlov in haskell_blah
все списки подобного типа стягиваемы в точку
источник

к

кана in haskell_blah
Danil Berestov
То есть он возвращает не int?
он возвращает пруф равенства

а равенство элементов типа X это функция от [0..1] -> X
то есть для a, b : X
p : a = b
это функция [0..1] -> X где
p 0 = a
p 1 = b
и p при этом является неприрывной

вот этот конструктор задает аксиому что между neg 0 и pos 0 существует неприрывный путь
источник

DB

Danil Berestov in haskell_blah
Хорошо, как тогда расшифровать
forall x e -> x :: e = e?
источник

к

кана in haskell_blah
Danil Berestov
Хорошо, как тогда расшифровать
forall x e -> x :: e = e?
для любого x и e, список x :: e равен e)
источник

AG

Alex Gryzlov in haskell_blah
это доп ограничение на тип
источник

AG

Alex Gryzlov in haskell_blah
т.е. когда ты будешь что-то с термом этого типа делать, тебя язык заставит соблюдать это условие
источник

DB

Danil Berestov in haskell_blah
Alex Gryzlov
т.е. когда ты будешь что-то с термом этого типа делать, тебя язык заставит соблюдать это условие
Понятно, шо ограничение. Пока не доходит его суть. Ща дайте переварить..
источник

AG

Alex Gryzlov in haskell_blah
да тут нет особой сути, это гийом от балды написал побаловаться
источник

AG

Alex Gryzlov in haskell_blah
ща найду поосмысленнее пример
источник

AG

Alex Gryzlov in haskell_blah
источник

к

кана in haskell_blah
с int мне кажется пример поосмысленнее
источник

к

кана in haskell_blah
ну в том смысле что его проще осмыслить
источник

к

кана in haskell_blah
)
источник

AG

Alex Gryzlov in haskell_blah
вот например OddList
источник

AG

Alex Gryzlov in haskell_blah
список где неважен порядок элементов
источник

DB

Danil Berestov in haskell_blah
Ага, вот тут понятно что такое ослабленные равенство
источник

DB

Danil Berestov in haskell_blah
И его я даже понял
источник

DB

Danil Berestov in haskell_blah
А вот про равенство списка и его хвоста это что-то шизоидное, страшное
источник