[HN Gopher] Representing Type Lattices Compactly
___________________________________________________________________
Representing Type Lattices Compactly
Author : tekknolagi
Score : 74 points
Date : 2025-03-11 12:50 UTC (10 hours ago)
(HTM) web link (bernsteinbear.com)
(TXT) w3m dump (bernsteinbear.com)
| noelwelsh wrote:
| No parametric polymorphism aka generic types?
| tekknolagi wrote:
| It's in the context of a Python JIT, where we're looking for a
| different kind of type information
| abeppu wrote:
| JIT internals are very much not my area so this might be an
| ignorant question but ... why doesn't the parametric issue
| come up in this context? The author starts with the example
| of a value which could be a List or a String, where the code
| calls for its `len`. But one could also need to reason about
| `x: list[list[str]] | list[str]` and where we'll do `y =
| len(x[0]) if len(x) > 0 else -1` which requires the system to
| be able to represent both the type of x and x[0] right?
| deredede wrote:
| You typically don't represent that information in the type
| of the object itself but rather as separate information for
| the type of the values (ie fields). So maybe it's "a list,
| and also the values are lists" or maybe it's "a list, and
| also the first value is a string, and the other values are
| integers"... and maybe it's "a list, and the values are
| strings, and also it has a field named 'foo' that's an
| integer for some reason".
|
| You can still have the same information (depending on the
| actual system), just represented differently - parametric
| polymorphism is a bit too rigid here because not everything
| fits neatly into generic schemas.
| tekknolagi wrote:
| And another bit of info: it's _much_ harder to reliably
| track that, because as soon as the list (for example)
| escapes, its elements could have any type and it could be
| any size. PyPy has storage strategies and speculative
| typing (with guards and deoptimization) that help with
| this kind of thing.
| choeger wrote:
| There's little value for parametric polymorphism at this level
| as it requires parameters (not only type parameters, but also
| value parameters, as otherwise the type parameter are
| dangling).
|
| It's better to think of these types as different. Maybe
| "primitive types" or "shapes".
| nsajko wrote:
| Julia does this for parametric types, too.
| infogulch wrote:
| This seems similar to the way CUE type lattices work.
| https://cuelang.org/docs/concept/the-logic-of-cue/#the-value...
| PhilipRoman wrote:
| wow I guess great minds really do think alike, I did almost the
| same exact thing a few years ago, but eventually gave up as my
| type hierarchy grew too complex.
|
| You could probably represent a lot more complex relations with
| similar strategies by adding one or two cleanup instructions to
| union/intersection operations, but whenever I've tried to do it,
| my head gets dizzy from all the possibilities. And so far I've
| been unable to find software that can assist in generating such
| functions.
| sparkie wrote:
| One possible trick for unions is to use bloom filters,
| providing you have some way of hashing types. If you create a
| bloom filter `Bloom(t1, t2)`, it's the same as doing `Bloom(t1)
| | Bloom(t2)`, where `|` is just bitwise-OR.
|
| Obviously not perfect as it can produce false positives, but if
| we keep a filter of sufficient size, this will be low, and
| still be more space-efficient than keeping a bit per type in a
| large type hierarchy.
|
| Intersections can also be done, but with a potentially higher
| false-positive rate. The result of `Bloom(t1, t2)` has _at
| least_ the bits set by `Bloom(t1) & Bloom(t2)`.
| recursive wrote:
| I don't think space is going to be the first issue that
| causes this to fall. It will probably be the human mind's
| ability to conceptualize the space.
| pjs_ wrote:
| Come on man just do duck typing. You are killing me with this
| stuff.
|
| It all reads so technical and long and mathematically academic
| but it's just a bit mask.
|
| I absolutely hate writing python now because I have to reason
| about a "list of list of errors" type defined by a teenager and
| they get mad at me if I don't then define a new "list of list of
| errors, or none" type when I manipulate it. You guys are now
| employed by VSCode to make those hints look beautiful. VSCode is
| your boss now and your job is to make VSCode happy
|
| I predict that in five years we will retvrn to duck typing in the
| same way that we are now retvrning to server side rendering and
| running on bare metal. Looking forward to the viral "you don't
| need compound types" post on here. "Amazing - you can write code
| which does normal business tasks without learning or ever
| thinking about homotopy type theory"
|
| Yes I get it if we are writing embedded code or navigation
| systems or graphics or whatever, please help yourself from the
| types bucket. Go ahead and define a dictionary of lists where one
| list can contain strings but all the other lists either contain
| 8-bit integers or None. But the academic cachet of insanely
| complex composable type systems bleeds through into a web server
| that renders a little more than "hello world" and it ruins my
| life
| tekknolagi wrote:
| This is not about surface level typing. This is about compiler
| internals.
| tekknolagi wrote:
| I added a couple of sentences in the intro to clarify.
| Dr_Incelheimer wrote:
| >filtered by Python types
|
| lmaooo sub-2s golem detected
| __MatrixMan__ wrote:
| I don't think there will be a movement away from type hints in
| python any time soon, they're too useful as guardrails for an
| LLM. But even without using an LLM I'm definitely faster with
| type hints enforced because I can just sort of feel around with
| autocomplete. Sure, the transition sucks, but once you're there
| the benefits start stacking up pretty fast.
| pizlonator wrote:
| Looks almost exactly like what JavaScriptCore calls
| SpeculatedType.
| tekknolagi wrote:
| Excellent, thanks for the pointer. Mentioned!
| mncharity wrote:
| OT, I'm _so very_ looking forward to some language supporting a
| pushout (path independent) lattice of theories (types, operators,
| laws). So abstraction has math-like locality and composability
| and robustness.
| IsTom wrote:
| This is also how Erlang's Dialyzer works.
| tekknolagi wrote:
| Have a link to the implementation?
___________________________________________________________________
(page generated 2025-03-11 23:01 UTC)