DSL for building mathematical functions which supports type-safe variable capture and partial application: https://github.com/breandan/kotlingrad/blob/master/src/main/kotlin/edu/umontreal/kotlingrad/samples/VariableCapture.kt

Hi Breandan, nice to see some progress, I am not sure, what you want to achieve with that. Could you explain? Could it be obtained by more simple means like this one: https://github.com/mipt-npm/kmath/blob/master/kmath-core/src/commonTest/kotlin/scientifik/kmath/expressions/ExpressionFieldTest.kt ?

On mobile RN, but the intention is to have an API surface where, if passed a variable binding which does not occur in the expression, it does not compile. Invocation is only syntactically correct when variables which occur in the expression are bound to values. If and only if all variables in the expression are bound, it returns a value, otherwise it returns a partial function.

I am not sure that it is a good idea to do it all on a type level. Kotlin type facilities are just not meant for that level of compile-time control (you actually need higher-kinded types for that). As for returning value or function, it could be done by tracking the residual number of degrees of freedom. It could be done in compile time, but again, I do not see a reason to do it in compile time (other than mathematical correctness).

That’s what I thought as well, but higher-kinded types are not necessary, as long as you limit the number of unique variables in an expression. Then it’s fairly straightforward to build a state machine to capture the variables and perform partial application. Only downside is the code size, which can be reduced somewhat but is roughly O(2ⁿ) w.r.t. the number of unique variables. Re: Kotlin. It can also be implemented in Java or any language with subtyping and generics (I believe). It’s just a proof of concept, but also a demonstration that less powerful type systems like Kotlin and Java are also capable of encoding some interesting properties. In terms of usability, it would be easier to implement arity-checking and currying at runtime but if implemented at the type-level would allow for code completion and inference. The #arrow folks are using a similar approach for their curry implementation, which is order-sensitive: https://github.com/arrow-kt/arrow/blob/master/modules/core/arrow-syntax/src/main/kotlin/arrow/syntax/function/currying.kt

I do not like the idea of arrow. It brings some concepts not because we need them, but because others have them. As for discussed problem, I think that it could be a good solution to create a compiler plugin which would check mathematical correctness instead of abusing the type system. It should be straight forward after 1.4. you would be able to turn it on or off without changing the code.

I would be interested in developing a compiler plugin, but last time I heard it was not straightforward. Perhaps after 1.4 it will be easier, but I think it will still require maintaining a separate IDE plugin and compiler stack. At least for simple properties like array length checking and variable capture, it is possible to encode these properties at the type level, but I don't believe such a strict API should be forced upon the user - dynamic length array construction and unsafe currying should also be supported (just a matter of providing an unsafe API with a safe wrapper). Is it abuse? Maybe, I don't know. It's a design pattern that seems to work, and does not require building a separate compiler and IDE toolchain. Would you call LINQ/jOOQ or other fluent interfaces abusing the type system? https://en.wikipedia.org/wiki/Fluent_interface#Java