к
Size: a a a
2020 November 21
IB
То есть я не могу из [a] никак вытащить тайплевел репрезентацию?
IB
(не уверен что задаю очень правильные вопросы, но пытаюсь))
JS
То есть я не могу из [a] никак вытащить тайплевел репрезентацию?
можно, но у вас в коде написано обратное
JS
@[1, 2, 3] — это уже тайплевелIB
Ну вот да - foo работает как я задумал
KV
То есть я не могу из [a] никак вытащить тайплевел репрезентацию?
Может такое хотите?
data Vec a n where
VNil :: Vec a 0
VCons :: a -> Vec a n -> Vec a (n + 1)
IB
Я пытаюсь понять теперь как добраться из term-level
JS
вы хотите принимать список на уровне типов, это делает
forallJS
foo2 :: forall xs. ...
JS
Я пытаюсь понять теперь как добраться из term-level
а, зависимые типы хотите! вам в singletons
IB
вы хотите принимать список на уровне типов, это делает
forallХотелось бы из полученного на term-level [a] - фактического значения получить его тайплевел репрезентацию и посчитать пустая она или нет
JS
Хотелось бы из полученного на term-level [a] - фактического значения получить его тайплевел репрезентацию и посчитать пустая она или нет
вы зависимые типы хотите. вам в singletons
JS
Хотелось бы из полученного на term-level [a] - фактического значения получить его тайплевел репрезентацию и посчитать пустая она или нет
проверить пустоту легче на term level
IB
вы зависимые типы хотите. вам в singletons
Понял, направленеи получил хоть и не понимаю пока как это связано) Буду копать
IB
проверить пустоту легче на term level
Это исключительно в качестве упражнения. Разбирался с OpenProducts и не совсем понял что их так сильно отличает от обычного списка
JS
Понял, направленеи получил хоть и не понимаю пока как это связано) Буду копать
непосредственно связано. вычислить тип по значению — это и есть определение "зависимого от значения типа"
IB
Ага, так более понятно.
IB
Я хотел отпочковаться от примерно такого - тут я могу с помощью инфы которую несу в тайплевеле явно сказать что-то про список
AP
Мне тоже кажется, что человек хочет синглтонов