idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

[ cleanup ] Make `makeFuture` to be `%foreign`, not `%extern` #3341

Closed buzden closed 1 day ago

buzden commented 2 days ago

Description

System.Future in contrib is strange, especially because it relies on two backend-specific functions, prim__makeFuture and prim__awaitFuture which are very different: the first one is a special primitive function that compiler is aware of, when the second one is a normal %foreign function. The main reason for this was the desire to pass Lazy value into the foreign function, which is not supported (for good reason, I think), so it was made a primitive.

But I think that this was, basically, the XY-problem -- we actually wanted to pass not a Lazy value of type a, but a function that returns a when demanded -- in general case, semantics of Lazy values may differ, but semantics of this call does not. Also, it is pretty disgusting that we have a compiler primitive that is excersised only in contrib. Also, this siituation leads to problems like #3292.

So, I propose the change which makes both basic functions in this module be declared as %foreign, thus removing the MakeFuture primitive from the compiler.

Should this change go in the CHANGELOG?