Hacker News Reader

Comment by konjin | Hacker News Reader

Mathematical notation is terrible.

I don't mean this in the usual "we need to invent new symbols to make it clearer" way.

I mean it in the way that it has implicit typing that gets coerced constantly. Using Haskell types D :: (R -> R) -> (R -> R). Yet it gets used on things like D 2 = 0 which implies D :: (R -> R).

What you've actually done is an implicit conversion of 2 :: R to 2(x) = 2 :: R -> R and 0 is not 0::R it is 0(x) = 0 :: R -> R.

The Q_0 system described in [0] is a good start for a mathematical system that is both sane and as expressive as the one we have now. With term rewriting you can even keep the ridiculous notation we have today if you love it so much. Though I have grown incredibly fond of typing out extended typed lambda calculus using scheme notation in Emacs with a home grown automated theorem proving mode that was trivial to implement.

[0] https://www.springer.com/gp/book/9781402007637

View on HN

So you say we should specify when 2 means number two and when it means the constant function? How does it help?

Derivatives then are a higher order function that follow it's definition in all cases. You can't exactly apply it's definition as a limit in cases where it's applied to non-fictions.

That's not a very convincing example, given that numeric literals are polymorphic in Haskell.

Not all Haskell is GHC, though

I never said Haskell was a good language. Q_0 is a minimally acceptable math notation.

I honestly never found this an issue. Shorthand and type coercion is used a lot but at least when taught, it's usually made very explicit what notation means and when things are being excluded. After that point, the notation is the least challenging part.

It is not an issue until you start trying to teach any sort of fix point theorem, at which point the wheels fall off because the notion can't deal with higher order functions at all.

I guess I just don't get your point. D 2 = 0 doesn't imply anything, it's just shorthand to make working on something less tedious for people who are already familiar with it. It seems perfectly expressive and sane: mathematicians have successfully studied differentiation using standard math notation. 2 and (λ (x) 2) aren't 'treated the same', that's just a strawman.

Funny how its also used in every textbook for people who aren't. This is getting to be apologia on the levels that I'd only seen in history books about why Roman numerals were superior.

The premise of your argument is that this notation is confusing people, or it's impossible to make explicit what it means. I don't buy it, you even explained the type elision using standard mathematical notaion in your original comment.

So if there is some superior notation that would benefit all of maths, that sounds very interesting but I don't think you've made that point very well. Maybe a better example is needed, because on its own, eliding repetitive information from notation does not seem like a problem.

Because I'm not going to write a few dozen pages of latex in a text comment. If you're interested thrown me $2k over bitcoin and I'll spend the 8 hours it would take to make this rigorous at below my usual rates.

I use the mapsto arrow frequently for higher-order functions, and it seems to work fine for me.

Are you talking about this?

https://en.wikipedia.org/wiki/Q0_(mathematical_logic)

I agree that your example isn’t very convincing, for an additional reason. You can treat 2x as a function, or you can treat it as an expression, where x is its own special kind of thing: a symbol.

With how the notation is typically used, it’s at least closer to my mental model.

Treating the expression as a function under substitution is one way to look at it, but not the only way.

The point is that 2 and (λ (x) 2) are vastly different objects, yet in standard math are treated the same.

Also you don't need a symbol type to deal with variables, you just need to allow type variables to be used in standard expressions. (define x R) (^ x 2) is just as easy to manipulate as (λ (x) (^ x 2)), the only issue is that your rewrite rules how aren't just looking at syntax, but semantics too.

That sounds more like a lazy mathematician tbh. Do you have any other resource about the link you provided?

Reply on news.ycombinator.com