statebox / idris-stbx-core

Category theoretic semantics of glued open Petri nets in Idris
https://statebox.org/
1 stars 1 forks source link

Unifying FFI execution and Computer (step 1) #43

Open clayrat opened 5 years ago

clayrat commented 5 years ago

The problem we've encountered in a live coding session on 2019/10/03 is that we can't parameterize the FFI call over the function name:

Type checking ./Main.idr
idris: Foreign Function calls cannot be partially applied, without being inlined.
CallStack (from HasCallStack):
  error, called at src/IRTS/CodegenC.hs:350:38 in idris-1.3.2-HavsjJD68mD4JhbQOwqxh8:IRTS.CodegenC

One possible solution would be to use type providers to generate the static FFI function descriptions from some structured text file, a-la https://github.com/ctford/flying-spaghetti-monster/