Questions and future

[dumblob]

This is a copy of Soonad/FormalityFM#6 as I'm not sure where the development happens mostly.

---

Newbie here. I'm impressed by the goals (and their actual current state of implementation). Well done!

I'd like to ask some questions (some more dumb, some hopefully less). I might be adding more over time in comments below 😉.

1. Do you have plans to make the syntax even simpler? I mean e.g. removing unnecessary colons, arrows, etc. Feel free to get inspired by the highly readable but very minimal syntax of V or (a bit less) Arturo.
2. What's the license of the code? If not decided, I'd raise my hand for MIT or BSD or any OSI-approved (unlike FSF-approved) license.
3. Having a C backend along with JS backend is a win-win nowadays. Would you consider adding a C backend? It might attract new contributors (namely those not afraid of low-level interfaces, etc.). And exactly these "low-level" thinking contributors are especially important in this phase of development IMHO.
4. As follow-up of (3) - have you considered the trick above-mentioned language V uses regarding compiler backends? Namely for debug purposes use TCC for sub-second compile&run and then some proper (GCC, Clang, MSVC, ...) compiler for -prod build?
5. Another follow-up on (3) - do you think making a generic C FFI abstraction would be possible in Formality? This is IMHO necessary for interfacing with "existing impure world" to allow Formality to be used immediately without re-introducing and re-programming everything by hand again.
   1. This might require something like claim similar to what I envisioned in Concatenative languages - Quark zesterer/tao#8 (comment) (as a substitute for C libs being incapable to deliver the proof terms Formality requires) along with effect from Koka to cleanly handle the "errors" and all other impure stuff.
6. Speaking of errors in (5), it's inevitable for a practical language to gracefully (here I mean really only visually syntactically) handle any non-default code branch. I dislike C++/Java/... exceptions, I dislike (but less) optionals, I dislike goto, I dislike pure functions (because the number of arguments becomes tremendously verbose), but I think the effect as in Koka (or the same but slightly disguised in Dylan as outlined in The future of Quark henrystanley/Quark#2 (comment) ) might have some potential (compared to rewriting the whole lib in Formality).
7. How to write mocked up or incomplete code to "just demonstrate a default path" in Formality without thinking about the proper types? This is again a practicality question (boiling down to the proposal of sassert assert and claim from Concatenative languages - Quark zesterer/tao#8 (comment) which can be added any time later to make the code type check without rewriting & refactoring huge portions of the code).

[VictorTaelin]

I didn't notice you posted here too! Copying my answer from the other thread:

1. Yes, the syntax is actually much simpler on the current release. This repository is an archive, the language is now being developed here: https://github.com/uwu-tech/kind . Lots of new syntaxes, check SYNTAX.md. And it will get simpler every day

2. Everything MIT (see LICENSE on the repo above)

3. We're working in one now! Based on inets. But in our spare time. If you're interested in helping let us know!

4. Not sure I understand?

5. We kind have something like that for JS (importing and using a Kind library in JS is as easy as installing a normal JS module). But I'm not that proficient with C. So I'll accept inputs and opinions of these more experienced with the language.

6. The way we do errors is optionals (i.e., Maybe, Either), and monads really help making them much more manageable and joyful to use. Are you used to Haskell's do notation? Also check the <> and without syntaxes on Kind. Simple stuff but really handy. To further improve that we'd probably go in the direction of algebraic effects.

7. Not sure what you mean, but I think you're talking about holes? For example:

Bool.not(a: Bool): Bool
  case a {
    true: ?a
    false: ?b
  }

?a makes the code check and allow you to fill it later.

[dumblob]

I didn't notice you posted here too! Copying my answer from the other thread:

Sorry for that. I think we can close the other one (and maybe clicking on "archive repo" on GitHub to disallow any further contributions - and of course before doing that write at the top of the README that the development happens here under a different name).

1. Yes, the syntax is actually much simpler on the current release. This repository is an archive, the language is now being developed here: https://github.com/uwu-tech/kind . Lots of new syntaxes, check SYNTAX.md. And it will get simpler every day

Looks promising. Maybe just removing the colons would suffice to make the lang really slick.

2. Everything MIT (see LICENSE on the repo above)

Great!

3. We're working in one now! Based on inets. But in our spare time. If you're interested in helping let us know!

What inets you mean? I have thought of CPS [1] [2] and e-graphs, but what is inets?

4. Not sure I understand?

There is one often totally overlooked and underrated "feature" of a compiled language. Namely speed of compilation. And because C compilers are generally slow (still much faster than C++ which are still much faster than Rust), it's worth it to use some speed-oriented C compiler (like TCC) which produces slow binaries. And for production (-prod argument in case of V compiler) a proper fat compiler (GCC, Clang, ...). Another advantage of this distinction is that the default (fast) compilation can produce different warnings/errors (incl. debug symbols, additional instructions for safer parallelism, etc.) than -prod build. This is very useful for debugging.

In Kind we should think about the speed of compilation now before it goes wrong as in Rust 1, 2, 3, 4, ... (small article series from one of the founders and main contributors to Rust).

People love speed of compilation and it's often the underlying (invisible and implicit) reason why a language with faster compilation (don't forget about languages with infinite speed of compilation - namely interpreted ones) is chosen over another generally better language. The pressure during development nowadays is very high so the speed of compilation should be taken rather seriously to even allow the language become practical.

5. We kind have something like that for JS (importing and using a Kind library in JS is as easy as installing a normal JS module). But I'm not that proficient with C. So I'll accept inputs and opinions of these more experienced with the language.

I'm not sure whether we mean the same thing. I meant calling C/C++ functions from and importing C/C++ structures into Kind and using them as native Kind functions/lambdas and native types. Therefore my mention of claim sassert assert etc.

Does Kind support such FFI? Any plans for that?

6. The way we do errors is optionals (i.e., Maybe, Either), and monads really help making them much more manageable and joyful to use. Are you used to Haskell's do notation? Also check the <> and without syntaxes on Kind. Simple stuff but really handy. To further improve that we'd probably go in the direction of algebraic effects.

I've taken a very brief look at the <> and without syntax and I'm under impression it trades off performance for convenience - please correct me if I'm wrong. If it doesn't then it seems to cover some of the problematic use cases.

I'm not used to Haskell's do notation in practise, so I can't judge whether it helps a lot or not so much. It seems it's usable only with monads (which though seem quite ubiquitous in Kind) and is basically not doing much except for saving some keystrokes for "sequential combinators" (a though up denomination I just thought up due to my lack of Haskell experience). Please correct me if I'm wrong.

Algebraic effects look more promising - my wish would be to make them as easy to use (i.e. syntactically & visually) as effects in Koka (which is in sharp contrast to e.g. Scala where effects are still annoying syntactically & visually).

All this is better to demonstrate on some real piece of SW with networking, user input & output, persistence (not only sending strings with selects to a DB queue, but let's say SQLite API with support for fully concurrent rw access), multithreading, etc. E.g. a web server together with some web application (I dislike web technologies, but it'd be a really good demonstrator here). The game you made looks cool - maybe it could be enhanced by some server-client interaction, SQLite persistence, multithreading, etc. There the need for effects, FFI, etc. might be more prominent and might guide us to better design how to syntactically handle it (i.e. which sugar to introduce and around which abstractions).

7. Not sure what you mean, but I think you're talking about holes? For example:

Bool.not(a: Bool): Bool
  case a {
    true: ?a
    false: ?b
  }

?a makes the code check and allow you to fill it later.

I've taken a look at holes and if having holes everywhere will compile and run, then yes, it's what I was asking about. But if it covers only some use cases, but leaves one to specify vast majority of types anyway, then I'd consider "holes" not being enough 😉.

E.g. I want to write:

Bool.not( a )
  case a {
    true: ?a
    false: ?b
  }
Debug.log( Bool.not( true ) )  // don't know whether Debug.log() exists

^^^ should compile and run because a Bool is given to Bool.not() (assuming Debug.log() accepts any type). In other words it should behave kind of like a "generic" function.

Later I realize people mistakenly try to pass "true" (a string literal) to Bool.not(), so I decide to avoid cryptic error messages (and help their IDEs to suggest passing only Bools to it) by adding type annotations:

Bool.not( a Bool ) Bool
  case a {
    true: ?a
    false: ?b
  }

Anything along these lines possible? I.e. postpone the type resolution and backpropagate it?

[dumblob]

ping 😉

[VictorTaelin]

Looks promising. Maybe just removing the colons would suffice to make the lang really slick.

What colons exactly? All colons and semicolons are optional already!

What inets you mean? I have thought of CPS [1] [2] and e-graphs, but what is inets?

It is the optimal runtime for functional programs (and arguably everything). It is basically what you get when you have a graph with arbitrary confluent rewrite rules. I need to write a post someday introducing the subject.

There is one often totally overlooked and underrated "feature" of a compiled language. Namely speed of compilation.

I fully heartedly agree, and I'm glad you asked! Having a fast compiler is one of the largest priorities of Kind, so turns out we have a plan. This is actually what I'm working on right now, since the last few changes in the language caused Kind to need way too much time to type-check itself: about 12 secs currently. Time has come to implement some long promised fast type-checking features, so they're coming soon.

First of all, let me remark a few things. Dependent types are naturally slow because you can have arbitrary computations on the type level. So the question is, how do we do it as fast as possible? First of all, we must make sure that, if we're type-checking simple/polymorphic terms, that we do it without extra costs. That is, checking a Haskell-like program shouldn't take more time than in Haskell, just because Kind has dependent types. This is something we explicitly optimize in procedures like Kind.Term.equal, by checking hashes, returning early and never triggering computations when not needed.

Second, we must make sure that, when type-level computations are unavoidable, that at least they're performed as fast as possible. This is a huge low-hanging fruit that we can take advantage of. Most (all?) other proof languages use explicit substitutions on type-checking. Agda, Idris, Coq, Lean do that. This is slow. As in, 100-1000x slower than it should be. Our type-checker is 100% HOAS, which means we delegate substitution to native lambdas and, thus, reduce the problem of having a fast type-checker to the problem of having a fast runtime.

Right now, though, we compile to JavaScript, which means type-level lambdas use JavaScript lambdas. That's great, but could be better. We'll very soon (like, in 2 weeks or so) migrate to using ChezScheme on the back-end, which means type-level computations will use native ChezScheme closures. This will make type-level substitutions fast. As fast as I think it is practically possible today, since ChezScheme is the fastest strict functional runtime available in the world. Compared to other proof languages, which do a ridiculously heavy "search/replace" of variables every time you apply a function, the difference is just ridiculous.

Of course, computation isn't only about substitutions. Sometimes you want to do things like multiplying numbers, sorting lists, manipulating data structures, doing loops. Right now, if you, for example, type-check refl : Equal(Nat, 100 * 100, 200 * 50, it will fully-expand both sides to their λ-encodings and reduce these. So there isn't much point in having fast substitutions, if the type-checker is dumb enough to do 10000's function calls when it could literally perform two native multiplications :) I have rough ideas on how to use Scheme's compilation capabilities to kind of compile type-level computations and have a JIT'ed type-checker, but this will be for a next moment.

Third, and, of course, there isn't much point in doing all of these optimizations, if we end up doing more work than needed anyway. Right now, every time you type-check a Kind term, it fully type checks its dependencies, all the way up to their very primitives. So, for example, when you type-check Kind/api.kind, it will go as deep as checking that Strings and UTF-16 libraries are well-typed. This all takes about 12 seconds currently, which IMO is quite good all things considered, and will be better. But is still obviously wasteful, since there is no point in re-type-checking all the base libraries when you only changed a few things. That's when incremental compilation comes in. Good news is: we'll probably have a fully incremental compiler very soon too; possibly together with the ChezScheme update!

The way it'll work is by storing type-checked, hole-filled top-level definitions in a .cache directory. So, once you attempt to type-check a term that is on .cache, it will completely skip it. The problem is: how do we invalidate that cache? We could naively store a hash of the source term and check if that changed. But this doesn't cover the possibility that the term didn't change, but one of its dependencies did, causing it to break even though it looks the same. In order to avoid that, whenever you retrieve a term from a cache, you'll recursively retrieve all its dependencies, and if any of these has changed, then the cache will be invalidated. The nice thing about this approach is that mutual recursion still works (it wouldn't if we used hash-based references, for example). That's because we can stop retrieving caches when find a loop.

So, for a roadmap: Kind's type-checker will use ChezScheme native lambdas and incremental compilation in 2 weeks or so. And, a little bit later, it may have JIT compile procedures for fast type-checking of numeric computations and things like that. To be very clear: my goal os to make Kind the fastest type-checker for a dependently typed functional language and I believe I'll accomplish that goal.

---

I'll answer the rest later, a lot to say too but you're covering lengthly subjects like monads, syntax, hole-filling/inference/unification, error messages etc. So I'll need some time to address these

[dumblob]

Again, thanks for the detailed write up! It sheds light on some things I was afraid of.

Looks promising. Maybe just removing the colons would suffice to make the lang really slick.

What colons exactly? All colons and semicolons are optional already!

Oh, didn't know that! So I assume the following is valid:

Bool.not( a Bool ) Bool
  case a {
    true ?a
    false ?b
  }

and means the same as:

Bool.not( a: Bool ): Bool
  case a {
    true: ?a
    false: ?b
  }

What inets you mean? I have thought of CPS [1] [2] and e-graphs, but what is inets?

It is the optimal runtime for functional programs (and arguably everything). It is basically what you get when you have a graph with arbitrary confluent rewrite rules. I need to write a post someday introducing the subject.

Very much looking forward to that! I skimmed your repository with inets, but I'm still missing some broader train of thought to realize their potential (and weaknesses/upper_and_lower_bound 😉).

There is one often totally overlooked and underrated "feature" of a compiled language. Namely speed of compilation.

I fully heartedly agree, and I'm glad you asked! Having a fast compiler is one of the largest priorities of Kind, so turns out we have a plan. This is actually what I'm working on right now, since the last few changes in the language caused Kind to need way too much time to type-check itself: about 12 secs currently. Time has come to implement some long promised fast type-checking features, so they're coming soon.

First of all, let me remark a few things. Dependent types are naturally slow because you can have arbitrary computations on the type level. So the question is, how do we do it as fast as possible? First of all, we must make sure that, if we're type-checking simple/polymorphic terms, that we do it without extra costs. That is, checking a Haskell-like program shouldn't take more time than in Haskell, just because Kind has dependent types. This is something we explicitly optimize in procedures like Kind.Term.equal, by checking hashes, returning early and never triggering computations when not needed.

Second, we must make sure that, when type-level computations are unavoidable, that at least they're performed as fast as possible. This is a huge low-hanging fruit that we can take advantage of. Most (all?) other proof languages use explicit substitutions on type-checking. Agda, Idris, Coq, Lean do that. This is slow. As in, 100-1000x slower than it should be. Our type-checker is 100% HOAS, which means we delegate substitution to native lambdas and, thus, reduce the problem of having a fast type-checker to the problem of having a fast runtime.

Clever!

Right now, though, we compile to JavaScript, which means type-level lambdas use JavaScript lambdas. That's great, but could be better. We'll very soon (like, in 2 weeks or so) migrate to using ChezScheme on the back-end, which means type-level computations will use native ChezScheme closures. This will make type-level substitutions fast. As fast as I think it is practically possible today, since ChezScheme is the fastest strict functional runtime available in the world. Compared to other proof languages, which do a ridiculously heavy "search/replace" of variables every time you apply a function, the difference is just ridiculous.

It might be rather less related to Kind's backend, but let me point out that ChezScheme still seems several times slower than non-functional languages (let's not discuss the benchmark itself and its accuracy - it's merely to demonstrate the trend and there I think it's representative enough).

But let's see how it goes in practice (I can easily imagine Kind will use mostly "highly optimizable" constructs of ChezScheme shifting the gaus curve closer to leading non-functional languages in the benchmark). My goal would be sub-second non-production-build (i.e. build without deep optimizations) compilation of non-cached project of the size of "full" Kind (i.e. several hundreds of thousands of lines of Kind source code).

Of course, computation isn't only about substitutions. Sometimes you want to do things like multiplying numbers, sorting lists, manipulating data structures, doing loops. Right now, if you, for example, type-check refl : Equal(Nat, 100 * 100, 200 * 50, it will fully-expand both sides to their λ-encodings and reduce these. So there isn't much point in having fast substitutions, if the type-checker is dumb enough to do 10000's function calls when it could literally perform two native multiplications :) I have rough ideas on how to use Scheme's compilation capabilities to kind of compile type-level computations and have a JIT'ed type-checker, but this will be for a next moment.

Third, and, of course, there isn't much point in doing all of these optimizations, if we end up doing more work than needed anyway. Right now, every time you type-check a Kind term, it fully type checks its dependencies, all the way up to their very primitives. So, for example, when you type-check Kind/api.kind, it will go as deep as checking that Strings and UTF-16 libraries are well-typed. This all takes about 12 seconds currently, which IMO is quite good all things considered, and will be better. But is still obviously wasteful, since there is no point in re-type-checking all the base libraries when you only changed a few things. That's when incremental compilation comes in. Good news is: we'll probably have a fully incremental compiler very soon too; possibly together with the ChezScheme update!

The way it'll work is by storing type-checked, hole-filled top-level definitions in a .cache directory. So, once you attempt to type-check a term that is on .cache, it will completely skip it. The problem is: how do we invalidate that cache? We could naively store a hash of the source term and check if that changed. But this doesn't cover the possibility that the term didn't change, but one of its dependencies did, causing it to break even though it looks the same. In order to avoid that, whenever you retrieve a term from a cache, you'll recursively retrieve all its dependencies, and if any of these has changed, then the cache will be invalidated. The nice thing about this approach is that mutual recursion still works (it wouldn't if we used hash-based references, for example). That's because we can stop retrieving caches when find a loop.

Yes! Yes! Yes! Caching! That'll help a lot in large projects!

I'll answer the rest later, a lot to say too but you're covering lengthly subjects like monads, syntax, hole-filling/inference/unification, error messages etc. So I'll need some time to address these

Take your time and thanks!

[VictorTaelin]

Oh I meant , and ; are optional, not :. Sorry.

Incremental compilation was added on 1.0.35 (e7ba5f8), the compiler is now basically instantaneous for every term on base.

[nothingnesses]

Fwiw, I'd also like to know what the situation and roadmap is with Kind's language interoperability and FFI.