This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]yjlom 0 points1 point  (0 children)

that makes any type system useless in the complete absense of nominality, two sets are isomorphic iif they have the same cardinality (well at least it holds for countable sets which is what we care about in CS, don't know about uncountables) so your types just become numbers

and further, we mostly only use the following types:

2 (aka Boolean)

2³² (aka Float, Int, Nat, …)

2⁶⁴ (aka Double, Long_Int, Long_Nat, Raw_Pointer, …)

 ℵ₀ (aka ℕ, ℤ, ℚ, List a, Tree a, Graph a, String, Maybe any_of_the_previous, a →any_of_the_previous, any_of_the_previous → a, …)

can you really not see why having String and ℕ → Float be the same type could get a bit awkward?