Automatic type inference and explicit elaboration of programs with support for algebraic effects is presented in this work. ImpEff, a simple polymorphic functional calculus with support for algebraic effects, based on the Eff language is presented. For the MiniEff language a corresponding progress and preservation theorems are presented and proved. The type system of the MiniEff language is enhanced with the ImpEff programing language, which adds an effect-type system with subtyping to existing MiniEff types. Progress and preservation theorems and their proofs are updated to coincide with effect based type system, where key changes to the MiniEff version are explained. The ExEff language is presented, which is an explicit version of ImpEff language based on the polymorphic lambda calculus. A type system along with the accompanying progress and preservation theorems and their proofs is presented. The rules for the elaboration of programs from ImpEff to ExEff are presented along with proof, that elaboration preserves types. A variation of the Hindley-Milner type derivation algorithm is presented, which infers types of ImpEff programs and elaborates them to explicit ExEff programs. For the given elaboration algorithm, the corresponding soundness, and completeness theorems are presented. Changed inference and elaboration relation with lazy substitutions, as currently used in Eff compiler is presented.
|
