5 ms·

On a tangent. I think its worth it to push typed mathematics waaaaay down into highschool. While students are learning multiplication, the teaching tools/questi

On a tangent. I think its worth it to push typed mathematics waaaaay down into highschool. While students are learning multiplication, the teaching tools/question/answers need to teach how that changes the result's units (types). Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. ps. and our calculators (& excel) needs better support for it

carbocation 3y ago
When I was in high school units were a key part of science education. Is this no longer the case? Your point about tools that support units is great. Reminds me of https://frinklang.org/ https://frinklang.org/
Jtsummers 3y ago
> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).
- euroderf 3y ago
  Nor possible to write literately about energy issues.
seanhunter 3y ago
Most maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problems around velocity, speed, physical quantities etc and you are taught not to mix units, and how units "cancel" etc each other when you deal with exponent laws. Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education. I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before. [1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.
crazygringo 3y ago
> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. Did your highschool physics not have this? I always thought it was a universal part of all physics education. Doing things like canceling out units etc. has always been a big part of high school physics, and checking that your final answer has the units it should. (If it didn't, you made a mistake somewhere.) The idea of building units into Excel is definitely an intriguing one, though. I'm honestly kind of surprised it's the first time I've ever heard it suggested. It does seem like a pretty useful idea.
- antegamisou 3y ago
  Did your highschool physics not have this? Gotta love that USA's 'A'P classes' entire curriculum are Chapter 1, p.1 everywhere else.
  - OkayPhysicist 3y ago
    Unit analysis is absolutely a graded element of the AP test. The American educational system has enough to point and laugh at without fabricating new stuff.
tsimionescu 3y ago
Types and units are very different concepts. In fact it's quite hard to formalize the way units are used in everyday physics. For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2? It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way. Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics. And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade. But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.
mdnahas 3y ago
A good way to do this is to replace Geometry class. It is only there because Euclid’s Elements was read by Charlemagne’s kids. Geometry teaches proof, but a very outdated style of proof. It should be replaced with formal proofs, written in Lean or Coq. Since “a proof is a program”, it would also introduce programming into the curriculum.

carbocation 3y ago

When I was in high school units were a key part of science education. Is this no longer the case? Your point about tools that support units is great. Reminds me of https://frinklang.org/ https://frinklang.org/

Jtsummers 3y ago

> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).

euroderf 3y ago
Nor possible to write literately about energy issues.

seanhunter 3y ago

Most maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problems around velocity, speed, physical quantities etc and you are taught not to mix units, and how units "cancel" etc each other when you deal with exponent laws. Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education. I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before. [1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.

crazygringo 3y ago

> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. Did your highschool physics not have this? I always thought it was a universal part of all physics education. Doing things like canceling out units etc. has always been a big part of high school physics, and checking that your final answer has the units it should. (If it didn't, you made a mistake somewhere.) The idea of building units into Excel is definitely an intriguing one, though. I'm honestly kind of surprised it's the first time I've ever heard it suggested. It does seem like a pretty useful idea.

antegamisou 3y ago
Did your highschool physics not have this? Gotta love that USA's 'A'P classes' entire curriculum are Chapter 1, p.1 everywhere else.
- OkayPhysicist 3y ago
  Unit analysis is absolutely a graded element of the AP test. The American educational system has enough to point and laugh at without fabricating new stuff.

tsimionescu 3y ago

Types and units are very different concepts. In fact it's quite hard to formalize the way units are used in everyday physics. For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2? It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way. Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics. And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade. But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.

mdnahas 3y ago

A good way to do this is to replace Geometry class. It is only there because Euclid’s Elements was read by Charlemagne’s kids. Geometry teaches proof, but a very outdated style of proof. It should be replaced with formal proofs, written in Lean or Coq. Since “a proof is a program”, it would also introduce programming into the curriculum.