The online hangout for Göteborg Functional Programming Group and everybody interested.

@Jell I stumbled into linear logic. It seems like it could be interesting also from a non-applied perspective (such as "only use once" type system).

@jolod I personally got lost in a new sea of uncertainty after reflecting on "all the possible ways to handle division by zero". Ended up looking at Liquid Haskell and SMT https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

but still only see 4 ways: a partial solution that raises an exception (which give you the locality of the error), a Maybe that makes you wrap stuff in monads (loses the "locality" of the error, but makes it "noisy" / visible), using NaN which absorbs the error, or carrying proofs that you never divide by zero

my understanding of Liquid Haskell is that pretty much like you can do in Idris, you carry the proof that things are not zero (reading up on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18/refinement-reflection.lhs/)

Idris actually offers: a partial implementation with

`div : Nat -> Nat`

that raises error, a total implementation that requires you to carry a proof with `divNatNZ`

, and an "absorbing" version for doubles with `/`

If you're up for it, I think we should have a meetup presentation centered not about Idris or LiquidHaskell in particular, but about the problem/solution space in general.

so to be clear on the above, you get this for doubles in Idris:

```
λΠ> 1.0 / 0.0
Infinity : Double
```

```
λΠ> 0.0 / 0.0
NaN : Double
```

If infinity is involved, do you have different cardinalities as wel? ;-)

```
λΠ> :type Type
Type : Type 1
```

and I think Type 1 is of type Type 2

(if that's the question? :p)

but I suspect that was not the question

I should stop asking questions about Idris since I don't understand the answers. :-)

... and just learn some Idris already!

hum you not understanding my answers is probably me not understanding them enough to carry them clearly

I understood your question about cardinality to mean "can one express in Idris that one type (set) is bigger than the other"

as in: can I say "I want Nat + Infinity"

but also yeah, learning Idris is fun.

but what my thought led me to is: is there a point in having a

`Num -> Num -> Maybe Num`

instead of having a num with a built-in representation of NaN and Infinity?
it seems that the only reason would be purity, and the possibility to declare a function undefined on a particular domain

so I guess having a Maybe Num is a way to say "this particular function is partially defined"

but if you use Maybe, then any arithmetic code would either have to be tainted by partial

Or you use a default value. Which you would do anyway, if you actually wanted the value.

or absorb / correct the error somewhere silently by overriding the undefined place

yes

so what's the difference between that and NaN in that particular case?

So you could display

`show rating`

to the user, which might see "NaN", instead of "Be the first to rate this product."
With NaN being part of the type, you must remember to check against NaN yourself.

If you have a list of ratings, you'd naturally get

`Maybe Number`

. But if you have a number `totalScore`

and `numberOfRatings`

you wouldn't.
Unless you use some

`safeDiv`

function.
I still wonder why both Haskell and Idris chose to use NaN and Infinity

If you add Infinity, which is nice, you need to add NaN, which is not nice.

Cauchy would agree with me on that

but he'd argue that lim n->0, n<0 of 1 / n is -Infinity right?

All calculations should be indeterministic.

Or, there should be no zero.

Only zero+ and zero-

Or, there should be zero+ and zero- and zero, where division by zero is Nan, but division by zero+ and zero- is pos infinity and neg infinity.

division is simply not defined for 0

it's defined asymptotically around zero

I think when talking about generalized natural numbers (i.e. positive natural numbers including zero and infinity) you can consider 1 / 0 = Infinity

Perhaps it's best then to use Maybe, and have your own richer type that has infinity. DoublePlus = Double Double | PositiveInfinity | NegativeInfinity.

And then you need to do

`fromMaybe PositiveInfinity (x / y)`

.
No, wait.

Or yes.

jolod @jolod is tired and confused.

Or do

`fromMaybe PositiveInfinity $ map Double $ (x / y)`

if x and y are plain numbers.
where

`(/) :: Double -> Double -> Maybe Double`

.
I think I prefer (/) to throw an exception over NaN being a valid number.

And if I want to handle NaNs, I prefer Maybes.

Because if I get an exception when I used (/) because I thought it was indeed safe, my logic was flawed anyway, and there's no point in using Maybe because I cannot recover.

I like the Idris "provide a proof" approach that lets you think about it and you can provide a bogus proof if you can't actually prove it, but the issue with that approach in idris is that if your bogus proof is wrong and you indeed call with zero I'm pretty sure you segfault which is way worse that a typical runtime error

I want my runtime error to have a stack trace :p

not sure how I feel about the NaN vs Maybe, for sure for exploratory stuff you want NaN right?

especially if you're dealing with some kind of dataset with missing data

Usually when I have gaps in data and I have NaN instead, e.g. in a time series, then I filter on finite anyway. I can just as well filter or Just.

`filterMap id`

in PureScript.
which is just more typing / overhead when exploring

unless you have a super neat typeclass algebra that lets you

`+ : Maybe a -> Maybe a -> Maybe a`

which, come to think of it...

is pretty much NaN

also yeah you lose the "reminder"

like if you're exploring and you don't mind the NaN have a constant reminder has to be a downside

as in, the reason to have a Maybe is to nag you about the fact that it's not defined

And those would be the Maybe versions. I've thought about that.

in the exploratory case where you tell yourself "I don't mind about the undefined bits" having the feature of "please keep nagging me about the undefined bits" has to stand in the way :p

Yeah, but using +' makes it not stand in the way, but it's still there.

yeah why not. Perhaps with a different prelude even then?

but then all your custom functions still need to deal with the Maybe

They can coexist, so it's no problem. And easy to write.

`plusPrime = map (+)`

.
Yeah, but that's when you want the maybes.

Like you don't want to take NaN numbers from a list.

But when doing the arithmetic you don't care about the NaN (perhaps).

No need to use +'.

if the division returns a Maybe?

Now, don't use +'.

Instead, use +? for type Number -> Maybe Number -> Maybe Number. Use ?+ for Maybe Number -> Number -> Maybe Number. And ?+? for Maybe Number -> Maybe Number -> Maybe Number.

convenient!!

who said lenses?

But honestly, wouldn't that work? The question mark is great way to say maybe.

with all those implementations?

You only need ?+? and you can use Just on the correct side to have the rest.

(+?) x y = Just x ?+? y

Or yes, that's what you meant.

I think that

`score /? count`

is pretty nice.
so Haskell doesn't let you

`take (1 / 0)`

because the numeric tower in Haskell makes it not an Int
OK, so when would your numbers, that involve NaN, interact with the "outside" in a meaningful way?

I think in that case basically only when casting them or representing them

showNumber being

`Number -> Maybe String`

??? :p
yeah if you

`show $ showNumber`

then you say you want to print Nothing :p
Yeah, so that would be super annoying, because you would not be able to have data showable if it has numbers in them.

Still annoying.

jolod @jolod off.