24 Jan
2009
24 Jan
'09
5:42 p.m.
On 25 Jan 2009, at 00:11, Thomas Davie wrote:
I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.
Note that we can't possibly know what information can we possibly know about a value being given it's type. For example, you can prove that the only "reasonable" value of type (forall a. a -> a) is (id); so, from you POV, (_|_) :: forall a. a -> a is equal to (id). This means, that ((_|_) :: forall a. a -> a) 1 = 1 instead of (_|_). But there is no way for a compiler to deduce all the equalities of this kind.