• CS typefun dependent-types И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
    Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?

Replies (13)

  • @qnikst, а что за линейные стркуткуры ?
  • @segfault, Список у которого элемент и хвост линейные типы
  • @qnikst, + длина на уровне типов
  • @qnikst, А какой язык?
  • @segfault, idris например
  • @qnikst, ну там unique types но я тонкую грань между ними пока не понял
  • @qnikst, Это вы там на идрисоконфе то? Приколько вам там.
  • @segfault, ну нам посоветовали не делать сортировку, т.к. если доказательство сортированности списка и длины можно сделать, то доказать что новый вектор это перестановка элементов старого уже сложн и на идрисе малореально, проще брать кок. Мне интересно можно ли там схалявить
  • @qnikst, а я правильно понял, что линейные типы не дадут сделать `\a -> repeat (length a) 1` ?
  • @segfault, ну т.е. если даже доказать длину и сортированность.
  • @segfault, да
  • @segfault, в этом и фишка, но я не знаю мжно ли это или честно ли это. лектор сказал, что тоже не знает. Спросил пока в рабочем чятике
  • @qnikst, Запилил вчера сортировку на линейных типах, с гарантией сохранения длины. Удовольствие ниже среднего, полиморфных по uniquenessity (?) типов нет, методов почти нет; классов нет; доказательств и лемм нет; еще похоже и баги в тайпчеккере, которые приводят к тому, что ReadOnly (Borrowed) значения "съедают" линейные. В итоге для своих собственных Nat, в cps-стиле в проверках оно скомпилировалось и работает, но писать доказательство сортированности для этого дела, я наверное не готов. Разве мне объяснят почему итоговая сортировка будет доказанной.