ВСЕМ ПОХЕР-2
Забавно - как мне тут указали товарищи - насчет разрешимости Java я ошибался:
https://arxiv.org/pdf/1605.05274.pdf
таки неразрешима.
"Попали на сабтайпинг"
Что по мне довольно удивительно, так как варианты system F с сабтайпингом отклассифицированы еще в 80-е годы и неразрешимая там только одна - самая-самая навороченная, причем никакой особенной пользы в ее навороченности нет - там вся жопа стрясается из-за одного не слишком нужного правило вывода.
Ее скорее из соображений общности рассматривали.
Попасть на это не использовав почти ничего что собственно делает эту и близкие к ней подсистемы интересной - великая моща в работе с типами высших порядков - которых в Жабе просто нет. Но тем не менее...
заодно опробовал тестик еще на нескольких езыках:
Так вот как ни смешно - единственный кто это переварил - G++.
При том что и haskell и ocaml тут вполне разрешимы (в haskell неразрешимости возникают если включить расширенную версию языка, ocaml попадает на type-checkingе параметризованных модулей (где действительно юзается вся system F<: во всей ее мощи.
заодно замечу, что в полезности полноты по Тьюрингу системы плюсовых темплейтов я сильно сомневаюсь - практически уверен, что там для всего для чего ее используют реально, хватит примитивной рекурсии (те же списки она покрывает).
А она разрешима и енфорсится очень просто - типизацией системы типов "по Черчу" - kind's из Haskell например (то есть в Haskell можно написать арифметику на типах - и ее и пишут - поскольку констант-то целочисленных в параметрах типов он не допускает - но неразрешимым стандартный Haskell это не делает)
То есть на разрешимость всем похер еще даже более, чем я думал - мне-то казалось, что в java об этом из чистоплюйства позаботились :)
https://arxiv.org/pdf/1605.05274.pdf
таки неразрешима.
"Попали на сабтайпинг"
Что по мне довольно удивительно, так как варианты system F с сабтайпингом отклассифицированы еще в 80-е годы и неразрешимая там только одна - самая-самая навороченная, причем никакой особенной пользы в ее навороченности нет - там вся жопа стрясается из-за одного не слишком нужного правило вывода.
Ее скорее из соображений общности рассматривали.
Попасть на это не использовав почти ничего что собственно делает эту и близкие к ней подсистемы интересной - великая моща в работе с типами высших порядков - которых в Жабе просто нет. Но тем не менее...
заодно опробовал тестик еще на нескольких езыках:
type ('a, 'b) c = C of 'a * 'b
let f : 'a -> ('a, 'a) c = fun x -> C (x, x)
let x = 1 |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f |> f
data C a b = C a b
f :: a -> C a a
f x = C x x
main = 1
x = 1 $ f $ f $ f $ f $ f $ f $ f $ f $ f $ f
$ f $ f $ f $ f $ f $ f $ f $ f $ f $ f
template <class A, class B> class C { };
template <class T> C<T, T> f (T x) { return C<T, T>(); }
int main () {
auto i =
f (f (f (f (f (f (f ( f (f (f (f (f (f (f ( f (f (f (f (f (f (f (
f (f (f (f (f (f (f ( f (f (f (f (f (f (f ( f (f (f (f (f (f (f (
1
))))))) ))))))) )))))))
))))))) ))))))) )))))));
return 1;
}Так вот как ни смешно - единственный кто это переварил - G++.
При том что и haskell и ocaml тут вполне разрешимы (в haskell неразрешимости возникают если включить расширенную версию языка, ocaml попадает на type-checkingе параметризованных модулей (где действительно юзается вся system F<: во всей ее мощи.
заодно замечу, что в полезности полноты по Тьюрингу системы плюсовых темплейтов я сильно сомневаюсь - практически уверен, что там для всего для чего ее используют реально, хватит примитивной рекурсии (те же списки она покрывает).
А она разрешима и енфорсится очень просто - типизацией системы типов "по Черчу" - kind's из Haskell например (то есть в Haskell можно написать арифметику на типах - и ее и пишут - поскольку констант-то целочисленных в параметрах типов он не допускает - но неразрешимым стандартный Haskell это не делает)
То есть на разрешимость всем похер еще даже более, чем я думал - мне-то казалось, что в java об этом из чистоплюйства позаботились :)