Draft talk:Unison (programming language)

Unison resources

• Unison threads
• On Twitter

• A look at Unison: a revolutionary programming language
• Unison github topic
• Magic refactoring with Unison
• UNISON: A NEW DISTRIBUTED PROGRAMMING LANGUAGE
• A look at Unison: a revolutionary programming language
• What's cool about Unison?
• Reading Files in Unison

Talks

• Lambda World 2018 - Introduction to the Unison programming language - Rúnar Bjarnason
• Abilities in the Unison Language: A New Way of Looking at Dependency Injection and Stateful Effects

Background

• Slides from Lambda Converence

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism

Jana Dunfield, Neelakantan R. Krishnaswami

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as eta-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete.

• Lennart Augustsson: Better type-error messages

Mechachleopteryx (talk) 23:59, 21 July 2023 (UTC)