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

_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to