Size: a a a

2020 December 04

DB

Danil Berestov in haskell_blah
кана
ну просто вот так
Да у них же даже длина разная
источник

DB

Danil Berestov in haskell_blah
Такова не бывает
источник

к

кана in haskell_blah
ну смотри
источник

AG

Alex Gryzlov in haskell_blah
тут равенство ослабленное
источник

DB

Danil Berestov in haskell_blah
В смысле! Кем!
источник

к

кана in haskell_blah
data nat = zero | succ nat
data int where
 pos : nat -> int
 neg : nat -> int
 neg_zero_eq_zero : pos zero = neg zero

получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные

и доказательство это как раз наш конструктор neg_zero_eq_zero
источник

к

кана in haskell_blah
конструкторы это же аксиомы
источник

AG

Alex Gryzlov in haskell_blah
Danil Berestov
В смысле! Кем!
создателями теории :)
источник

DB

Danil Berestov in haskell_blah
кана
data nat = zero | succ nat
data int where
 pos : nat -> int
 neg : nat -> int
 neg_zero_eq_zero : pos zero = neg zero

получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные

и доказательство это как раз наш конструктор neg_zero_eq_zero
Вместо равно стрелка?
источник

к

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

AG

Alex Gryzlov in haskell_blah
не, в том то и фишка
источник

DB

Danil Berestov in haskell_blah
Капец
источник

AG

Alex Gryzlov in haskell_blah
это так называемый высший индуктивный тип
источник

AG

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

DB

Danil Berestov in haskell_blah
Неясно. А что мы построим-то этим конструктором
источник

к

кана in haskell_blah
если посмотреть на теорию групп и на фактор-группы, то может появится некоторая интуиция
источник

к

кана in haskell_blah
Danil Berestov
Неясно. А что мы построим-то этим конструктором
пруф равенства
источник

DB

Danil Berestov in haskell_blah
кана
если посмотреть на теорию групп и на фактор-группы, то может появится некоторая интуиция
Боюсь стать шизоидом, как Михайлов
источник

DB

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

NI

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