[alexkcd]

I really like how type checking is implemented for parameter lists. I think there's a more generalized extension of this.

Specifically, I think that there exists a lisp with a set of axioms that split program execution into "compile-time" execution (facts known about the program that are invariant to input) and a second "runtime" execution pass (facts that depend on dynamic input).

For example, multiplying a 2d array that's defined to be MxN by an array that's defined to be NxO should yield a type that's known to be MxO (even if the values of the array are not yet known). Or if the first parameter is known to be an upper-triangular matrix, then we can optimize the multiplication operation by culling the multiplication AST at "compile-time". This compile-time optimized AST could then be lowered to machine code and executed by inputting "runtime" known facts.

I think that this is what's needed to create the most optimally efficient "compiled" language. Type systems in e.g. Haskell and Rust help with optimization when spitting out machine code, but they're often incomplete (e.g., we know more at compile time than what's often captured in the type system).

I've put "compilation" in quotes, because compilation here just means program execution with run-time invariant values in order to build an AST that can then be executed with run-time dependent values. Is anyone aware of a language that takes this approach?

[_fbpt]

https://github.com/idris-lang/Idris-dev/blob/5965fb16210b184...

Idris is not a Lisp and I've never used it, but it has dependent types (types incorporating values) and encodes matrix dimensions into the type system (I think only matrix multiplications which can be proven to have matching dimensions can compile). I think the dimension parameters are erased, and generic at runtime (whereas C++ template int parameters are hard-coded at compile time). IDK if it uses dependent types for optimization.

[e12e]

I'm not sure, but this seems a bit like how Julia specialize functions based on type of arguments? Or maybe it's the inverse - as Julia creates specialized functions for you (eg add can take numbers, but will be specialized for both int32 and int64 and execute via appropriate machine instructions).

In fact, I think Julia is a great example of taking some good parts of scheme and building a more conventional (in terms of syntax anyway) language on top.

[alexkcd]

Yes, Julia has some of it. But you're still required to specify the template parameters of a type (unless I'm mistaken). Whereas what I'm talking about is that any value of a data type could be compile time known. For example, some or all of the dimensions of an nd-array, as well some or all values of said nd-array.

[KenoFischer]

Julia has explicit parameterization, but will also interprocedurally propagate known field values at compile time if known (which happens a lot more because our compile time is later), even if they weren't explicitly parameterized. Since this is so useful (e.g. as you say for dimensions of nd arrays - particularly in machine learning), there's been some talk of adding explicit mechanisms to control the implicit specialization also.

[alexkcd]

Ah, that's good to know. This sounds exactly like what I'm looking for. Thanks will read up on this in the docs!

[stewbrew]

"I think that there exists a lisp with a set of axioms that split program execution into "compile-time" execution"

Common lisp macros? Pre-hygienic macros in scheme? Did I get you wrong?

The question is what is missing to implement _static_ type checking as macros and to allow the compiler to leverage the generated information.

[alexkcd]

I'm not sure, but I think it's different. Specifically, I think you would do macro evaluation first, then fully evaluate the resulting program on run-time independent values, and only then evaluate the resulting program on run-time dependent values.

Edit: Also, run-time independent evaluation would need to handle branching differently. For example, in this expression: (if a b c). If `a` is not known at "compile time" then this expression remains in the AST, and run-time independent value propagation continues into `b` and `c`. If `a` is known at "compile time" then only `b` or `c` remain in the AST depending on whether `a` is true or false.