![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
akuklevВ комментах к прошлому посту ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
krlz прислал линк на более доступное описание (слайды) System S, полиморфного лямбда-исчисления с поддержкой зависимых типов: http://staff.computing.dundee.ac.uk/pengfu/document/talks/rta-tlca-14.pdf.
Выложу ещё из комментов, почему я считаю, что это важно: «Я уже упоминал о вселенском разрыве между тем, как проработаны в смысле computational overhead elimination и оптимизации производительности языки на базе полиморфного лямбда-исчисления (в особенности OCaml и SML), и как убого это выглядит в отношении языков на базе зависимых теорий типов: там вопросы computational overhead elimination и оптимизации — это непаханое поле на десяток лет работы в лучшем случае.
Так что если говорить о превращении зависимых типов из академического изыска в повседневный инструмент, то вложение замысловатых интуиционистских теорий типов в изъезженное вдоль и поперёк полиморфное лямбда-исчисление, это просто то, что доктор прописал.
Пока мне непонятно, насколько сильна System S. На данный момент у меня впечатление, что я понимаю как там делать indexed containers, но этого мало, на практике хочется умения делать там любые fibered data types, чтобы можно было осуществлять туда трансляцию из Агды. Вообще fibered data types это очень могучая абстракция данных, они включают в себя индексированные индуктивно-индуктивно-рекурсивные типы данных, indexed containers и тем более W-types как мелкие частные случаи. До недавнего времени не было понятно, замкнут ли этот класс типов относительно композиции, и как их описывать так, чтобы для понимания не требовалось 10 лет ботанья жосткого категорного матана, однако судя по всему в этой области недавно случился прорыв: https://pigworker.wordpress.com/2015/01/01/irish-induction-recursion/.
Очень было бы здорово, если бы System S реально предоставляла effective typed (impredicative) lambda-encodings for fibered data types.
Вообще хочется текстбука на тему fibered inductive datatypes, где шаг за шагом разрабатываются примеры хитрых типов данных, начиная от натуральных чисел Nat, конечных чисел Fin(n : Nat), списков List, списков фиксированной длинны Vec(n: Nat), продолжая замысловатыми, но нужными в народном хозяйстве типами данных вроде traffic-dependent session types (включая Conway games, включая surreal numbers), evaluation trees, deduction trees, red-black trees и вообще balanced trees, и заканчивая совсем замысловатыми типами навроде typed abstract syntax trees (incl. case of dependently typed languages), Tarski universes, PER-based and set-theoretic models.
Или можно подождать, пока fibered data types интерпретируют в HoTT/CubTT и обобщат до higher fibered data types (вон Альтенкрих уже весь в работе над higher indexed containers, и вроде там всё гладко), тогда можно будет смело добавлять в текстбук всевозможные quotient types и suspension types:
от Bool получается интервал и спектр сфер, от List получаются Cycle, Collection (aka Finite Multiset) и всевозможные другие Combinatorial Species, от структурированных коллекций всевозможные Concrete Shape Categories; кроме того, можно определить Cauchy Reals, Model of ZFC set theory, univalent universes. Сверхзадачей было бы сделать обогащённое path abstractions (a la Cubical Type Theory) полиморфное лямбда-исчисление, обеспечивающее effective typed (impredicative) lambda-encodings for higher fibered data types.
krlz прислал линк на более доступное описание (слайды) System S, полиморфного лямбда-исчисления с поддержкой зависимых типов: http://staff.computing.dundee.ac.uk/pengfu/document/talks/rta-tlca-14.pdf.Выложу ещё из комментов, почему я считаю, что это важно: «Я уже упоминал о вселенском разрыве между тем, как проработаны в смысле computational overhead elimination и оптимизации производительности языки на базе полиморфного лямбда-исчисления (в особенности OCaml и SML), и как убого это выглядит в отношении языков на базе зависимых теорий типов: там вопросы computational overhead elimination и оптимизации — это непаханое поле на десяток лет работы в лучшем случае.
Так что если говорить о превращении зависимых типов из академического изыска в повседневный инструмент, то вложение замысловатых интуиционистских теорий типов в изъезженное вдоль и поперёк полиморфное лямбда-исчисление, это просто то, что доктор прописал.
Пока мне непонятно, насколько сильна System S. На данный момент у меня впечатление, что я понимаю как там делать indexed containers, но этого мало, на практике хочется умения делать там любые fibered data types, чтобы можно было осуществлять туда трансляцию из Агды. Вообще fibered data types это очень могучая абстракция данных, они включают в себя индексированные индуктивно-индуктивно-рекурсивные типы данных, indexed containers и тем более W-types как мелкие частные случаи. До недавнего времени не было понятно, замкнут ли этот класс типов относительно композиции, и как их описывать так, чтобы для понимания не требовалось 10 лет ботанья жосткого категорного матана, однако судя по всему в этой области недавно случился прорыв: https://pigworker.wordpress.com/2015/01/01/irish-induction-recursion/.
Очень было бы здорово, если бы System S реально предоставляла effective typed (impredicative) lambda-encodings for fibered data types.
Вообще хочется текстбука на тему fibered inductive datatypes, где шаг за шагом разрабатываются примеры хитрых типов данных, начиная от натуральных чисел Nat, конечных чисел Fin(n : Nat), списков List, списков фиксированной длинны Vec(n: Nat), продолжая замысловатыми, но нужными в народном хозяйстве типами данных вроде traffic-dependent session types (включая Conway games, включая surreal numbers), evaluation trees, deduction trees, red-black trees и вообще balanced trees, и заканчивая совсем замысловатыми типами навроде typed abstract syntax trees (incl. case of dependently typed languages), Tarski universes, PER-based and set-theoretic models.
Или можно подождать, пока fibered data types интерпретируют в HoTT/CubTT и обобщат до higher fibered data types (вон Альтенкрих уже весь в работе над higher indexed containers, и вроде там всё гладко), тогда можно будет смело добавлять в текстбук всевозможные quotient types и suspension types:
от Bool получается интервал и спектр сфер, от List получаются Cycle, Collection (aka Finite Multiset) и всевозможные другие Combinatorial Species, от структурированных коллекций всевозможные Concrete Shape Categories; кроме того, можно определить Cauchy Reals, Model of ZFC set theory, univalent universes. Сверхзадачей было бы сделать обогащённое path abstractions (a la Cubical Type Theory) полиморфное лямбда-исчисление, обеспечивающее effective typed (impredicative) lambda-encodings for higher fibered data types.
