3 ms·
> "full" dependent types From the quotation marks, I surmise that you're wondering what a non-full dependent type system could possibly mean. I added that qual
by gilch 4y ago
> "full" dependent types
From the quotation marks, I surmise that you're wondering what a non-full dependent type system could possibly mean. I added that qualifier because Python, in fact, had one, last I checked, with its `Literal` type (https://peps.python.org/pep-0586/#rejected-or-out-of-scope-ideas https://peps.python.org/pep-0586/#rejected-or-out-of-scope-i...), which is "a very simplified dependent type system", according to the PEP, but "True dependent types" are out of scope, at least for now.
- still_grokking 4y ago> From the quotation marks, I surmise that you're wondering what a non-full dependent type system could possibly mean. That wasn't the point. Scala has a few variants of dependent types but that features are constantly diminished as not being "full" (or sometimes even "real") dependent types. I don't buy that as dependent types aren't defined as being like dependent types in say CoC (the Calculus of Constructions). For example Singleton types match also the definition of dependent types when derived from literals; even such types are still weaker than the usual "full" dependent types à la CoC. Regarding Python: Python has only one type, the "almighty-python-runtime-type", as it's a "dynamic" (unityped) language. Therefore it does not make much sense to talk about "types" in Python at all… https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...