I agree that you can probably do that with dependent-types, I am just wondering if there is a way to do stuff like that in more simpler formalism, similar to untyped lambda calculus.<p>I mean, in untyped lambda calculus you start with simple objects that are fully specified and you compose them to get more complex objects. I think one should be able to do the &quot;opposite&quot; thing, i.e. start with potentially complicated objects and restrict those down by adding relational conditions on them.<p>So I am looking for some (minimalistic) formalism to do that, something like &quot;lambda calculus in reverse&quot;. In classic Lisp, there were operators CAR, CDR and EQ which let you introspect any lambda expression. So maybe there should exist a formalism having these decompositional operators as primitives..