.png)
2 weeks ago
6
TLDR. Types are basically sets. Why not python sets?
I enjoy mixing the sacred and the profane. Making a python model clarifies complex topics for me and gives me something to do. The core intuition often comes from finitary computable examples.
As in any sound-ish model, anything you can prove in dependent type theory (DTT) ought to be true here, but some things that are true here are not provable in weak versions of DTT because there are other kinds of models in which they do not hold.
I can see a theme with what I have done here and in the past. Other examples of me attempting a related kind of thing.
- https://www.philipzucker.com/finiteset/ modelling some basic definitions using nested frozensets. This post is particularly modelled after that one
- https://www.philipzucker.com/computational-category-theory-in-python-i-dictionaries-for-finset/ making a class to model categorical formulation of finite sets
- https://www.philipzucker.com/a-short-skinny-on-relations-towards-the-algebra-of-programming/ algebra of programming / relation algebra using finite sets in haskell
Try this notebook yourself in colab https://colab.research.google.com/github/philzook58/philzook58.github.io/blob/master/pynb/2025-05-19-frozenset_dtt.ipynb
While one may want to map dependent types into python types, the python type system is awkward, isn’t that rich, and most importantly opens the door to considering objects that are too big to actually conclusively analyze and understand. A much simpler thing to attempt do is map dependent types into python sets, specifically frozensets.
The base sets are pretty straightforward
Note because I have made the choice of being extremely finite, I can’t make a frozenset of all int. What I can do make finite sets of ranges of ints. The parameter n is a meta parameter. This does evoke the dependent type Fin https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Fin but maybe it isn’t really because I can’t internalize int.
A hallmark of Martin-Lof type theory is that it has a couple different judgements https://ncatlab.org/nlab/show/judgment .
- $\vdash A \ type$ — A is a type
- $\vdash t : A$ — t has the type A
- $\vdash A \equiv B$ — type A is equal to type B definitionally
- $\vdash x \equiv y : A$ — x and y are definitionally equal terms of type A
These judgements can be mapped to python functions that check that they hold in the model. The claim of soundness of my model says that if you can derive the judgements syntactically using the appropriate inference rules, these python functions ought to return True.
Two canonical things you want to talk about in type theory are dependent sum $\sum$ and dependent function $\Pi$ types.
To build these things, you want the notion of a family of sets https://en.wikipedia.org/wiki/Family_of_sets, aka a function that returns a set. “Type family” has a connotation of type theory, but it is also a perfectly valid topic in ordinary set theory as merely an indexed family of sets. You may want to union, intersect, or cartesian product over this family. See Halmos Naive Set Theory Chapter 9 for example.
In terms of python, I remain a little confused on what is the right thing to do, but I chose to use python functions to describe my notion of Family. I think maybe a family is any python expression that uses variables into context to build a frozenset, which is related but a little different.
The dependent aspect of this dependent type can be clearly see in B(a). While dependent types may sound exotic, a python function that returns a set is not exotic. It is also not exotic to have nested for loops where the thing you search over has a dependency on the previous for loop parameters. One place this shows up is as a way to implement obvious pruning in a naive loop based brute force search.
Pair is the the version of this that doesn’t use the dependency
For dependent functions, we want to build a frozenset of something “functionlike”. Dictionaries are basically functions with foo(bar) replace with foo[bar]. You can do this as long as the function has finite domain, which we do here.
While frozenset is a python built in, frozendict is not. There is a library though https://pypi.org/project/frozendict/ . The reason I need frozen versions I because I want to hash these things and make them keys and elements of further dicts and sets.
The way Pi works is by selecting every possible choice for every value of the input. The fact that I use itertools.product makes sense because dependent functions are sometimes called dependent product and have a notation $\Pi_{x : A} B(x)$
Non dependent functions just throw away the argument.
We can also have sum types, which are pretty straightforward.
The dependent typing context $\Gamma$ aka telescope https://ncatlab.org/nlab/show/type+telescope is a central piece of dependent type theory. Just as the things that are types are runtime values, the things that are typing contexts are runtime environments. While I could reify it as a data structure, I actually think there is a nice shallow version of it in the form of python set comprehension notation.
The context here is somewhat identified with the python context. We can reify this python context using locals https://docs.python.org/3/library/functions.html#locals if we so choose, which is kind of an interesting feature from a PL perspective. It’s a reification that has a flavor akin to call/cc but maybe not discussed as much.
The telescoping character that the Types can depend on the previously bound variables in the telescope comes naturally with the structure of for loops. Syntactically, the order of the expressions in the comprehension is flipped compared to what is the typically convention in type theory. It looks more like A type -| Gam than Gam |- A Type
Iin other words, I am for serious interpreting the telescope context $x : A, y : B(y), z : C(x,y)$ with the python textual code for x in A for y in B(x) for z in C(x,y)
All the judgments can be extended to being hypothetical judgements by making a comprehension wrapped in an all
Vec is a common example of a dependent type.
Everything is too decidable and makes the distinction between propositional and definitional equality too hard to notice. Also it is quite extensional.
Nevertheless, we can construct a type family akin to an Identity type. https://ncatlab.org/nlab/show/subsingleton
Universes are big. They are the things that contains Types. https://ncatlab.org/nlab/show/type+universe https://en.wikipedia.org/wiki/Universe_(mathematics) https://en.wikipedia.org/wiki/Constructible_universe
Note that frozensets can’t have a set be an element of itself without trickery. So we need a universe level for that so we can quantify over types and types of types, etc. https://agda.readthedocs.io/en/latest/language/universe-levels.html https://lean-lang.org/functional_programming_in_lean/dependent-types/indices-parameters-universes.html https://en.wikipedia.org/wiki/Axiom_of_regularity https://ncatlab.org/nlab/show/axiom+of+foundation https://en.wikipedia.org/wiki/System_U https://ncatlab.org/nlab/show/Burali-Forti%27s+paradox
But also if we include all applications of Arr and Pair etc in our smallest universe, then it isn’t a finite set. So another parameter that controls the depth of applications of the constructors also seems like a reasonable thing to do.
Here is an example of a polymorphic construction. Note that in this model, we don’t have only the functions that obey parametricity. Does this mean the model is “wrong”? No, I don’t think so. It just isn’t a complete model. The properly parametric functions are going to be a subset of the things returned.
Thanks to Cody Roux and Graham Leach-Krouse for helpful discussions
Some useful resources on dependent types are
- https://arxiv.org/abs/2212.11082 Introduction to Homotopy Type Theory
- https://www.cse.chalmers.se/research/group/logic/book/book.pdf Programming in Martin-Lof ’s Type Theory
- https://www.danielgratzer.com/papers/type-theory-book.pdf
- https://homotopytypetheory.org/book/
- https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx HoTTEST Summer School 2022
- https://www.cs.uoregon.edu/research/summerschool/summer14/rwh_notes/ssdt.pdf Syntax and Semantics of Dependent Types -Martin Hofmann
- https://people.cs.nott.ac.uk/psztxa/publ/ydtm.pdf Why Dependent Types Matter
- https://www.kleene.church/tt-notes Cody’s notes
- https://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf Dependent Types at Work
Python comprehesions are modelled after set comprehensions. I think this means that has_type is something like the axiom of collection / replacement https://en.wikipedia.org/wiki/Axiom_schema_of_replacement , a connection I hadn’t ever really considered before. Telescopes are telescoped because it models the scoping structure of quantifiers.
Having a notion of execution by using generators or dictionairyes that key on which time a thing enters the set might be interesting. Maybe a more faithful model of constructive principles / enables Int.
Maybe using quoting of code / partial evaluation / bytecode normalization might be a way to get at definitional equality.
Cody pointed out that Fin is totally cursed. The parameter coming in is an int and I vaguely silently cast between int and all the versions of Fin.
Sympy, Z3, step indexing, actually using python functions as functions, hypothesis generators generate stream A and check A -> Bool pairs as types and just sort of randmize test it rather than enumerate it. Contracts.
I kept getting surprised by the stuff that is actually empty vs stuff that had non parametric solutions. Is there something interesting there?
Maybe interpret identity types into
- Code string equality
- bytecode equality
- z3 smt equality
- egraph equality
- paths in a graph
- permutations
- isomorphisms
- simplicial complexes something somethjing (simplical sets really probably)
- sympy equality (t - t1).simplify().is_zero
- proof terms from something?
- is equality
- == equality
Maybe finite models like this are useful for counterexample finding or attempting to generalize/antiunify into suggested terms. https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/mace4.html Mace4 is a cool model enumerator for first order logic
Rather than use frozendict and frozenset, using BDD like structures could be useful https://en.wikipedia.org/wiki/Binary_decision_diagram . We are kind of model checking type thoery
Subsets, proof irrelevance, predicativity, quotients
https://lawrencecpaulson.github.io/2022/02/23/Hereditarily_Finite.html https://en.wikipedia.org/wiki/Hereditarily_finite_set What I am doing is the analog of hereditarily finite set theory. Cody claims makes sense because DTT interpeters into set theory, and there are finite set models of the appropiate set theories. https://eprints.illc.uva.nl/id/eprint/1769/1/wehr.pdf https://www.sciencedirect.com/science/article/abs/pii/S0049237X0871989X The Type Theoretic Interpretation of Constructive Set Theory - Aczel. https://www.lix.polytechnique.fr/~werner/publis/tacs97.pdf Sets in Types, Types in Sets - Benjamin Werner
Classes ~ functions.
parameters vs indices. Python functions vs ?
https://golem.ph.utexas.edu/category/2022/07/identity_types_in_context.html https://cs.stackexchange.com/questions/20100/what-are-the-difference-between-and-consequences-of-using-type-parameters-and-ty https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
The fiber perspective. Hmm. If I want to be categorical about it. Actually implement telescoped substitution. But this is way more deeply embedded than what I’ve done here.
Refinement typing discipline vs dependent typing discipline. Related. What does the telescoping really achieve? Is it more or less powerful than binding all variables at once and then forall x y z, P(x,y,z), Q(x,y,z), R(x,y,z) => Foo which is more like Isabelle Pure. Triangularity is reminscent of triangular matrices but also triangular substitutions from minikanren implementations. Any connection?
Do the parametricity relational model finitely. Explain its relationshiop to information hiding of the universe and oninterference. Run a program twice on some unchanged and some changfed inpputs as a method to detect leakage. Fuzzing the universe might also work, since that can expose information hiding problems. Information hiding and staged metaprogramming also. Kind of you can’t leak information from runtime to compile time.
One way for a topic to have meaning is to explain how to map it into another thing you’re already comfortable in. For some new programming language, a way to do this is to give an interpreter of the new programming language inside a programming language you already know. An example of this in the context of a formal logic is to give a way to translate the syntax of your logic into a description of a thing metatheory you’re working in, which might be some set theory or lean or isabelle or whatever. https://plato.stanford.edu/entries/model-theory/ . You then also want to find an instance of this thing.
I’ve become used to saying the phrase “python is my metatheory”. This is true because in Knuckledragger https://github.com/philzook58/knuckledragger , I metaprogram my higher order logic in python, doing the sorts of things a metalogic does. It is also true because I only feel comfortable that a mathematical topics makes sense if I can see something to do or compute with it. A model, however janky, finitized, or lightly unsound, inside of python can help strip away a befuddling aura of mysticism around a topic. Maybe from a fancier perspective, python is an interesting dirty place to put realizability https://en.wikipedia.org/wiki/Realizability https://ncatlab.org/nlab/show/realizability models, which I think are models with a notion of computation baked in.
I can see a theme.
- https://www.philipzucker.com/finiteset/ modelling some basic definitions using nested frozensets
- https://www.philipzucker.com/computational-category-theory-in-python-i-dictionaries-for-finset/ making a class to model categorical formulation of finite sets
- https://www.philipzucker.com/a-short-skinny-on-relations-towards-the-algebra-of-programming/ algebra of programming / relation algebra using finite sets in haskell
In the typical arch of understanding , there is a naive version, then sophisticated, and then you appreciate the naive version again.
On a first pass, types are basically sets. The type int is basically interpretable as the set of all integers and the type bool -> bool is interpretable as the set of all functions from bool to bool (of which there are 2^2 = 4).
On a second pass, types aren’t sets https://dl.acm.org/doi/pdf/10.1145/512927.512938 . Sets do a bad job of explaining parametricity for example, for which a relational interpretation is more appropriate. https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf Parametricity is basically the same idea as information flow security.
On a third pass, types aren’t not sets.
Using this meme is a bit propaganda-y. It is implocitly calling you a bespectacled midwit if you think types are not sets. Maybe I’m using the wrong meme. Maybe I should use the brain exploding one? There are probably more passes beyond 3 and I think types are not sets is a perfectly valid viewpoint. Moreso than projecting this meme onto others, I mean it to explain how I currently see my own history of understanding.
Static vs dynamic. Type judgements are the string of python? x : Fin(5), y : Fin(x) |- x + y : Fin(x)
The interpretation of contexts is sets of environments.
dependency shows up naturally in the ordering of loops. what’s up with that?
Quotient / Subset
Sympy
Sympy set module seems too weak to do families. Maybe it could be extneded? https://docs.sympy.org/latest/modules/sets.html
Gassed
How to include integers? Lets everything become generators. Allow semidecidable sets. Marshall https://github.com/andrejbauer/marshall https://dl.acm.org/doi/abs/10.1145/3209108.3209193
Maybe a kripke model version with just N steps allowed. Then could index what is in set by integer is appears at. Monotonic set growth.
Z3
Z3 can describe finite sets as models. A Pi constructor akin to kd.QForAll.
Terms
I have been very vague what my allowed terms are.
https://github.com/Marco-Sulla/python-frozendict
https://en.wikipedia.org/wiki/Family_of_sets
A graph neighborhood map V -> edges
Anytihng A -> [B]
relation to the finite parametricity idea.
Internalized == frozendict Meta = python fun
Finite dependent type theory in python.
groupoid model? paths on a graph?
isomorphisms?
The is basically model checking of dependent type theory? Which is easier. We get a little bit of jimmies by fiddling with the universe.
step indexed relatiobns. Maybe there’s some way to use computation bounding to model check.
indices vs parameters and meta vs other
inference rule form vs internialize pi form of induction
quotient types extensional equality
Yes, this is a logical relation. https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf I am being vague what the actual syntactic language I’m working in. Also the caveat that everything is a frozenset before I even get to it somehow is the intution behind termination.
Another axis to finitize on ot number of computational steps allowed and to have partial functions
defaultdict can do more but still not everything. You can have a defaultdict from the integers. BDDs are interesting also but just as a compression.
are types sets? https://bsky.app/profile/hillelwayne.com/post/3lms36j275s26
Trying to make a sound model of dependent type theory If you can derive a judgement (which I am not doing) or if there is a derivation of a judgement, the corresponding python statement should return true
[[x : A]] -----> "for x in [[A]]"
Model checking dependent type theory A python frozenset model of dependent type theory
How does one build a finite model of first order logic for example
Translate |- forall x, p(x,y) into Picking p, A etc all(p(x,y) for x in A)
string codes z3 ast codes
z3 egraph somehow?
Graham suiggested “dispaly indexing”. Represent Family as it’s sigma type + a projector? https://ncatlab.org/nlab/show/displayed+category ? [for x in A for base, totpoint in B if base == x]
def ITE(A : Type, B : Type) -> Family: return frozenset({(True, A), (False, B)})
but again this is kind of a poor mans frozendict?
def ITE(A : Type, B : Type) -> Family: return frozendict({True : A, False : B})
That telescopes turn into foralls is interesting. And it does make sense from a finitrary efficiency standpoint to not do a big non dependent loop and then cut out. You want to generate only that which is obvious plausible
Z3 model. Internal SetSort() f = Function vs f = Array(“f”, , ) as internal vs external. Universes.
vs
vs
vs for x in A: if cond(x): for y in B(x): if cond2(x,y): yield yada
althouggb basically cond(x) can be fused into B by returning null iterator.
I’ve been playing the same game for so long https://www.philipzucker.com/finiteset/ https://www.philipzucker.com/a-short-skinny-on-relations-towards-the-algebra-of-programming/
hmm. Using quickcheck. That’s intriguing. hypothesis. quickcheck over different universes or interpretations.
quickcheck set theory statements too. Huh. I wonder if quickchecks in lean or quickchick have something like this
Krivine realizability models What does this say about the sympy thing. Why isn’t it working? No notion of set?
Codes and Tarski Universes
Comprehensions are modelled after set comprehensions. Are has_type judgements like set comprehensions?
|- A type is say the set exists |- t : A is like using seperation on a type that exists?. But we generate t, not cut it out. Seperation ought to look more like this. [t == x + y for x in Fin(5) for y in Fin(x) for t in Fin(5 + y) ] ?
Maybe it’s more like replacement? https://en.wikipedia.org/wiki/Axiom_schema_of_replacement predciates A -> Bool as classes. Set[A] as sets. Converting is not obvious. |- A type is more like asserting a class expression is well formed? |- t : A is using (hypothetical?) axiom of collection?
|-
https://ncatlab.org/nlab/show/Tarski+universe You have |- T : type and then |- t : El(T) T is code
Cody points out Fin is an abomination because it takes Fin as a parameter. But it always terminates at meta Nat.
families could be codes of families?
El family is a meta function. is it eval? And codes = str
https://okmij.org/ftp/Haskell/TypeClass.html#Haskell1 only 1 typeclass Oleg
vytecode equality as definitional equality. A little strong than string equality of code. Would normalize withspace, parens. But also maybe names? Maybe not https://arxiv.org/abs/1805.08106 The sufficiently smart compiler is a theorem prover https://dl.acm.org/doi/10.1145/3611643.3616357 Speeding up SMT Solving via Compiler Optimization
I could do fstring stuff to partially eval. `lam(lambda xlambda x: f”{x}” == lambda y:
Code string equality bytecode equality z3 smt equality egraph equality paths in a graph permutations simplicial complexes something somethjing (simplical sets really probably) sympy equality (t - t1).simplify().is_zero proof terms from something? is equality == equality
