KV
конструкторы типов
Исключая термы, населяющие все остальные кайнды
Size: a a a
2020 December 15
AA
Исключая термы, населяющие все остальные кайнды
зачем их изключать
KV
У них разница есть существенная, в том, что 'True ничё не может населять, а Maybe Bool может
Довольно разные классы вещей
Довольно разные классы вещей
AA
потому что 'True не конструирует тип!
конструирует не населенный прост. но да, я в курсе, что эйзенберг считает, что типами можно называть только типы типа TYPE r
KV
Заведомо ненаселяемые типы это смешно
AA
остальные что тогда?
AA
почему?
KV
остальные что тогда?
Kind children. Одно из смешных предложений назвать одним словом — "angels"
AA
почему типы не могут быть значениями на тайплевеле, тем более в хачкеле где с лохматых годов завкайнды
AA
Kind children. Одно из смешных предложений назвать одним словом — "angels"
но в хаскеле больше нету кайндов, только типы
KV
почему типы не могут быть значениями на тайплевеле, тем более в хачкеле где с лохматых годов завкайнды
Ну такое... хочется сказать, что типы — это что-то свойственное термам, а не просто так, но пустой тип — тип
к
почему типы не могут быть значениями на тайплевеле, тем более в хачкеле где с лохматых годов завкайнды
так типы могут быть значениями на тайплевеле, но не все значения на тайплевеле - типы
KV
но в хаскеле больше нету кайндов, только типы
Haskell> :t Int#
<interactive>:1:1: error: Data constructor not in scope: Int#
Haskell> :k Int#
Int# :: TYPE 'IntRep
А это чё тогда
AA
Bool - тип, и значение типа Type
True - значение типа Bool (на всех уровнях), но не тип ни на одном из уровней
True - значение типа Bool (на всех уровнях), но не тип ни на одном из уровней
но бул и промотнутый бул это разные типы