I recently had the insight- surely induced by reading something on HN or listening to some podcast- that types are simply functions from the set of all possible "values" to a logical value...
Yeah, a type is really just a set (in the mathematical sense). And a set can be defined by a function to {0, 1}. I don’t know if this function has a formal name, byt you can think of it as a “is this value a member of the set?” function.