I have too many things I want to do at once :blobcat_ohnoes:
=> More informations about this toot | View the thread
Thinking about plants and trees and grammars :thaenkin:
=> More informations about this toot | View the thread
Being interested in the design of programming languages and type systems, I found the physical safety systems used on this steam railway fascinating:
• A metal staff that only a single train can carry at a time prevents crashes
• Mechanical constraints prevent signals being set incorrectly
https://youtu.be/T2_LEQU6uZQ?t=414
=> More informations about this toot | View the thread
Does anyone have any context to how things went with the Static DOM and Purview stuff Phil Freeman was working on in Purescript?
From what I’ve seen Purview seems relatively lightweight https://github.com/paf31/purescript-purview (including the library it’s based on) and learning about the incremental lambda calculus might be handy, so might be worth a quick experiment… I’m mainly curious to know if there’s any pitfalls to be aware of.
=> More informations about this toot | View the thread
If for some reason you want the old code, you can still find it here: https://github.com/brendanzab/color-rs (it's so ancient that all the metadata is messed up on crates.io).
=> More informations about this toot | View the thread
Glad that the Linebender org is now making use of the color crate name! https://mastodon.online/@raph/113516957574119221 😅
=> More informations about this toot | View the thread
I’ve been thinking along these lines because I’d like to try using build systems for implementing query-based language tooling (see https://ollef.github.io/blog/posts/query-based-compilers.html), and it would be neat if similar infrastructure could be re-used for other things.
I could be missing some key challenges however – not being an expert in either domain.
=> More informations about this toot | View the thread
Wondering if “Build Systems à la Carte” https://doi.org/10.1017/S0956796820000088 could be used for implementing reactive user interfaces 🤔
=> More informations about this toot | View the thread
Is there a programming language out there that sort of has… built in recursion schemes? i.e. so that you don’t need to remember a menagerie of different weirdly named functions, juggle fix datatypes or do painful stuff to support mutual recursion? I know of the “catamorphisms” in the nanopass framework (https://nanopass.org/), which essentially let you forward through a transformation automatically and elide boilerplate cases, but I’m hoping for something more general.
=> More informations about this toot | View the thread
Kurtz and Fernhout also made a tool for creating interactive fiction called StoryHarp: https://www.kurtz-fernhout.com/StoryHarp/
=> More informations about this toot | View the thread
Lovely blog post on PlantStudio, an interactive tool for creating plants: https://pketh.org/plantstudio.html. You find out more about it from the original site too: https://www.kurtz-fernhout.com/PlantStudio/.
=> More informations about this toot | View the thread
One frustration I’ve run into when making a type checker/elaborator for a programming language that uses normalisation-by-evaluation in types is the following gap in terminology:
I.e. what do I call a type in the semantic domain?
I’ve listed some potential solutions here, but I’m curious if other people have favored approaches to this: https://gist.github.com/brendanzab/61ad11d0e6d007a084365c56035efd79
=> More informations about this toot | View the thread
@TodePond These videos remind me of @jesper’s recent toot: https://agda.club/objects/f7187912-c99e-4105-85b2-f85ef37e2fe7
=> More informations about this toot | View the thread
Watched a good chunk of @TodePond’s calming, expansive and surreal videos on computational world building last night! It’s an incredibly inspiring body of work! I’d love to make things like this some day.
Here’s one to start you off: https://www.youtube.com/watch?v=Q4OIcwt8vcE
=> More informations about this toot | View the thread
Went on an adventure today and came back with this:
=> View attached media | View attached media | View attached media | View attached media
=> More informations about this toot | View the thread
@ollef oh hello!! 👋
=> More informations about this toot | View the thread
In case it’s useful to anyone, I’ve added an example of bidirectional elaboration for a polymorphic lambda calculus to my language garden, using normalisation-by-evaluation for comparing types: https://github.com/brendanzab/language-garden/tree/main/elab-system-f-bidirectional
Note that I’ve not implemented implicit instantiation of type applications and pattern unification – that would be a separate project, but I’ve provided links to sfpl and elaboration-zoo which show how to implement this.
=> More informations about this toot | View the thread
related conundrums:
:blobcat_ohnoes:
(edit: removed some nonsensical versions)
=> More informations about this toot | View the thread
Is anyone else unreasonably distressed by the asymmetry of “metalanguage” and “object language”? :-(
=> More informations about this toot | View the thread
Bumped into some nice slide decks from @graydon today (more here http://venge.net/graydon/talks/):
I always find this kind of synthesis of theory and practice, with a keen awareness of historical context and one’s own limitations in understanding this context incredibly inspiring and wonderful.
=> More informations about this toot | View the thread
=> This profile with reblog | Go to brendan@types.pl account This content has been proxied by September (ba2dc).Proxy Information
text/gemini
