MK
allow me to introduce myself
Слушаю
Size: a a a
2020 November 20
DB
нет, вынести терм на тайплевел в хаскеле нельзя, но можно заранее иметь термы, которые однозначно выводимы из типа, сигнлтон типы иметь то есть
Ну вот я про это и спрашиваю, можно ли как-то Int лифтануть в пару (Знак, Абсолютное_Значение)?
AV
о, я похожим образом значения от 0 до 1 мутил, кажется
а это нельзя просто через Integer, где число как 1/Integer
AV
DB
о, я похожим образом значения от 0 до 1 мутил, кажется
Как это связано?)
DB
а что за задачу вы решаете
Я хотел просто лифтануть числа в тип)
A
а это нельзя просто через Integer, где число как 1/Integer
можно было, но лень, мне буквально несколько значений надо было изобразить, да, то совершенно другая задача
AV
Врятли это вопрос не не 0
DB
это не похоже на задачу по симлификции
это похоже на задачу по усложнению
a
Слушаю
хотя я не сильно знаю идрис, но агда хотя бы юниполиморфная
MK
хотя я не сильно знаю идрис, но агда хотя бы юниполиморфная
Что это значит?
A
Как это связано?)
никак, просто к ситуации пришлось, другая задача
DB
Что это значит?
вот и тебя переиграли. не тошо индексированные монады
к
Я хотел просто лифтануть числа в тип)
someNatVal вернет SomeNat, который потом распаковывается и получается некий тип