Koka to C

[swarnpriya]

Is there a way to see the "intermediate C program" generated by the Koka compilation process?

[woojamon]

Are the files in the generated .koka folder what you're looking for?

[swarnpriya]

Thank you!

[swarnpriya]

Is there any good documentation about understanding the compilation chain from Koka to C? I am interested in changing the compiler to add more functionality to Koka like dealing with different kinds of syscalls etc.

[TimWhiting]

Sorry, not much documentation.

Runtime system is implemented in kklib. Most definitions have comments. I'd recommend starting with kklib.h here, which has the basic datatype definitions.

After that I'd look at how the std/core modules interface with C, the vector api is a simple place to start: vector.c vector.kk. You'll notice the extern import and the extern definitions.

The basic syntax is:

extern import
  c  file "inline/vector" // (or "vector.h" or "vector.c", etc) - in this case, it is in the folder 'inline'.

inline extern unsafe-assign : forall<a> ( v : vector<a>, i : ssize_t, x : a ) -> total ()
  c "kk_vector_unsafe_assign" // (c) Call this function with all of the parameters in the same order

inline extern unsafe-vector : forall<a> ( n : ssize_t ) -> total vector<a>
  c  inline "kk_vector_alloc(#1,kk_box_null(),kk_context())" // (c inline) Call this function but with the arguments as given with #1 being replaced with the first parameter etc... 

// Less well known if you want to directly call an external function you can omit the `kk_` and it won't add the `ctx` parameter
// which is used for the evidence vector.
inline extern unsafe-assign : forall<a> ( v : vector<a>, i : ssize_t, x : a ) -> total ()
  c "vector_unsafe_assign" // (c) Call this function with all of the parameters in the same order

inline fip extern ssize_t/(<)  : (ssize_t,ssize_t) -> bool
  inline "(#1 < #2)" // Sometimes you don't even need the extern import

// From the regex library (you can even import static libraries)
// Koka mainly supports preinstalled libraries and vcpkg, with conan best effort
extern import
  c { conan="pcre2/[>=10.37]"; vcpkg="pcre2"; library="pcre2-8" } // links libpcre2-8

This paper is the most recent as far as understanding the transformation that happens in the compiler to support algebraic effects.

Note that the hnd.kk module is the only module that
does not go through a monadic transform to support algebraic effects (as it is part of the implementation of that system).

You do not need to understand how it works under the hood though if you just want to bind to some system libraries. Let me know if you'd rather have some pointers into the compiler where this all happens, but I think you mostly want to use the extern system, and not mess around if the compiler if you do not have to.

[swarnpriya]

Thank you for these pointers. I will get back with more questions.