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