What are types anyway? For the Cish person, the "type" tells you basically how many bytes there are in a thing. That's not very satisfying. Another take is that a type is sort of the collection of things that satisfies a predicate, which leads to computability and contradiction questions. Somehow I feel systems with a principal type property find a sweet spot. A principal type captures some real abstraction from the details of a program.

It's this a logic programming question? 🤗

I was going to bring it back around to unification and cut, but I had dug myself a deep enough hole, so I went right on to abort.

i think of types as macros, but maybe not in the usual sense. constraining a piece of data is exactly as much “programming” as assigning that piece of data. to get zen: is slicing the bread part of making the sandwich, even if a machine has done it before you got there? i think: yes.

Types are shapes: that pre and post select by arbitrary boundaries around your domain and codomain. They can be thought of as composition of logic operations but in the orthogonal direction.

wikipedia to the rescue: "a type system is a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program, such as variables, expressions, functions or modules.[1] These types formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components (e.g. "string", "array of float", "function returning boolean")"

By Steve: https://medium.com/@stevekrouse/types-are-shapes-d6af1e83192f But I mean in a more rigorous / mathemarical way. They can be modelled to map to topological spaces and I think each individual type is a kind of container for the logical content / information to flow through.

For an explicit link between types and logic programming, see the Shen language. It's a dialect of Lisp with optional type checking. And it comes with a built-in Prolog-like sublanguage for writing type checkers. There is a default type checker of course, but my understanding is that you could replace it with your own (I didn't try). Types can thus be defined by a wide range of predicates.

shen is really cool! here’s a video on it: