(This comes from @annedino4's User Research Report Round 2, issue number 22.)
Initial testing indicates that students have a bit of trouble initially describing the type of a fully-saturated function application. They want to mention arrows (→) in the type because up to this point, they've only been writing function definitions, and we ask them to describe the function types, which always include an arrow.
Why don't we replace function application symbol $ with ← ? This nicely mirrors the function type constructor → and gives students a handy rule: when applying a function to an argument, each ← "cancels out" a → in the function type. Then figuring out how many applications are needed is just a simple bookkeeping rule.
Another nice feature is that applications and function type constructions are kind of mirror images of each other.
(This comes from @annedino4's User Research Report Round 2, issue number 22.)
Initial testing indicates that students have a bit of trouble initially describing the type of a fully-saturated function application. They want to mention arrows (→) in the type because up to this point, they've only been writing function definitions, and we ask them to describe the function types, which always include an arrow.
Why don't we replace function application symbol $ with ← ? This nicely mirrors the function type constructor → and gives students a handy rule: when applying a function to an argument, each ← "cancels out" a → in the function type. Then figuring out how many applications are needed is just a simple bookkeeping rule.
Another nice feature is that applications and function type constructions are kind of mirror images of each other.