­jonoodle­ @ionchy@types.pl

Tired: #AxiomKCrew
Wired: #TeamHaskell

I'm looking at the set of slides titled "Functional programming in other languages" and the example they use is PYTHON
How much influence can I impose on the prof to at least mention that the Racket they've been using all along in the intro course

Looking at last year's schedule, it looks like the first month about covers all the functional programming features we've been using in the PL course (which uses Racket)
It's just kinda weird that on one hand you'd need a month to cover all this stuff that we half expect the PL course students to be comfortable with, and that on the other hand we expect them to be comfortable with functional concepts that take a month to teach in the FP course

🎉 I'll be TAing a Haskell course next term 🎉

I apparently have forgotten how to write proofs that don't look like they should be typed into a proof assistant

(\x:(!P or Q). case x of [y:!P => \p:P. explode (y p)] [y:Q => \p:P. Q]) : (!P or Q) -> (P -> Q)
I think going the other way requires LEM so that breaks the connection these things have with each other

If (!P or Q) is classically equivalent to (P -> Q) and (P -> Q) is the nondependent version of (forall x:P. Q(x)), what's the relation between (!P or Q) and (forall x:P. Q(x))

That stuff is reserved for social media imo, it's the whole point

I mean I do spend a good chunk of time doing my own things, but it seems absurd to mention Pokemon Go or that tasteless coffee cake I made or the latest book I read in a meeting

Thinking about that time in a meeting after I mentioned the work I did that week someone asked me what about aside from work? and I was like aside... from work... ??

I mean how hard could it be to pick it up, I already know a couple of programming paradigms, what is but another

(Famous last words)

gasp I've been given the opportunity to TA the functional programming and logic course... but I do not know logic programming...

There are aesthetic problems with my type system and I do not like it

Continuing on my journey of not really understanding things until I actually implement them

We seem to be doing closure conversion in the same breath as defunc in this class
It's really closure conversion + hoisting but it ends up with an apply

I'm really taking this TAing thing by the seat of my pants huh

Oh defunctionalization is kinda like hoisting! But with datatype and an application function instead of a top-level function for each lambda