GP
выводы
сделал выводы в голос
Size: a a a
2020 February 17
DM
на самом деле скала 3 уже гораздо лучше выводы делает
Но ваши выводы были безупречны. Сложная система типов не может позволить такого идеала.
Oℕ
так систем ф тоже не позволяет
Oℕ
система ХМ позволяет
DM
Oℕ
при типах второго ранга хошкель тоже не может все типы вывести
GP
токсичный сова
GP
Oℕ
в присутствии рекурсии
(
система ХМ позволяет
Система выводов ведьмака
(
Так сказать
DM
А разве в ф выше первого? (я опять перепутал с кем то)
(
Oℕ
А разве в ф выше первого? (я опять перепутал с кем то)
второй
DM
При втором ранге вики говорила иногда можно еще
Oℕ
The version of System F used in this article is as an explicitly typed, or Church-style, calculus. The typing information contained in λ-terms makes type-checking straightforward. Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking is undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.[2][3]
Wells's result implies that type inference for System F is impossible. A restriction of System F known as "Hindley–Milner", or simply "HM", does have an easy type inference algorithm and is used for many statically typed functional programming languages such as Haskell 98 and the ML family. Over time, as the restrictions of HM-style type systems have become apparent, languages have steadily moved to more expressive logics for their type systems. GHC a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality;[4] non-HM features in OCaml's type system include GADT.[5][6]
Wells's result implies that type inference for System F is impossible. A restriction of System F known as "Hindley–Milner", or simply "HM", does have an easy type inference algorithm and is used for many statically typed functional programming languages such as Haskell 98 and the ML family. Over time, as the restrictions of HM-style type systems have become apparent, languages have steadily moved to more expressive logics for their type systems. GHC a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality;[4] non-HM features in OCaml's type system include GADT.[5][6]