The difference between set theory and type theory: there is set intersection but no type intersection. It makes no sense to ask for ints that are also bools.
Show this thread
Types are sets of the (provable) properties of their inhabitants, and we can do set operations on these properties. If we think of subtypes as supersets of properties, a union of properties is, in general, some intersection of the type inhabitants. #duality
-
-
The idea is that you can't define a variable without specifying its type x:T. It can't exist outside of its type. An element of a set can, so it can be a member of two sets at once. If you want to pass x to f:U->V, there has to be a coercion T->U. It doesn't mean x is of type U.
-
We can't define a variable without its type in Church systems only. In Curry systems we can: (\x -> x) :: a -> a and (\x -> x) :: (a -> a) -> a -> a etc... id is inhabitant of both types.
- Show replies
New conversation -
-
-
Some viewpoints would describe them as categorical in the sense that there's an adjunction or equivalence between a cat and a TT, or as synthetic objects like in HoTT. Haskell's types, for instance, are only superficially set like, but this breaks down. https://ncatlab.org/nlab/show/type+theory …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.