generic code and dependent types
I'm interested in the proposals for adding type annotation. Coming from some experience with generic code in c++, one of the difficult issues has been reasoning about dependent types in generic code. In general, we need to be able to declare a type via an arbitrary metafunction some_metafunction<T>::type F (... It is also useful to be able to write something like: typedef typeof (int() * float()) my_type; I wonder if any of the proposals will be able to handle this sort of algebra on types? I think it's needed to truly support generic code.
On Fri, Aug 15, 2014 at 06:56:46AM -0400, Neal Becker wrote:
I'm interested in the proposals for adding type annotation. Coming from some experience with generic code in c++, one of the difficult issues has been reasoning about dependent types in generic code.
In general, we need to be able to declare a type via an arbitrary metafunction
some_metafunction<T>::type F (...
It is also useful to be able to write something like:
typedef typeof (int() * float()) my_type;
I wonder if any of the proposals will be able to handle this sort of algebra on types? I think it's needed to truly support generic code.
Let's pretend that this is a Python mailing list, and that some readers aren't familiar with C++ generic syntax :-) What does typedef typeof (int() * float()) my_type; do? From a Python perspecive, that looks like type(0*0.0) which will return float. Presumably that's not what you want, or you would have just said "float". So what am I missing? (Apart from years of C++ experience.) -- Steven
Am 15.08.2014 14:26, schrieb Steven D'Aprano:
Let's pretend that this is a Python mailing list, and that some readers aren't familiar with C++ generic syntax :-) What does
typedef typeof (int() * float()) my_type;
do?
I think its "whatever type operator*(int a, float b)" returns. Or more generally: "whatever type a suitable * operator returns after, where suitable means after int and float might or might not have been casted into another type so that a matching operator was found" So, for example, if there were no operator*(int a, float b), it would look if there's at operator*(int a, int b), and if not, operator*(float, float) (or vice versa). The "advantage" is that you do not need to change your code if the meaning of multiplying an int with a float changes.
Dennis Brakhane wrote:
Am 15.08.2014 14:26, schrieb Steven D'Aprano:
Let's pretend that this is a Python mailing list, and that some readers aren't familiar with C++ generic syntax :-) What does
typedef typeof (int() * float()) my_type;
do?
I think its "whatever type operator*(int a, float b)" returns.
Or more generally: "whatever type a suitable * operator returns after, where suitable means after int and float might or might not have been casted into another type so that a matching operator was found"
So, for example, if there were no operator*(int a, float b), it would look if there's at operator*(int a, int b), and if not, operator*(float, float) (or vice versa).
The "advantage" is that you do not need to change your code if the meaning of multiplying an int with a float changes.
I really meant more like typeof (A() * B()) where A and B are 2 types, and A() is a call to the default constructor for A. For example ret_t multiply (A a, B b): return a * b what is ret_t?
Am 15.08.2014 12:56, schrieb Neal Becker:
I wonder if any of the proposals will be able to handle this sort of algebra on types? I think it's needed to truly support generic code.
I hope it won't ;-) I agree that it is needed for truly generic code, but if Python gains a truly complete type system, then what's the point of having dynamic typing at all? At this point, you might as well program in Scala instead. What's the point in trying to turn Python into a statically typed language that can optionally be dynamically typed? There are enough good static languages out there. IMHO, the type information in Python should be considered part of the documentation, if the type system gets too complex and can only be parsed by the linter, then what's the point? Is the information: "this function takes an Iterable of T and a Map[U,Map[U,T]|T|int] and returns the type of the result of foo applied to parameters of type T and U" really useful for a programmer anymore? Does it help me if the linter says that "Map[int,float]" is not compatible with "T|Map[U,V subtype str]|Map[U subtype str, V]"? I think if my unit test fails with a "TypeError: float has no method strip" that's a much more useful information to me. So I think limiting the power of the type system will actually be a good thing.
On Fri, Aug 15, 2014 at 8:36 AM, Dennis Brakhane
What's the point in trying to turn Python into a statically typed language that can optionally be dynamically typed? There are enough good static languages out there.
That's important. Even within the standard lib, Python is a well behaved systems citizen, so people are free to write parts of their software in any language/environment, and Python will happily communicate with whatever. Cheers, -- Juancarlo *Añez*
Le 15/08/2014 06:56, Neal Becker a écrit :
I'm interested in the proposals for adding type annotation. Coming from some experience with generic code in c++, one of the difficult issues has been reasoning about dependent types in generic code.
In general, we need to be able to declare a type via an arbitrary metafunction
some_metafunction<T>::type F (...
What is a metafunction?
Am 16.08.2014 06:24, schrieb Antoine Pitrou:
What is a metafunction?
In C++, roughly speaking a function that is evaluated at compile time not runtime, used for template metaprogramming. They accept compile time constants and types as parameters and return constants or types. So as a silly example, if we were to have metafunctions in Python's type system, it would allow me to define a metafunction NestedList, and if I wrote def (x: NestedList[3, int]) it could be evaluated to def(x: List[List[List[int]]]) or IntOrString which would evaluate to Int if the parameter was true, or String otherwise.
participants (5)
-
Antoine Pitrou -
Dennis Brakhane -
Juancarlo Añez -
Neal Becker -
Steven D'Aprano