Compiler Coffee Club - Interning Cyclic Types in a Compiler


See https://github.com/SeaOfNodes/Simple and https://github.com/cliffclick/aa.

This example at the beginning of type-checking a parser record structure is reminiscent of the problem of typing/sorting higher-order polyadic π-calculus. See Using Pipewire to Make A Music Synthesizer. I think there is some maths by Grothendeick that should help, see Category of elements in Wikipedia and Grothendieck construction in nLab. There is a use-case in David MacQueen's model of  types of higher-order functors: see David Macqueen's A Semantics for Higher-order Functors (1997) and Higher-order modules and the phase distinction by Harper, Mitchell and Moggi:

The hard part is probably deciding on what is the most useful phase distinction to introduce.

Subscribe to Cliff Click.

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

Welsh Republic Podcast Talking With Kars Collective on Armenia Azerbaijan Conflict

Image
  In the last 30 hours, Azerbaijan has blocked the Berdzor Corridor (the only route in and out of Artsakh), established a military police presence, threatened to shoot any flying object leaving the capital Stepanakert, and has now cut the gas supply. This is now a blockage. — Kars Collective (Կարսի Կոլեկտիվ) (@KarsCollective) December 13, 2022 Subscribe to Welsh Republic Podcast .
Read more

Daniel Tubbenhauer on The Riemann Hypothesis and Prime Counting

Image
He calls this lecture series The Analytic Theory of Monoidal Categories. So this is Analytic Number Theory with a Category Theoretic slant. This lecture is about graph theory. At 16:22 he asks for ideas: See the video description and  Standard ML For The Lady Programmer . Here's Sophie Maclean on the Catalan Numbers and Graph Theory: Here's what they posted 6 hours ago: see Daniel Tubbenhauer Doing Inscrutable Things With Analytic Number Theory ... for another finite-looking problem that might be solvable with SAT or SMT . Subscribe to Numberphile . See Larkin Poe - If God is A Woman, ... then I'm gonna get my bonfire, ... we have been building a giant haystack in a desert getting ready for Burning Man, the REAL F*CKING DEAL! Here's what I posted this morning on Nick Cave's The Red Hand Files #300: Joy! I went out walking this morning, ... But when I went past the boat again, I saw it was Sunquest : boat #6 from Bridge Boat Yard in Ely and the graffiti i...
Read more