New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Feature Request] Contravariant generics (if feasible, but maybe infeasible) #187
Comments
Glorious request is glorious! Yes, contravariant type variables is absolutely in @beartype's wheelhouse, which increasingly resembles an API pigsty. Let's add this to the back burner with firm and resolute promises that we will do something about this, we solemnly swear it, even as we wring our hands in supplication towards the increasingly unruly Oh – and the fourth item of your tuple of (True, False, True, True, False) Is that right? Hidden Horrors Lurk off the Long-Forgotten ShoresLastly, we need to discuss the disgustingly huge alien megastructure hiding in the room. Thanks to the fact that PEP 484 and thus PEP 484-compliant type variables were never intended to actually be used by anyone at runtime, this may not be feasible. Specifically, subscripting a type hint subscripted by one or more type variables destructively replaces those type variables with their substituted type hints at runtime. The original type variables cannot be recovered from those type hints at runtime, because those type variables have been replaced by the That is to say, the type hint >>> MyFakeEntity.__args__
(typing.Union[int, str], <class '__main__.Fake'>) # <-- uhohs. "DataType" is gone, bro. EVERYTHING. IS. LOST.
>>> MyFakeEntity.__parameters__
() # <-- ...oh my Gods. I consider this a I acknowledge that this a tall ask. But... would you mind opening a discussion on Python's official Typing-sig mailing list about this? That's where all high-level discussion on Weep for me! My citizenry already do. |
Damnit, python, ya done me dirty again. Wellp. I wouldn't blame you to ignore this entirely, then! Not going to lie, the list of reasons to abandon the "lets me do anything" python land, which began with a lovely debate about HKTs, is growing ever longer. But hey, I guess life isn't as fun without Sisyphusian kicking against the proverbial goads. (unless, wait, is that just called masochism? So, as per my usual, is there another way...? I'm starting to think that user-derived types, similar to how you are starting to support NamedTuple, dataclass, etc, are a possibility to double down on. Perhaps there is room to "bless" certain types, especially user-created ones, with enhanced capabilities like contravariance, tagged unions, etc. You already have the machinery, right? These beautiful TypeHint objects. With a proper decorator, we can permanently attach metadata that informs beartype hey, this thing is an X, trust me. This means beartype can know or easily infer at run time the type of pretty much any "thing" that is or was derived from these special "blessed" types. And boom, we've kinda invented Algebraic BearTypes. I know this is sort've sounding like the tack that pydantic took, but rather than rely on a basemodel and focus on validation, we can maybe use relatively straight-fwd protocols to cleanly endow types with BearTypeable (or something). An outer beartype check makes sure that if we're trying to do something advanced, it at least passes an is_bearable beartypable check. Plus, the protocol approach means we can provide machinery for folks to add beartyp-ability to whatever-they-want™, and then just let them deal with the fallout™ of such decisions! Also, I'm pretty sure any types we can "assign" a priori to get a "TypeHintBadge" as metadata wouldn't need anything more than a subhint check at runtime, which is...faster? maybe? than full beartype type checking of a complicated nested type? So then the questions are 1) am I needlessly reinventing, what, GHC as a rebellious fiefdom in the kingdom of python, and should pack up my toys and go to a new sandbox? 😆 No joke, I booted up Stellaris for the first time from an old humble Bundle yesterday, after getting my steam deck in the mail. So glad you brought it up, and now I'm going to give it another go instead of losing myself to Factorio again for the 10th time. |
Perl 5 intensifies. Inb4 @tbsexton publishes a
You walk the dark plugin roads – and you walk them alone. Currently, @beartype lacks a plugin API. This is a thing we routinely think about until remembering that we lack this precious thing called time other sentient beings claim without evidence they have. beartype.vale.IsParametrization: Because We CanThat said, in the absence of official I contemplate a dread API resembling: # Old stuff copy-pasted from above. Boring!
from beartype.door import TypeHint as th
from beartype import typing as bt
E_ID = bt.Union[int,str] # Entity ID's
DataType = bt.TypeVar('DataType', bound=bt.Optional[bt.Iterable], contravariant=True)
Entity = bt.Tuple[E_ID, DataType] # So (valid_id, (some_data1, some_data2, ...))
class Fake(bt.NamedTuple):
name:str
kind:str
velocity:float
# NEW STUFF IS NEW. Excitement ensues as madness prevails.
from beartype.typing import Annotated
from beartype.vale import IsParametrization
# PEP-compliant type hint notifying @beartype that "Entity[Fake]" is
# the result of substituting one or more type variables subscripting
# the "Entity" type hint with concrete types satisfying those variables,
# while preserving compatibility with static type-checkers and IDEs.
#
# @beartype will then dynamically do the rest. Specifically, by the
# dark power of introspection, @beartype will iteratively do a diff
# between "Entity[Fake]" and "Entity" to find the type variables in the
# latter replaced by types in the former. Doing so then enables
# @beartype to validate that these types either do or do not satisfy
# the contravariance or covariance of these type variables.
#
# Chortle with glee as @beartype does something.
MyUsableFakeEntity = Annotated[Entity[Fake], IsParametrization[Entity]] BearTypeable: We Go Where We Shouldn'tIn the absence of collective sanity, a hypothetical If your first-draft stab in the darkness successfully results in a wet, meaty sound indicating that something unmentionable was hit and is now pathetically bleeding out on the dungeon floor, perhaps we could begin running the PR gauntlet with... something. Since your galactic-tier intelligence clearly exceeds that of my own, I leave everything in your capable clutches. Treat @beartype gently. It is tired and getting old.
...actually, your wise words make me reconsider that risky ploy. Let's perhaps ignore Typing-sig for the moment. Official Python devs frighten me. It's a rough crowd and I'm kinda too sleepy to defend myself in a heated scrum of fifty brawling typing purists. They usually see runtime as an afterthought. That's an uphill dogpile. Cue Sisyphus and his rolling rock.
Yes, yes, yes! By all the ancient leviathans that plumb the empty depths of space, yes! There are white-knight humans and there are bad-seed humans. The white-knight humans replicate the plucky happy-go-lucky Star Trek Federation. The bad-seed humans replicate the disgustingly "so bad they're good" Terran Empire from the Star Trek mirror universe. Either way, you really can't go wrong with any species. It's Stellaris, after all – the impossibly complex 4X you never quite understand where mechanical victory is secondary only to your having nebulous fun while role-playing out the vicious childhood fantasies of galactic domination you always knew was your rightful inheritance.
That... may not happen. Thankfully, the joy of Stellaris is learning the joy of Stellaris while failing your homeworld's citizenry in a nuclear conflagration of forced assimilation at the underhanded probes of the nearby machine culture you thought you could trust. You were wrong. Specifically, I advise while stroking my suspicious goatee:
|
@tbsexton Are you running a prerelease version of @beartype? I read this thread and was surprised to see this I assume you've installed from I'm just curious because I currently use Somewhat along the lines of covariant v. contravariant generics, I'm curious if there will ever be a flag-type-thing for strictly checking not-necessarily-generics, i.e. something that behaves like Edit. Actually, now that I think about it, there's already a pretty good way to do this. Namely to define something like: class Str(str):
"""A parsed string value.""" and then box the parsed |
@langfield So you're right, they aren't (yet) deeply typechecked in the released version (though this info is becoming out of date rapidly, I belive). BUT I discovered that the DOOR api actually does deeply typecheck comparable As for your question about
Other great reading for the kinds of things you'd be interested is from a fantastic dev of the
As an aside here, I love to see a Lark person in the wild! I spent a lot of time digging into the parsley library recently, but I almost went the Lark route and read a lot of the documentation 😅. If you're looking for something like NamedTuples but catered toward ADTs and immutability/memory usage, please please please check out coconut-lang! I love coconut so much. The documentation mentions their custom
I had way more fun writing my parser in coconut with pattern matching and ADTs than I did with plain python! Lastly, you said
And go on to do a wrapper class. There's a couple options here, but the core is to make use of predicates on that same wrapped class you show.
|
This is super helpful to know! I bet
Wow, this looks sweet! I'll be trying this out soon.
Neat stuff! Yes I suppose I have become a Lark person, but under duress. I'd really rather be known as an attoparsec person, lol. I've been looking into trying to get a lot of what I'm missing from Haskell in Python. Unfortunately, I think something that compiles to python is just a bit too far away for me. I've been looking at using |
...ohnoes. So sorry about that, @langfield! Everything's mostly ready to go for Sweat is beading my bald head over here. 😓
This is the way, because Parser Expression Grammars (PEGs) are the way. I'm a simple parsing man. I see PEGs. I star on GitHub. Technically, there is one well-known CFG that has no equivalent PEG. Pragmatically, PEGs can do everything and more (and more importantly, much faster) than CFGs. There is a reason Guido transitioned Python to a PEG-based parser. Packrat parsing for life! Flex that determinism, folks. 💪
What is this sanity-shredding oblivion that I see: "Coconut provides a recursive decorator to perform tail recursion optimization on a function written in a tail-recursive style..." wut It's tail recursion in Python, everybody! The prophesied Golden Age has finally arrived.
Gah! Please someone: laboriously crawl over the Thanks for the thrilling discourse that is opening my eyes to a whole new typing world, @tbsexton and @langfield. @beartype bros the best bros. 🫂 |
👋 The requirements you mention in this thread, ie compatibility with both static and runtime checkers is exactly what cornered me into the design of phantom-types. I've written a blog post explaining how the core of phantom-types work, if you want to dig into the details: https://www.agest.am/phantom-types-in-python The real implementation is just a generalization of the technique described there. |
Hey @antonagestam! Incredible project! I've really never seen anything like it. I've got a question on an example:
So I imagine that if we call |
@langfield The phantom type doesn't do anything magical to the function signature that it is used in, so it won't make any runtime errors happen for calls to the def fn(v: int) -> None: ...
fn("foo") ... neither will this. def fn(name: Name) -> None: ...
fn("not a name") However, if you combine it with a runtime type checker, like beartype, you would see a runtime error, i.e. like the invocation in this example below. greet = beartype(greet)
greet("not a name") # <-- runtime error
greet("Joe") # <-- no runtime error Just like you mention though, calling name = "Joe"
# Even though "Joe" is a valid value, the type checker hasn't
# been presented with proof to back that claim yet, and so infers
# just `str` for name at this point. This call gives a static type
# checker error.
greet(name)
# Now we're presenting proof. mypy understands that the program
# cannot possibly continue unless name is a Name, and so happily
# narrows name from str to Name for any line of code following
# this assertion.
assert isinstance(name, Name)
# And so, with the presented proof, the type checker finds this
# call valid.
greet(name) So that's the trade-off really, the burden to prove validity is pushed to the call site. However, because Python also has support for So we have a set of values that the input must adhere to, we can change so that we define those as a from typing import Literal
LiteralName = Literal["Joe", "Jane"] Now we can update the definition of from typing import get_args, Literal, TypeAlias
from phantom import Phantom
from phantom.predicates.collection import contained
LiteralName = Literal["Joe", "Jane"]
class ParsedName(
str,
Phantom,
predicate=contained(get_args(LiteralName)),
):
...
Name: TypeAlias = LiteralName | ParsedName What do we end up? There are good things and slightly less good things. The cool thing is, mypy now understands which literals are valid def greet(name: Name) -> ...: ...
greet("Joe") # valid!
greet("Jane") # valid!
greet("who?") # not valid! The slightly less bad thing is that def greet(name: Name) -> ...: ...
val = read_from_somewhere()
assert isinstance(val, ParsedName)
# or
val = ParsedName.parse(read_from_somewhere())
# this would pass with one of the two proofs above
greet(val) I do believe that Pydantic would be able to figure out usage of the union though, to be honest I'm not sure if it'd work with beartype, but I think it should? So if your source of parsed values is a typing-compatible validation framework like Pydantic, you'd likely not ever have to use explicitly use the underlying phantom type. In the library, the I guess this was sort of off-topic, hope it's at least tangentially relevant for this discussion ;) |
Apologies, yes! Makes sense. I meant with the use of @beartype. My bad entirely.
It will work with
I do think @leycec supports this currently.
No, no, I think it's fair to say we're all pretty deeply interested in this stuff! Thanks for the exposition! 😁 |
Fascinating discussion continues fascinating. Thankfully, @beartype has everyone covered here; we deeply type-check arbitrary combinations of both I'm also crossing my age-wizened fingers behind my back, which now itches suspiciously.
|
This is very cool. @leycec I feel like everyone's use of Which got me thinking... If I'm understanding the beartype so? Well...could we hack together a true sum type that MyPy, phantom-types, etc. could understand, by proxying a |
So there I was, happily humming a tune while beartype slays the typing demons of type-tetris' past... and, suddenly:
OK, now add some spice...
and test them all:
(True, False, True, False, False)
... wait a minute...?
Obviously without the
contravariant=True
I get aTrue, False
, as expected. But in my case, entities are just consumers of their datatype, like "tagging protocols". So if data iterable type B is a subclass of iterable type A, and I can tag arbitrary iterables withEntityA
, and only special Fake iterables withEntityB
, EntityA should be allowed anywhere EntityB is expected (EntityA is a subtype of EntityB).All this is to say, I did a quick
ctrl+F
on that glorious readme of yours, and lo-and-behold, contravariant is mentioned... in the table as "not supported"! 😅 And... I didn't see any open issues for the feature request. If this isn't a good place for that, let me know!The text was updated successfully, but these errors were encountered: