<div class="chatlog__message-group"> <div id="chatlog__message-container-847793615077900288" class="chatlog__message-container" data-message-id="847793615077900288"> <div class="chatlog__message"> <div class="chatlog__message-aside"><img class="chatlog__avatar" src="https://cdn.discordapp.com/avatars/189711109966659584/95280765d1be73ce985dce15ea3585f6.png?size=512" alt="Avatar" loading="lazy"></div> <div class="chatlog__message-primary"> <div class="chatlog__header"><span class="chatlog__author" style="color:rgb(237,171,161)" title="omochimetaru" data-user-id="189711109966659584">omochimetaru</span> <a href="/channels/380329942505750529?category=コミュニティ&channel=waiwai-swiftc&message_id=847793615077900288"><span class="chatlog__timestamp" title="Friday, May 28, 2021 11:09 AM"></span></a><a href="#chatlog__message-container-847793615077900288">5/28/2021 11:09 AM</a></div> <div class="chatlog__content chatlog__markdown"><span class="chatlog__markdown-preserve"><a href="https://forums.swift.org/t/formalizing-swift-generics-as-a-term-rewriting-system/45175">https://forums.swift.org/t/formalizing-swift-generics-as-a-term-rewriting-system/45175</a></span></div> <div class="chatlog__embed"> <div class="chatlog__embed-color-pill" style="background-color:rgba(255,255,255,255)"></div> <div class="chatlog__embed-content-container"> <div class="chatlog__embed-content"> <div class="chatlog__embed-text"> <div class="chatlog__embed-title"><a class="chatlog__embed-title-link" href="https://forums.swift.org/t/formalizing-swift-generics-as-a-term-rewriting-system/45175"> <div class="chatlog__markdown chatlog__markdown-preserve">Formalizing Swift generics as a term rewriting system</div> </a></div> <div class="chatlog__embed-description"> <div class="chatlog__markdown chatlog__markdown-preserve">Formalizing Swift generics as a term rewriting system Previously I wrote about how the full generality of the Swift generic system is undecidable. The basic idea is that "finitely-presented monoids" can be written as a Swift protocol where the "word problem" on the monoid reduces to proving an equivalence between two types. Since the word proble...</div> </div> </div> <div class="chatlog__embed-thumbnail-container"><a class="chatlog__embed-thumbnail-link" href="https://images-ext-1.discordapp.net/external/_Hh9yA8h7qPuitkZs_0x0RZmHnZSATEiv_IAmCnP7cM/https/aws1.discourse-cdn.com/swift/original/1X/0a90dde98a223f5841eeca49d89dc9f57592e8d6.png"> <img class="chatlog__embed-thumbnail" src="https://images-ext-1.discordapp.net/external/_Hh9yA8h7qPuitkZs_0x0RZmHnZSATEiv_IAmCnP7cM/https/aws1.discourse-cdn.com/swift/original/1X/0a90dde98a223f5841eeca49d89dc9f57592e8d6.png" alt="Thumbnail" loading="lazy"> </a></div> </div> </div> </div> </div> </div> </div> </div>