Pun Calculus

A variant of Typed Lambda Calculus with generalized variable punning (ad-hoc polymorphism).

EBNF

rhs        := [a-z][_a-zA-Z0-9]*   //Variable
            | ( rhs* )             //Function Application
            | λ rhs* . rhs*        //Lambda Function
            | [^ ]+                //Literal Value

binding    := [a-zA-Z0-9]+ [:] [=] rhs \n

program    := binding*

Types

Typechecking is a graph-coloring problem to ensure that Cannot Determine Color does not get applied to the result of Greedy Infer.

$$greedy \ infer \quad \frac{f:A \to B \quad f:B \to C}{f:A \to C}$$

$$cannot \ determine \ color \quad \frac{f:A \to B \quad f:B \to C \quad f:A \to C}{\bot}$$