> When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". I like analogies, but I

> When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". I like analogies, but I don't think bringing the real world into this helps – irl, "is a" relationships are pretty fuzzy and arbitrary. What does it mean for something to "be" a door? If I'm using a window as a door, does it become a door? "Being a door" is just another property. And if I have a door and start chopping away pieces of it, at what point does it stop being a door? "things" often don't have well defined boundaries, so even the notion of "objects" becomes meaningless. (see also: Ship of Theseus). A lot of it is up to a person's perception too... So in general, I think it's better to keep the real world separate from formal/mathematical concepts. --- Encoding some "properties" in the type system is a tool for ensuring (some degree of) correctness. Sometimes, a property is important enough that you want to put it in a type variable, as in `data Connection (status :: ConnectionStatus)`. But if you'd prefer your properties to be "disconnected" from the actual type, you might enjoy dependently typed languages[1] like Idris, where you can have statically enforced "proofs" that a value has some property. In such a system, a function `readData` could take a `Connection` and a proof that the connection is open. It'd look something like this: readData : (conn: Connection) -> IsOpen conn -> Bytes Note that the proof, `IsOpen conn`, refers to the value of the first argument. How do we obtain those proofs is up to the connection library. For example, `openConnection` could return a connection along with a proof that the connection is open: openConnection : Address -> ((conn: Connection), IsOpen conn) The library could also supply a "smart predicate" function that gives you proofs of a connection's status: status : (conn: Connection) -> Either (IsOpen conn) (IsClosed conn) Take this with a grain of salt though – I haven't actually used Idris, just read a few tutorials.