Sharing some of my own work for comparison and inspiration

[wkolowski]

Hi

I have read some of your writing in this repo and I strongly agree with the overall goal/idea/vision, but disagree with particular details. The disagreements are not that important, however. What I want to do instead is a (shameless) plug: over the past months I too have tried to design a "one language to rule them all", inspired by the usual suspects of Coq, Agda, F*, Lean and Idris (and a few others). You can read the draft here: https://github.com/wkolowski/Type-Theory-Wishlist (but beware: contrary to you, I prefer purely functional languages; also, it is very long). I hope you find some time to take a look at it and draw some inspiration from there.

Also, just like you, I too have stumbled upon the idea of writing a "Coq for programmers" book (well, in my case it's more like "Coq for everyone"), stemming from my dissatisfaction with the fragmentation of knowledge sources, obscure and badly written papers and so on. I even tried to write it: https://wkolowski.github.io/CoqBookPL/ (beware: it's written in Polish), but I don't have enough time to finish it.

I hope your grand quest will be successful : )

[blainehansen]

Thank you for sharing! I'll absolutely read through these resources as much as I can :)

I've been working on a more in-depth defense of my insistence on the imperative paradigm being the focus of our efforts, so as soon as that's done I'll share it here. I look forward to discussing!

[chkoreff]

You might want to check out some of the concepts in my functional programming language Fexl. I have been using it almost exclusively for years in my business, which is accounting for investment partnerships.

https://fexl.com

Fexl is not statically typed. I figured if I wanted to build a static type system, I would do that in Fexl itself, which would start off untyped. So far I have not been inclined to do static typing. Good systematic development with regression testing and full coverage have worked very well for me. Personally, I find statically typed languages to be too burdened with cumbersome declarations.

Although Fexl is not "purely functional," you can make any program be exactly as "pure" as you want it to be. For example, I/O is straightforward, so the "Hello, world" program is simply; say "Hello, world." There is no "monad" there, just a call to the "say" routine. To make that program purely functional, you would write a function that returned the string "Hello, world." Then a higher-level "impure" layer would be tasked with applying "say" to that result.

If you want to do "memoized" functions, Fexl has routines for doing mutable variables. This can be nice for optimizing naive versions of recursive functions like Fibonacci, or the Partition count function which is far more self-recursive. (Note: I'm personally in favor of a more purely functional approach to memoization, where an immutable cache table is explicitly passed around in and out of the function, but sometimes the grungy mutable approach will save you in a pinch.)

Fexl represents recursion explicitly using the fixpoint operator, which I denote by "@". The nice thing about explicit fixpoint recursion is that a call to a recursive function can be expanded directly in place -- i.e. referential transparency applies here as well. You can also identify some interesting optimizations where some parameters are fixed and do not need to be passed into recursive calls. (Note: Tail recursion "just works" because of how I do parameter substitution. I don't have to do anything special to get it.)

Fexl also has a very useful feature for idempotent "once" calculations. If you have an expression such as (f x y) buried somewhere, and maybe it takes a long time to run or even has side effects you only want to happen once, you can change the expression to (\= f x y) and then it only runs once, if you happen to call it. I cannot emphasize enough how useful and convenient that is for my real project work.

My design goal for Fexl was to have a language which is as close to pure lambda expressions as possible, with additional syntax added only to make it practical. Most of the additional syntax has an equivalent plain lambda expression. Another goal was to implement Fexl in the smallest feasible plain C code, which I think I've done.

I'll leave it there for now. If you'd like me to elaborate anything further, please let me know. You may find some of the ideas helpful in your efforts. For example, I think I've done very solid work on concepts such as parameter substitution, and the closely related concept of modularity, which Fexl handles using functions known as "contexts."