Learning Function Derivatives

It seems that there is a new feature that makes paragraphs all-caps??? WHAT? What-is-this-capitalization-scheme? Or is it just the first line ??

testing… 1, 2, 3… Okay, just first line of first paragraph. lovely!

Now then, having learned of causes for all the quirks in life, we should continue by introducing my own representation for talking about functions. Let the identity brane P_f:<String, Type>_I be the functional association of types with a set of formal parameter names:

        "first parameter"  : Integer
        "second parameter" : Boolean

The actual parameters has a dependently typed I-Brane P_a having instances that look like:

        "first parameter"  : 1
        "second parameter" : False

For convenience, we endow P_f and P_a with mutators: for some P_f we can write P_{f+\{"\textrm{third parameter}": String\}} to mean adding a parameter to the formal parameter specification, P_{f-["\textrm{first parameter}"]} to mean removing a formal parameter. similarly: with p:P_a the expression p_{[-"\textrm{first paramter}"]} has type P_{a-["\textrm{first parameter}"]} and can be used in the full invocation of any function typed P_{f-["\textrm{first parameter}"]}\rightarrow\Psi

Finally we type the type signature:

\Game_b: \big(P_f\rightarrow\Psi\big)\rightarrow P_{f-[b]}\rightarrow(B,B)\rightarrow\Psi\rightarrow\Psi

so, the type bounds would be able to stipulate that

\partial_p <: \Game_p

Note the \Game_b f should mostly be defined for functions f:P_f\rightarrow\Psi that has b as a formal parameter: b \in P_f.

   [ ] type up concrete example using ML
   [ ] dive into type definitions to be more rigorous.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s