This Func Prog Sweden podcast episode features a conversation with Aram Hăvărneanu about type theory, programming languages, and functional programming. The discussion centers on the differences between Curry-style and Church-style type systems, exploring their implications for modeling open versus closed worlds, and the design considerations for a new programming language aiming for simplicity, flexibility, safety, and performance.
Curry-style vs. Church-style Type Systems: The podcast delves into the fundamental differences between these two approaches. Curry-style systems prioritize computation, assigning types externally, while Church-style systems prioritize types, integrating them directly into the operational semantics. This distinction significantly impacts the ability to model open-world systems.
Open vs. Closed World Assumptions: The discussion highlights how Church-style systems inherently assume a closed world (all information is known), whereas Curry-style systems better accommodate open worlds (where information may be incomplete or evolve). This is crucial for modeling real-world systems.
Types as Meanings: Hăvărneanu proposes that types represent meanings, serving as mental or mathematical models for understanding systems. This perspective influences the design of type systems for better comprehension and engineering of real-world programs.
The Design of a New Programming Language: Hăvărneanu discusses his work on a new language emphasizing simplicity, flexibility, safety, and performance. The design incorporates Curry-style type systems and linear logic to address limitations in existing languages, particularly regarding memory management and the representation of complex data structures.
Q Language and its Unique Properties: The conversation explores the Q language, highlighting its unique features: a total language with a termination checker, reliance on unification rather than function application, and a set-theoretic model that enables flexible type assignments and monotonic refinement of information.
