Thanks Wes, especially for the URLs relating type theory to "HoTT" by way category theory.
My friend and co-podcaster Alex, a math-physics-philo guy, has been pushing me to bone up in that area [1]. Those links really helped. I'm squeezing some of this in while reading the OSCON 2019 proposals, a big job, but I always learn a lot by so doing. [2] When it comes to Beginner Python and types, people have a strong grasp of number types coming in, especially ints, but think they know more about the string type than they really do, thanks to the whole coding/decoding business. i.e. strings are always "encrypted" (encoded) a specific way, even if only as plain ASCII text. K-16 doesn't do a lot to introduce Unicode, even though it's fundamental. I'd teach Unicode in language arts, along with fonts and old fashioned printing and book binding. What I find works well with kids and adults alike is a lot of emphasis on Emoji, which are now a part of Unicode after all. They're colorful and ubiquitous in modern life. There's something satisfying about being able to have ["😉", "🐋", "🚂"] as a Python list. We can also use non-keyboard characters in identifiers, though emoji won't work (there's no making your emojis callable in other words). *** testing 1-2-3... how did that list come through in the Mailman archives? Displayed as Emoji, not as missing glyphs? I see Wes already used a yellow hand pointing down, so I'm confidant the glyphs should be there *** Contemporary IDEs and web browsers are up to showing emoji. When you think about Unicode as a database with records (fields as attributes) you realize that the string type alone is a huge door opener. It's also about number bases and HTML entities. Lots to know. About half of my students are middle schoolers [3], the other half are adults [4]. The Emoji (Unicode) stuff works at all levels. I notice the Rust docs are into it. Show your language is Unicode savvy that way, good PR. Kirby Urner 4dsolutions.net cascadia.or.pdx [1] It's something of a joke how everyone starts a Monad tutorial the same way, by decrying the dearth of coherent Monad tutorials, hah hah. The emphasis on composing functions in category theory takes me to this decorator class, my Monad in progress: https://repl.it/@kurner/MakingMonads https://youtu.be/caSOTjr1z18 (functional programmer speaking to his community) https://youtu.be/SknxggwRPzU (Dutch prof with several relevant interviews on computerphile channel) https://youtu.be/IOiZatlZtGU (good overview of how logic and CS come together over time, focus on lambda stuff). FYI, I've used "λ-calculus" (Church, Turing et al) to loosely brand an alternative track through high school, that could in theory count with future employers and colleges as much as today's prevelant "Δ-calculus" (Newton-Leibniz). Here's how I use λ-calc in contrast with Δ-calc (against a STEM backdrop -- I've since done more to map out PATH). https://youtu.be/eTDH7m4vEiM I'm simply sharing a vision (heuristic, gestalt), akin to science fiction, not proposing legislation nor composing any "thou shalt" edict -- so no need to get too political about it I'm hoping. Food for thought. [2] a Medium story (be me) that gives a big picture broad brush stroke history leading up to the resurrection of O'Caml, the language: https://medium.com/@kirbyurner/stories-from-cyberia-fc857867e147 [3] middle school: next Coding with Kids gig starts tomorrow: https://youtu.be/6qlj_AZqpto (a look at Codesters) [4] adults: next SAISOFT gig starts in February: https://github.com/4dsolutions/SAISOFT (lots of Jupyter Notebooks; we also use Spyder and vs code, both with Anaconda)
_______________________________________________ Edu-sig mailing list Edu-sig@python.org https://mail.python.org/mailman/listinfo/edu-sig