Hi, I'm reading a book where the guy (Abraham Robinson, "Non-Standard Analysis") write a type system like following for his needs. First, he gets an initial type: 0 This is going to be the type of all individuals. Then, types of relations (sets, functions etc.) are built like this: given existing types, a n-uple of them is a new type. So, these are possible types: (0) ((0),0,0) (0,0,0) ( ((0),0,0) , 0 , 0 , (0,0,0) ) I think it's easy, and similar to above, to do that for Haskell kinds. Would it be possible to do something similar for haskell types? If possible, I think that it could be a great help in understanding Haskell type system, specially new things like GADTs and RankN types. Thanks, Maurício