Archive for the ‘type theory’ Category

Sample Terms for Practical Type Inference for Arbitrary Rank Types

I’ve been heads down following from my past work on Model Driven Architecture, Ontology and Logic(s). The questions that arise naturally in the course of studying these topics lead me to closely examine quantification and type systems. Higher rank types provide both a mechanism for polymorphism and high assurance in the subjects that motivated my study.

Down the Rabbit-Hole with Monad Transformers

Down the Rabbit-Hole with Monad Transformers describes my experience with type families that caused me to learn monad transformers.

Values, Types and Foundations

Recaps my Values, Types and Foundations talk at the OMG September Technical Meeting. Describes the computational, logic and philosophical presentation topics. Describes the demonstrations based on Oleg Kiselov and Anton Setzer’s work in Haskell and Agda. Constrasts the approach with ISO 24707 Common Logic.