In retrospect, was burning bridges a mistake?

[atravers]

@dixonary

To make division into a function, we can either exclude (x,0) from the domain […]

newtype NonZero a = NonZero a

(/) :: Fractional a => a -> NonZero a -> a
(/) x y = ...

unitNonZero :: Num a => a -> NonZero a
unitNonZero x | x /= 0 = NonZero x

bindNonZero :: Num a => NonZero a -> (a -> NonZero b) -> NonZero b
bindNonZero (NonZero x) k = k x

@dixonary

[…] or make the codomain a union of the reals with a singleton of some sentinel value indicating failure (e.g. { ⊥ } ).

divide :: Natural -> Natural -> Natural
divide x y | x < y = 0
           | otherwise = 1 + divide (x - y) y

divide x 0 = (\ y -> 1 + divide (x - y) y) 0  {- x >= y -}
           = 1 + divide (x - 0) 0)            {- application -}
           = 1 + divide x 0                   {- (-) identity -}
           = 1 + ⊥                            {- (divide x 0) regresses infinitely -}
           = ⊥                                {- (+) strict -}

…hence you either accept that division can fail:

(/) :: Fractional a => a -> a -> a

…or you make it annoyingly explicit that it doesn’t:

• (/) :: Fractional a => a -> NonZero a -> a
  

• (/) :: Fractional a => a -> a -> Maybe a
  

That would have been an interesting experience to rewrite everything in Haskell which relies on division to use the more explicit style for use in that course - the students must have been very impressed!

---

This is off topic though, so I’d recommend we don’t go on about it.

Agreed.