s
Так, просто взяв бинарное отношение между термом и его абстрагированной формой, мы уже получили нечто, похожее на тип.
Size: a a a
2020 October 29
s
Но на метауровне, а не на уровне термов.
s
Мы можем уточнить это отношение, привязав форму к входному параметру.
s
Вроде
lam(_, _) или lam(lam(_,_), _).s
Можем записать это инфиксно, как
_ → _ или (_ → _) → _.s
Короче, мы получили типы по Карри, просто взяв отношение между термом и абстрагированным термом.
s
Не зная вообще ничего про Рассела и его парадоксы.
s
Может быть, чтобы получить систему типов по Чёрчу, нужно знать что-то про Рассела.
s
Но по Карри это термы + sequent calculus с бинарным отношением.
ΑZ
evaluates_to(app(Ex, Ey), _) :- evaluates_to(Ex, lam(_)), evaluates_to(Ey, _).это пролог чтоли?
s
это пролог чтоли?
Да, я записал в синтаксисе пролога.
p
@DogeShibu у меня так случайно выходит кстати что можно в качестве Transient сервиса добавлять любые сервисы которые реализуют Dependency, и их не обязательно добавлять в ServiceProvider. Прикольный баг. Как думаешь, убрать его или оставить как фичу?
ΑZ
@DogeShibu у меня так случайно выходит кстати что можно в качестве Transient сервиса добавлять любые сервисы которые реализуют Dependency, и их не обязательно добавлять в ServiceProvider. Прикольный баг. Как думаешь, убрать его или оставить как фичу?
что это значит?
ΑZ
и вопрос, как ты резолвишь если челик делает синглтон сервис с зависимостью от transient/scoped?
p
что это значит?
Типо я в ServiceProvider не добавляю зависимость но ее можно получить лол
p
и вопрос, как ты резолвишь если челик делает синглтон сервис с зависимостью от transient/scoped?
transient же означает что инициализация зависимости производится при запросе зависимости
p
Значит и в синглтон ее можно добавлять
p
Так ведь?
ΑZ
Так ведь?
так