PS
всё придумал Вегнер, Кнут только рядом стоял!
Вот это уже серьезный выпад :)
Size: a a a
2021 March 24
DK
А какие значимые работы у Кормена есть по PL/компиляторам?
Я про Алгоритмы
AG
Вот это уже серьезный выпад :)
PS
Да, я эту статью читал неоднократно :)
DK
Рекурсивный низ. подход ?
AG
двухсторонний скорее :)
AG
у bidirectional тайпчекеров наверняка тоже ноги откуда-то отсюда растут
к
раз уж заговирили про bidirectional тайпчекеры.
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
A
раз уж заговирили про bidirectional тайпчекеры.
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
Не является, надо на стрелки смотреть.
(Хотя особого смысла в нём нет при наличии
⇒ означает, что выполняется синтез типа, то есть тип - выходное значение, а определить его можно, зная только Γ и x. А вот ⇐ - это проверка типа, в таком случае тип должен быть известен заранее. То есть A будет аргументом в таком правиле:(x : A) ∈ Γ
----------- Var⇐
Γ ⊢ x ⇐ A
(Хотя особого смысла в нём нет при наличии
Sub⇐)к
ну, вот тут A и аргумент, и результат
но тут понятно что он из терма пришел
но тут понятно что он из терма пришел
A
Да. Это всё есть в описании правил. Для
→I⇐, например, объясняется, почему тип для лямбды проверяется, а не синтезируется
A
Если попытаться сделать правило с
Γ ⊢ (λx.e) ⇒ A1 → A2, то негде будет взять тип A1, чтобы добавить тип x в контекст для синтеза A22021 March 25
AG
раз уж заговирили про bidirectional тайпчекеры.
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
нет, тип переменных выводится
AG
точнее достается из словаря, куда его кладет кейс для лямбды
AG
поэтому лямбды и аннотируются
AG
Если попытаться сделать правило с
Γ ⊢ (λx.e) ⇒ A1 → A2, то негде будет взять тип A1, чтобы добавить тип x в контекст для синтеза A2^
ЗП
раз уж заговирили про bidirectional тайпчекеры.
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
вот тут правило по выводу типа A, но не ясно по предпосылке (x : A) elem Г, является ли A аргументом
то есть это правило что
> для аргументов (x, A, Г) вывести тип x как A, если x : A есть в контексте
ИЛИ ЖЕ
> для аргументов (x, Г), если в контексте есть какой-то x : A, то вывести тип x как A
https://www.cl.cam.ac.uk/~nk480/bidir-survey.pdf - страница 3
похоже для этого языка тоже использовали этот пейпер
https://github.com/zehaochen19/vanilla-lang
https://github.com/zehaochen19/vanilla-lang
M
https://rms-support-letter.github.io/
Просьба поддержать Столлмана
Просьба поддержать Столлмана