алгоритм J и bidirectional typechecking, но может есть ещё популярные методы?
когда-то искал какие ещё виды бывают. и натыкался на что-то с названием tridirectional вот это вроде, третье направление, как я понимаю, появляется, когда идет не synth внешнего -> check внутреннего выражения, а synth внутреннего и уже потом check внешнего, но я пока не пытался разобраться как это работает 😥
а, тут вообще зависимые типы
Ну они вроде сделали зависимые с бидиром и получилась undecidable система типов
Хороший небольшой tutorial с реализацией всех базовых идей
https://davidchristiansen.dk/tutorials/nbe/
Обсуждают сегодня