KR
Size: a a a
2021 May 26
TK
Или branded types, но что-то оба варианта плоховато гуглятся
AN
так а где принципиальное отличие у нас?
TK
С ними доказательство не построишь
AN
доказательство чего?
KR
То есть это всё такие же костыли к завтипам как plug+unplug и type families к rank-2 полиморфизму для монад в Расте
AN
а как ты определяешь костыли?
TK
Представь, что сигнатура функции является теоремой некоторой, и ты её обязан доказать в теле
TK
Понимаю, что оно так должно работать
AN
ну это какое-то слабое определение. у меня язык тьюринг полный. я что хочешь могу доказать
TK
С брендированными типами можно сделать эффективную индексацию, но нельзя заставить компилятор проверить, что он не unsound
TK
В общем, бесполезная фигня так-то)
AN
а как ты с завтипами что то проверяешь?
AN
точно так же там где то внутри get_unchecked(i)
TK
Говоря, например: "Обязуюсь вернуть беззнаковое число, меньшее длины такой-то коллекции"
TK
И оно прямо в сигнатуре функции в качестве возвращаемого типа
AN
я думал там похожий трюк с лайфтаймами.
TK
С лайфтаймами на выходе будет просто Index<'id>
AN
ты обязыешься вернуть лайфтайм 'a < 'b например. повсюду в расте.
RP
так, а про политику больше не говорим?