DS
Такое может сделать через зависимые типы
arraySize, но хочу попробовать на литералах сделатьSize: a a a
2020 April 14
VK
Переслано от Юрий Бадальянц
На самом деле мне в рантайме просто нужно такое число, которое описывает длину массива. У меня есть тайплкасс, который сериализует данные в массив фиксированной длины. Я могу добавить просто ещё одно полюшко в трейт, реализующий тайпкласс, типа
AH
Я не знаю, что там происходит у них в чате, но например, ты хочешь создать такой массив по переданному пользователю числу
Сделать массив по переданному числу... Звучит как задача для зависимых типов!
DS
Сделать массив по переданному числу... Звучит как задача для зависимых типов!
Создать массив константной длины n по переданному числу n
AH
Создать массив константной длины n по переданному числу n
Array.zeroInit N
AH
Массив очень константной длины
AH
Длину можно достать в рантайме так
arr.Length
arr.Length
DS
Array.zeroInit N
Нет, ты потом сможешь сделать: Array.get (N+1) myArray и компилятор тебе не помешает
DS
А вот этого и хочется избежать
AH
Нет, ты потом сможешь сделать: Array.get (N+1) myArray и компилятор тебе не помешает
Он мне и так не помешает. Мы ж в РАНТАЙМЕ
DS
Он мне и так не помешает. Мы ж в РАНТАЙМЕ
Помешает
AH
Помешает
Нет. Там нет компилятора
DS
Нет. Там нет компилятора
Тебе надо будет в коде предоставить доказательство того, что данное пришедшее N удовлетворяет нужным условиям.
И код скомпилиться, только если нужные проверки есть
И код скомпилиться, только если нужные проверки есть
AH
Тебе надо будет в коде предоставить доказательство того, что данное пришедшее N удовлетворяет нужным условиям.
И код скомпилиться, только если нужные проверки есть
И код скомпилиться, только если нужные проверки есть
Тогда это не рантайм, ты же понимаешь
AH
Речь шла про рантайм
DS
Тогда это не рантайм, ты же понимаешь
Ты не понимаешь до конца, о чем речь, сейчас скину пример
AH
Ты не понимаешь до конца, о чем речь, сейчас скину пример
А, ты про евиденсы тайп классов
DS
А, ты про евиденсы тайп классов
Ага
DB
ммм а зачем им тогда типизация если есть рантайм?)