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

ззвучит как что-то что можно сделать но не очевидно как именно

16:05пожаловаться #1

Если не хочется бодаться с тайп-чекером, всегда можно после рантайм-валидации сделать ансейф-коерс к типу с нужными размерностями

16:06пожаловаться #2

Хотя скорее даже и это не нужно

16:07пожаловаться #3

а хочется чтобы эта самая “нужная” размерность определялась входными данными (с некоторыми ограничениями)

16:08пожаловаться #4

Ilya Kos

а хочется чтобы эта самая “нужная” размерность определялась входными данными (с некоторыми ограничениями)

Так она и будет. Вопрос-то только в том, как данные поднять с терм-левела на тайп-левел

16:08пожаловаться #5

A64m AL256m qn<co... in Haskell

ну для натов-то такая функциональность в base есть

16:10пожаловаться #6

поднятие в тайп-левел?

16:11пожаловаться #7

где

16:11пожаловаться #8

https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-TypeNats.html#v:someNatVal
Видимо здесь

16:12пожаловаться #9

A64m AL256m qn<co... in Haskell

GHC.TypeNats/GHC.TypeLits

16:12пожаловаться #10

ну вот принимаю я матрицу, на выходе Matrix n m

16:13пожаловаться #11

принимаю другую матрицу, там выход Matrix m’ u

16:13пожаловаться #12

но в данных m и m’ одинаковые, но компилятор об этом не знает

16:14пожаловаться #13

как ему сообщить это

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

Roman in Haskell

кана

как ему сообщить это

функция, которая принимает Proxy m, Proxy m' и возвращает Maybe (m :~: m')

16:14пожаловаться #15

Roman in Haskell

с гхцшными натами придется использовать unsafeCoerce внутри

https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-TypeNats.html#v:sameNat

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

A64m AL256m qn<co... in Haskell

кана

как ему сообщить это

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

Alexander Vershilov in Haskell

А у нас есть библиотека для операций всяких на type level lists?

17:53пожаловаться #18

Alexander Vershilov in Haskell

чтобы не тащть синглтоны

17:53пожаловаться #19

Alexander Vershilov in Haskell

И чтобы самому в тысячный раз не писать заново