9 Jun
2003
9 Jun
'03
9:18 a.m.
On Thu, 5 Jun 2003, Thomas Streicher wrote:
Hi Paul,
"The neglect of sum types is the root of all evil."
To some extent this may be true for programming languages (but see recent work of Jim Laird). For logics it is less clear. Actually you mean the empty type, isn't it?
which is the n=0 instance of the n-ary sum connective. So it should be included in even the simply typed setting. Paul
Moreover, sunset types are slightly heavier than ordinary sum types. Subset types are rather dependent sum types.