Syntax sugar and other tricks for inspiration about basil HOT 2 CLOSED

I'm not totally familiar with Agda, so perhaps I am missing something...but I believe the features described in the linked post are already mostly achievable (pending a stable Basil implementation 😛), at least within the scope Basil plans to support them.

Modules are already first-class, but only at compile-time - modules in Basil represent specifically namespaces or compilation units, and aren't repurposed as objects as they are in some other languages. Since they're a compile-time only construct, they can take advantage of the dynamic typing permitted in compile-time Basil, and store values of whatever type they want - effectively, modules are like a dictionary mapping from Symbol to Any. Like everything in compile-time Basil, we either resolve it correctly ahead of time, or we have to statically typecheck it before compiling it, so incorrect usage should be caught at the usage site of any module member during compilation.

The rest of their syntax looks quite nice! Unfortunately I'm not usually at liberty to adopt other languages' syntax into Basil's - generally we strive to have as little parsed syntax as possible, so most of these constructs would ideally be expressed as built-in functions. I'm still bookmarking that syntax listing for inspiration though - there's a few things I'm pretty uncertain about (self-referential types, for one) syntax-wise that Kind seems to have decent solutions for.

from basil.

There is cool trick how to "overcome" the static typing discipline incoherency when bundling e.g. a module with different functions having different return types:

https://github.com/uwu-tech/Kind/blob/master/blog/2-first-class-modules-with-self-types.md

It's probably that Basil will face similar typing issues, so this might come handy as an inspiration for a clean solution 😉.

from basil.