Simple dependent types

@gvanrossum

[This is based on a discussion between me and @gvanrossum last week. I'm writing this down so that we won't forget about this.]

Several stdlib functions have signatures where the return type depends on the value of an argument. Examples:

open returns an IO[str] or IO[bytes] depending on whether the mode argument has 'b' as a substring.
subprocess.check_output returns a str or bytes depending on the value of the boolean universal_newlines argument.

A simple way to support these would be to introduce a few additional types that work with str and bool literals:

A string pattern type that can describe the contents of a string literal, perhaps using a regular expression.
Types for False and True.

For example, if we had FalseType and TrueType, we could write a function whose return value depends on the value of a boolean argument:

@overload
def f(x: FalseType) -> bytes: ...
@overload
def f(x: TrueType) -> str: ...

def f(x: Any) -> Any:
    if x:
        return 'x'
    else:
        return b'x'

reveal_type(f(False))  # bytes
reveal_type(f(True)  # str

Not sure about this one:

...
x = bool('')
reveal_type(f(x))  # Union[str, bytes] since we don't know the boolean value statically?

We could also have a generic class where a generic type argument depends on the value of an argument to __init__. Not sure how we should represent these -- here is one potential approach:

class C(Generic[AnyStr]):
    @overload
    @returntype('C[str]')
    def __init__(self, x: TrueType) -> None: ...
    @overload
    @returntype('C[bytes]')
    def __init__(self, x: FalseType) -> None: ...
    ...

reveal_type(C(True))  # C[str]

Alternatively, we could use __new__, but this would be problematic if there is no corresponding method defined at runtime.

I think we can have LiteralType as in LiteralType['w'], LiteralType[True] etc. I think it will be better than special-casing True/False/string. Maybe we will get simple constant propagation "falling out" of type aliases (which might be helpful for e.g. NamedTuple)

I think regex will be problematic. How do you determine whether they overlap? String literals seems to suffice.

(And I don't think it counts as dependent type since it has little to do with runtime).

@JukkaL

The mode string syntax for open() is more complicated than just 'r', 'w', etc. Hence the regex.

I find LiteralType[True] pretty verbose; also it's more general than we want to implement (we really don't want this to be a big project, just enough to handle the cases @JukkaL mentioned).

If this doesn't count as a dependent type maybe you can explain your definition of dependent types? And what would you call this?

I'm not sure going into definitions is helpful, but the difference is (I guess) the reason you call it "Simple" dependent types - there nothing like def foo(x: int, y: bar[x]) -> str if x == 5 else bool. There's only information immediately available at compile time. Instead of defining True to be a literal of type bool, we define it as being a literal of type TrueType which is a subtype of (or coercible to) bool. I don't see the difference between this and the kind of types we already have. Just because the type has precisely single value you have precise information about its runtime value, but this is already the case with None, Void and Tuple[()].

However, I might be wrong. I am also too easily dragged into issues of terminology.

Possibilities for when you can't statically determine the overload variant because your argument isn't literal enough: * Union the alternatives you've got * Use the return type of the implementation (if any) (simpler, I think) * Use `Any` (simplest, I think)

…

On Mon, Mar 27, 2017 at 2:37 PM, Guido van Rossum ***@***.***> wrote: The mode string syntax for open() is more complicated than just 'r', 'w', etc. Hence the regex. I find LiteralType[True] pretty verbose; also it's more general than we want to implement (we really don't want this to be a big project, just enough to handle the cases @JukkaL <https://github.com/JukkaL> mentioned). If this doesn't count as a dependent type maybe you can explain your definition of dependent types? And what would you call this? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#3062 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABjs4Q_pmhJYnbeMNorZzX3OAIZpKeCzks5rqCw1gaJpZM4Mqfj6> .

I suspect special cases will continue to appear and build, and one day we will have to do this big project - which I have the feeling is not big right now, but will be big then and not easily backwards-compatible since special-casing is too easy to over fit for specific applications.

How complex is the mode for open? Correct me if I'm wrong, but it is not a language of infinite size; can't it be handled simply by many @overloads in the stub file?

Back when there were a couple interns working on this feature for a week, we had a few different use cases that they wanted to support:

open (a finite string-based language)
pow (wanted to dispatch on positive vs. negative exponents)
subprocess.check_output

What else? Is pow an odd one out here? Is open? Or are these complicated ones rare, and in the common case you just want to dispatch on a constant?

Maybe also Tuple * 5... Maybe pow can be handled by having positive and negative integer "subset types".

Any finite language is dispatch on a constant.

As of 3.6, the subprocess.check_output case is actually more complicated: it returns str if universal_newlines is True OR encoding is non-None, and bytes otherwise. I suppose existing overloads can take care of the encoding part: you'd have overloads for encoding is non-None returning str, universal_newlines=True returning str, and universal_newlines=False returning bytes.

But the main thing we really want is determining the correct return type when the argument is a compile-time literal. You can't overload on True or False because there's no way to spell "the subtype of bool that only contains True" (etc.). If it can't be determined what the value is at compile time it's okay to revert to the more general overload. Similar for open() and everything that takes a similar mode string (it's bred quite a following).

I would prefer this syntax:

from pathlib import Path

# type function
def open_return_type(kwargs: Dict[str, object]) -> Type[object]:
    assert isinstance(kwargs['mode'], str)
    if 'b' in kwargs['mode']:
        return IO[bytes]
    else:
        return IO[str]

def open(file: Union[str, bytes, int, Path], mode: str = 'r', buffering: int = -1,
         encoding: str = None, errors: str = None, newline: str = None,
         closefd: bool = ...) -> open_return_type: ...

It's flexible, and can be implemented like this:

TypeAnalyser.visit_unbound_type needs to allow "type functions" in function annotation
TypeChecker.check_return_statement, if it sees a type function, needs to call it, passing it the dict of all the arguments for which it knows literal values
if the type function returns a value, the type checker can use it as the return type
if the type function raises KeyError, the type checker should assume it relies on an argument that it doesn't know the value of; since it cannot infer the return type, it should do something sensible (e.g., issue a warning and use the return type based on the type context)

if it sees a type function, needs to call it,

How? Running arbitrary user code is certainly out of question. What do you suggest? To me this sounds like a turing-complete metaprogramming language and full-blown dependent type system.

I do like is the idea of avoiding the scoping problem (how to express def f(x, y:g(x)): ... using another function. But it will only be needed for fully-dependent type system, not for singleton-types.

@elazarg

@elazarg Ah yes, I did mean to run arbitrary user code. If the type checker is not allowed to do that for security or other reasons, my suggestion won't work.

It can't really do that in general, since there's nothing requiring type checkers to run in the same Python version as they're checking for, or even in Python at all.

Just found this: https://typesandkinds.wordpress.com/#what-are-singletons

@mehdigmira

@mehdigmira The plugin API is not documented, so you are on your own if you want to go there. There are some examples at https://github.com/python/mypy/tree/master/mypy/plugins.

@JukkaL

@JukkaL Thank you for the response.
I've peeked into these example.
My understanding is that if i wanted to do that I'd have to write one function-hook for every function in my code that relies on this dependant type logic. Is this true ?

@mehdigmira

@mehdigmira Yes. The plugin approach is really only practical for library functions with relatively stable interfaces, in my opinion. Otherwise it will be too difficult to maintain.

@ilevkivskyi

Here's my current thinking on what's needed to support this in a minimally useful fashion.

Our current idea for the syntax is like this:

Type syntax is Literal[x], where x can be True, False, an integer literal or a string literal (not sure about bytes).
Literal[x, y] is equivalent to Union[Literal[x], Literal[y]].

Literal types are not inferred for variables unless the lvalue is final:

y: Literal['foo'] = 'foo'  # Without the annotation the type would be 'str'
x: Final = 'foo'  # Type is Literal['foo']
z = 'foo'  # Type of 'z' is 'str'
zz: Final = z  # The type of 'zz' is 'str' here as well

Note that the Final exception only applies to simple types:

a: Final = ['a']  # Inferred type is still List[str]

We'd likely promote a string literal to str in many/most contexts, but I'm not sure what the precise rules should be.

Literal types are compatible with the corresponding non-literal types, but not the other way around:

x = 'foo'
y: Literal['foo'] = x  # Error
z: str = y  # Ok

For overloads we may need a fallback in addition to literal types to avoid false positives with legacy interfaces:

@overload
def f(x: Literal[True]) -> str: ...
@overload
def f(x: Literal[False]) -> bytes: ...
@overload
def f(x: bool) -> Any: ...

y: bool = ...
a = f(y)  # Any inferred
b = f(True)  # str inferred

cc @ilevkivskyi

I really don't like the enforced Literal[...] syntax. Python type annotations are already annoyingly verbose and often hard to read, compared to, for example, typescript. I understand that strings are problematic, due to forward references, but couldn't at least booleans and integers (and potentially bytes) be abbreviated with just x: True or y: 42? That would open the possibility to have a potential __future__ import (that only works in combination with annotations) to use string literals as dependent types as well.

If we don't want to execute arbitrary Python code at the type level, how about specifying a value-to-type mapping with a dict? Something like this:

def f(x: bool) -> FResult[x]: ...
#                         ^ the argument `x`   

FResult = TypeMapping[bool]({
  True:  str,
  False: bytes,
})

It's less verbose than @overloading every case, and perhaps more obvious than Literal[True]. Referring to the value of x in a type looks a bit weird [1], but that's what dependently-typed languages like Idris do [2], so it's not without precedent.

Here's a bigger example where the type depends on two arguments:

def open_file(path: str, access: str = 'r', encoding: str = 'u') -> SomeFile[access, encoding]: ...

SomeFile = TypeMapping[str, str]({
  ('r', 'u'): ReadableFile[str], # a read-only handle
  ('r', 'b'): ReadableFile[bytes],
  ('w', 'u'): WritableFile[str], # a write-only handle
  ('w', 'b'): WritableFile[bytes],
})

There's a bunch of ways TypeMapping can be made more expressive if desired. For example it could take a default parameter, making it like defaultdict. We could also make it more DSL-ish and allow more general pattern matching – I can post ideas for that in a follow-up if anyone's interested.

[1] Using a function argument in a type annotation would constrain this extension to python 3.7+ where type annotations aren't evaluated. This could be remedied with something like x = ArgVar('x') above the definition, but that could interfere with the actual code.

[2] For an example, see the printf function in typesafe printf

@srittau

@srittau Something like the Literal[...] syntax is needed at least until Python 3.8, since things like Tuple[True, False] generate a runtime error at the moment. Bare literal as a type can be proposed for Python 3.8 or later. I think that we should start with something that works with already released Python versions, however.

@lubieowoce Your proposal introduces quite a bit of new syntax for functionality that @overload already supports. I think that there would have to be some important use cases that could be supported with the proposed syntax before it might be worth the extra implementation effort (and cognitive load). Verbosity does not sound like a very compelling argument to me, since I don't expect overloads involving literal types to be that common.

@JukkaL

@JukkaL -- @Michael0x2a and me are already working on a draft-PEP about Final and Literal (it is not yet public, we will publish when we are relatively happy with the draft). Basically, it is just extended/detailed version of your comment above.

@lubieowoce -- Overloads (including type guards) is an important use case which will be explicitly mentioned in the draft PEP.

@srittau -- I don't think literal types will be used so often that saving 6 keystrokes is important. Second, I think explicit is better than implicit here, some people may be confused by bare literals in annotations. Finally, as Jukka mentioned, it just doesn't work.

Anyway, I would propose to pause the discussion here until the actual draft is posted here (hopefully very soon).

@ilevkivskyi

@ilevkivskyi Would something like Literal[x>0] work?

No.

@ilevkivskyi

@ilevkivskyi @JukkaL thank you for your comments. I'm aware (and not too happy) that my proposal duplicates some functionality – I didn't mention it to keep the post short. I'll hold off with responding until you publish the draft PEP – perhaps it'll clarify some things that concerned me about the @overload+Literal approach.

Small update -- here's the draft PEP mentioned above: https://github.com/Michael0x2a/peps/blob/literal-types/pep-9999.rst.

I think the new plan is to try discussing it on our shiny new typing-sigs mailing list instead of here, though? We'll see how it goes.

@Michael0x2a

@Michael0x2a seeing as PEP 586 is accepted (congrats!) perhaps this can be closed, in favor of #5935?

Yes, mypy now supports literal types Literal[...].

Navigation Menu

Repository navigation

Simple dependent types #3062

19 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Simple dependent types #3062

Description

Activity

elazarg commented on Mar 27, 2017

gvanrossum commented on Mar 27, 2017

elazarg commented on Mar 27, 2017

sixolet commented on Mar 27, 2017

elazarg commented on Mar 27, 2017

sixolet commented on Mar 27, 2017

elazarg commented on Mar 27, 2017

JelleZijlstra commented on Mar 27, 2017

gvanrossum commented on Mar 27, 2017

pkch commented on Mar 28, 2017

elazarg commented on Mar 28, 2017

pkch commented on Mar 28, 2017

JelleZijlstra commented on Mar 28, 2017

elazarg commented on Mar 28, 2017

19 remaining items

JukkaL commented on Oct 30, 2018

mehdigmira commented on Oct 30, 2018

JukkaL commented on Oct 30, 2018

JukkaL commented on Oct 30, 2018

srittau commented on Oct 30, 2018

lubieowoce commented on Nov 1, 2018

JukkaL commented on Nov 1, 2018

ilevkivskyi commented on Nov 1, 2018

brainrake commented on Nov 1, 2018

ilevkivskyi commented on Nov 1, 2018

lubieowoce commented on Nov 1, 2018

Michael0x2a commented on Nov 20, 2018

emmatyping commented on Jul 4, 2019

JukkaL commented on Jul 4, 2019

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions