Draft talk:Unison (programming language)

• [https://towardsdatascience.com/a-quick-dive-into-unison-threads-38f4839a5152 Unison threads]
• [https://twitter.com/unisonweb On Twitter]

• [https://community.tmpdir.org/t/a-look-at-unison-a-revolutionary-programming-language/842 A look at Unison: a revolutionary programming language]
• [https://github.com/topics/unison Unison github topic]
• [https://medium.com/gft-engineering/magic-refactoring-with-unison-much-more-than-a-new-programming-language-7ad080bf9b72 Magic refactoring with Unison]
• [https://www.thestrangeloop.com/2019/unison-a-new-distributed-programming-language.html UNISON: A NEW DISTRIBUTED PROGRAMMING LANGUAGE]
• [https://renato.athaydes.com/posts/unison-revolution.html A look at Unison: a revolutionary programming language]
• [https://jaredforsyth.com/posts/whats-cool-about-unison/ What's cool about Unison?]
• [https://itnext.io/reading-files-in-unison-161601c1f786 Reading Files in Unison]

• [https://www.youtube.com/watch?v=rp_Eild1aq8 Lambda World 2018 - Introduction to the Unison programming language - Rúnar Bjarnason]
• [https://www.youtube.com/watch?v=yT5bi1Q3d0c Abilities in the Unison Language: A New Way of Looking at Dependency Injection and Stateful Effects]

• [http://blog.higher-order.com/assets/LambdaWorldSeattle.pdf Slides from Lambda Converence]

• [https://arxiv.org/abs/1306.6032 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.

• [https://www.youtube.com/watch?v=rdVqQUOvxSU Lennart Augustsson: Better type-error messages]

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