Conversation

Notices

1. Embed this notice
   Jade Master (jademastermath@mathstodon.xyz)'s status on Thursday, 16-Jan-2025 06:50:22 JST Jade Master

   Latest on why would you do this

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Thursday, 16-Jan-2025 06:52:37 JST julesh

     in reply to

     @JadeMasterMath Filling a temporary file from a string constant is a bit horrifying, but otherwise this gets my stamp of approval for combining a proper top level language with "haha python go brrr"

     ps. since I also constantly bug Zanzi about unnecessary brackets in idris code: `IO Int` not `IO (Int)`

   • Embed this notice
     Dima Pasechnik 🇺🇦 🇳🇱 (dimpase@mathstodon.xyz)'s status on Thursday, 16-Jan-2025 08:17:33 JST Dima Pasechnik 🇺🇦 🇳🇱

     in reply to

     • julesh

     @julesh @JadeMasterMath I see - certified functional graphics in Haskell... and if you look under the hood of numpy/scipy you are likely to discover that it calls C functions, mostly 🙂

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Thursday, 16-Jan-2025 08:31:48 JST julesh

     in reply to

     • Dima Pasechnik 🇺🇦 🇳🇱

     @dimpase @JadeMasterMath Yeah, direct Idris bindings to BLAS or whatever would be pretty neat but would probably be an absolute tonne of work to build

   • Embed this notice
     Dima Pasechnik 🇺🇦 🇳🇱 (dimpase@mathstodon.xyz)'s status on Thursday, 16-Jan-2025 09:35:24 JST Dima Pasechnik 🇺🇦 🇳🇱

     in reply to

     • julesh

     @julesh @JadeMasterMath why does it have to be a ton of work? one needs to build a good enough FFI build tool, something akin to pybind11 for Python FFI to C++ (and C).
     https://pybind11.readthedocs.io/en/stable/