Телеграмм чат группы haskellru страница 15033

почему? это наблюдаемо для программиста же

20:57пожаловаться #1

да не очень-то наблюдаемое, для программиста наблюдаемо только то что нельзя напрямую перекидывать значения между уровнями, а что тип промоутится это ни разу не наблюдаемое

20:58пожаловаться #2

но ладно, это отдельный спор, в моем утверждении можно просто разбить строку про True на две отдельных строки

как и про Bool

20:58пожаловаться #3

Kirill Valyavin

Haskell> :t Int#

<interactive>:1:1: error: Data constructor not in scope: Int#
Haskell> :k Int#
Int# :: TYPE 'IntRep

А это чё тогда

тяжелое дотайпинтайп наследие, еще в названиях ленгвидж прагм всяких и т.д.

20:59пожаловаться #4

так, я смотрю комитетчики наголосовали таки МПТЦ но без фандепов и семейств/гадт/включения волночки

21:29пожаловаться #5

Maxim Koltsov in Haskell

волночки?

21:34пожаловаться #6

коершины мб, ~

21:34пожаловаться #7

ну я-то уже без фандепов не вижу смысла, но так-то есть желающие вместо них волночки писать

21:35пожаловаться #8

второй подход не особо популярный, но главное что без того или другого уж точно толку от МПТЦ никакого

21:36пожаловаться #9

Maxim Koltsov in Haskell

а что, есть экстеншен который включает ~?

21:37пожаловаться #10

Maxim Koltsov in Haskell

мне казалось эта штука тянется TF или GADTs

21:37пожаловаться #11

есть два, но комитетчики могут еще как-то включить, кто им запретит?

21:37пожаловаться #12

я понимаю почему тф не хотят добавлять

21:38пожаловаться #13

но ГАДТЫ почему нет?

21:38пожаловаться #14

так это одно и то же

21:38пожаловаться #15

кому они мешают, это же давно основа

21:38пожаловаться #16

нет, не одно и то же, гадты это только закрытые дата-семейства, а тф в том числе и открытые, и не дата вовсе

21:39пожаловаться #17

ну, вернее это два выглядывающих рога одной фичи

21:39пожаловаться #18

если бы им еще и синтаксис одинаковый сделали, типа

data family V (n :: N) a where
V Z _ = Nil
V (S n) a = Cons a (V n a)
V n a = Reverse (V n a) | Drop (V (S n) a)

у аренда для гадтов похожий синтаксис как у хаскеля с закрытыми семействами

21:40пожаловаться #19

и вывод типов ломает что одна что другая