[Haskell-cafe] bottomless Top?

[Conor McBride]

On 16 May 2008, at 01:13, Jonathan Cast wrote:

> On 15 May 2008, at 4:29 AM, Conor McBride wrote:
>
>> Replying slap-foreheadedly to own post...
>>
>> On 15 May 2008, at 11:56, Conor McBride wrote:
>>
>>> Folks
>>>
>>> I'm also wondering whether it makes sense to have a
>>> "bottomless Top" type, with constructor _ and lazy pattern _
>>> (with (undefined :: Top) equal to _). Then the constant-time
>>> shape operator makes the same sort of sense as the
>>> constant-time
>>>
>>>   inflate :: Functor f => f Zero -> f a
>>
>> We've got it already.
>>
>> data One
>>
>> would do, with smart constructor
>>
>> only :: One
>> only = undefined
>
> As I've mentioned before, my favorite data type
>
> newtype One = One One
>
> does the same, and stays in Haskell 98.

That's rather fun. On the face of it, it looks
peculiar that

*Top> case undefined of One _ -> True
True

until you put your newtype constructor sunglasses
on. Funny that newtype constructors really are like
id until you fmap them. Or is that optimized away
these days?


>   (And has the same weakness to seq: (`seq` ()) is perfectly strict  
> (it's const undefined)).

Oh boooo! I'd forgotten that seq lets you look at
an undefined thing just enough to go wrong.

It'd be lovely to have proper unit and product,
with their eta-laws, compiling pattern matching
to projection. Was it so bad to distingush the
value types at which seq could be applied?

Meanwhile, the game's up for the unsafeCoerce
dodge:

*Top> shape ['m', undefined, 'o']
[(),*** Exception: Prelude.undefined

I knew it was too good to be true. Like Randy
Pollack says, the best thing about working in
strongly normalizing languages is not having
to normalize things. Loose morals are neither
fast nor correct. I'd better crawl back under
my rock.

All the best

Conor