Bottom Type--Type Theory

[Johannes Loher]

Am 17.01.19 um 01:41 schrieb Jonathan Marler:
> 
> A good summary of the issues with void. Maybe adding a bottom type
> enables some new clever semantics, but I would venture to guess that
> adding a real unit type would be even more helpful than a bottom type.
> I've had cases where being able to use void as a function parameter or a
> field would have made some of my templates much cleaner. Maybe we should
> focus on making void a real unit type before we try to add a bottom type?

I totally agree with this. I would love to see void becomming a real
unit type!

I have already tripped over the fact that void is not a proper unit type
several times. It makes generic function composition (and other generic
constructions) so much more annoying: You always need to treat void as a
special case.