These are chat archives for got-lambda/expression

28th
Jan 2018
jolod
@jolod
Jan 28 2018 13:56
@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).
Jean-Louis Giordano
@Jell
Jan 28 2018 15:50
@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/)
Jean-Louis Giordano
@Jell
Jan 28 2018 15:57
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 /
jolod
@jolod
Jan 28 2018 15:57
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 15:58
yes that would be cool
jolod
@jolod
Jan 28 2018 15:58
(Obviously with examples from LH and Idris. :-))
Jean-Louis Giordano
@Jell
Jan 28 2018 16:00
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
jolod
@jolod
Jan 28 2018 16:01
If infinity is involved, do you have different cardinalities as wel? ;-)
Jean-Louis Giordano
@Jell
Jan 28 2018 16:02
I think so actually? :p
λΠ> :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
jolod
@jolod
Jan 28 2018 16:06
I should stop asking questions about Idris since I don't understand the answers. :-)
... and just learn some Idris already!
Jean-Louis Giordano
@Jell
Jan 28 2018 16:06
hum you not understanding my answers is probably me not understanding them enough to carry them clearly
jolod
@jolod
Jan 28 2018 16:07
Nah, the problem is that I don't know the second thing about Idris.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:07
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:13
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"
jolod
@jolod
Jan 28 2018 16:16
Yeah. Maybe means partial.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:17
but if you use Maybe, then any arithmetic code would either have to be tainted by partial
jolod
@jolod
Jan 28 2018 16:17
Or you use a default value. Which you would do anyway, if you actually wanted the value.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:17
or absorb / correct the error somewhere silently by overriding the undefined place
yes
jolod
@jolod
Jan 28 2018 16:17
Like, average rating of an unrated product.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:18
so what's the difference between that and NaN in that particular case?
jolod
@jolod
Jan 28 2018 16:18
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:20
right so it's about the "remembering" I guess
jolod
@jolod
Jan 28 2018 16:20
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:21
I still wonder why both Haskell and Idris chose to use NaN and Infinity
jolod
@jolod
Jan 28 2018 16:22
If you add Infinity, which is nice, you need to add NaN, which is not nice.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:22
also who decided that 1 / 0 is Infinity
jolod
@jolod
Jan 28 2018 16:23
I think maybe you should blame Cauchy.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:23
well, lim n->0, n>0 of 1 / n is Infinity
Cauchy would agree with me on that
but he'd argue that lim n->0, n<0 of 1 / n is -Infinity right?
jolod
@jolod
Jan 28 2018 16:24
You're right, number should actualyl be a set
All calculations should be indeterministic.
Or, there should be no zero.
Only zero+ and zero-
Jean-Louis Giordano
@Jell
Jan 28 2018 16:26
I've read about supernatural numbers a while back https://en.wikipedia.org/wiki/Supernatural_number
jolod
@jolod
Jan 28 2018 16:26
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:27
I think it's also fine with 1 / 0 = NaN
division is simply not defined for 0
it's defined asymptotically around zero
jolod
@jolod
Jan 28 2018 16:27
It's just that division by zero being Infinity is so often useful.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:29
I think when talking about generalized natural numbers (i.e. positive natural numbers including zero and infinity) you can consider 1 / 0 = Infinity
jolod
@jolod
Jan 28 2018 16:30
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.
jolod
@jolod
Jan 28 2018 16:35
Or do fromMaybe PositiveInfinity $ map Double $ (x / y) if x and y are plain numbers.
where (/) :: Double -> Double -> Maybe Double.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:36
but then you get weird code like fromJust (x / 2)
jolod
@jolod
Jan 28 2018 16:37
Right, so you'd have both safe and unsafe versions.
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:42
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
jolod
@jolod
Jan 28 2018 16:46
Not sure. I think it depends.
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:48
sure but to carry the maybe you have to fmap a lot
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
jolod
@jolod
Jan 28 2018 16:51
I wouldn't mind a library that provides +', -', etc.
And those would be the Maybe versions. I've thought about that.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:52
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
jolod
@jolod
Jan 28 2018 16:53
Yeah, but using +' makes it not stand in the way, but it's still there.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:54
yeah why not. Perhaps with a different prelude even then?
but then all your custom functions still need to deal with the Maybe
jolod
@jolod
Jan 28 2018 16:55
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).
Jean-Louis Giordano
@Jell
Jan 28 2018 16:56
also what would be the type of 1 +' (1 / 2)?
jolod
@jolod
Jan 28 2018 16:56
Would you have that though?
Jean-Louis Giordano
@Jell
Jan 28 2018 16:57
why not?
jolod
@jolod
Jan 28 2018 16:57
Well, first, if it's 1 +' (1 / 2) then you should use +.
No need to use +'.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:58
come to think of it need to try to take NaN from a list
if the division returns a Maybe?
jolod
@jolod
Jan 28 2018 16:58
Aha!
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 16:59
:p
convenient!!
who said lenses?
jolod
@jolod
Jan 28 2018 17:00
Hehe.
But honestly, wouldn't that work? The question mark is great way to say maybe.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:01
could you define +' as a typeclass?
with all those implementations?
jolod
@jolod
Jan 28 2018 17:02
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.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:06
so Haskell doesn't let you take (1 / 0) because the numeric tower in Haskell makes it not an Int
jolod
@jolod
Jan 28 2018 17:06
Ah, yes.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:06
div 1 0 returns an Int and raise a runtime
jolod
@jolod
Jan 28 2018 17:07
OK, so when would your numbers, that involve NaN, interact with the "outside" in a meaningful way?
Jean-Louis Giordano
@Jell
Jan 28 2018 17:07
I think in that case basically only when casting them or representing them
jolod
@jolod
Jan 28 2018 17:07
Yeah.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:08
which could be the boundary check you need instead?
showNumber being Number -> Maybe String??? :p
jolod
@jolod
Jan 28 2018 17:08
No can do. :-)
Jean-Louis Giordano
@Jell
Jan 28 2018 17:08
nowai
jolod
@jolod
Jan 28 2018 17:09
Or wait, you said showNumber.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:09
ah!
yeah if you show $ showNumber then you say you want to print Nothing :p
jolod
@jolod
Jan 28 2018 17:09
Yeah, so that would be super annoying, because you would not be able to have data showable if it has numbers in them.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:10
unless you cast them to non-NaN numbers first?
jolod
@jolod
Jan 28 2018 17:10
All those instances with Show a => Show (T a) where.
Still annoying.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:11
isn't show taken for granted there though?
jolod
@jolod
Jan 28 2018 17:11
Anyway, gotta go. Still fancy my /? operator. :-)
Jean-Louis Giordano
@Jell
Jan 28 2018 17:12
yeah you need to follow that through :p
jolod
@jolod
Jan 28 2018 17:12
(Yeah, you probably shouldn't use show in user-facing code.)
jolod @jolod off.
Jean-Louis Giordano
@Jell
Jan 28 2018 17:12
:wave: