SS
Прикольно
Size: a a a
2021 May 31
[
SS
Но что концептуально другого это дает?
[
Завтипы могут выразить программу без крашей
SS
Вот тут gen - это и есть завтипы?
[
Ага, и f
SS
При 0 одно поведение при чём то другом - другое
[
[
Это обычное сравнение с шаблоном
gо
Ты можешь доказывать рантаймовые свойства.
Раст паникует, когда ты обращаешься по невалидному индексу, но зачем вообще компилировать программу с обращением по невалидному индексу.
Раст паникует, когда ты обращаешься по невалидному индексу, но зачем вообще компилировать программу с обращением по невалидному индексу.
[
Смотри на сигнатуры
SS
Я вообще не понимаю синтаксис Хаскеля)
[
Это не хаскель
[
Это идрис
gо
Кам он, как будто есть серьёзная синтаксическая разница
[
В хаскеле нет завтипов😢
[
В хаскеле два двоеточия!
[
И Nat не выражен через числа пиано
gо
enum Fin<N> {
Z,
S(Fin),
}
fn gen(x: Nat) -> Fin<x + 1> {
match x {
Nat::Z => Self::Z,
Nat::S(prev) => Self::S(gen(prev)),
}
}[
Вернее, это просто исправить