Idris and PureScript are two very similar languages, so sometimes the differences can be surprising. In my time learning and using Idris, I ran into some of those surprises and thought I'd document them. The biggest challenges were in learning how to use Idris's foreign function interface, which is markedly different from PureScript.

FFI

In PS, we often rely on the run-time representation of certain data. For example, we might have an (admittedly contrived) definition as follows:

foreign import data SomeJsType :: Type

foreign import doSomething :: forall a. a -> a -> Effect SomeJsType

exports.doSomething = function (x) {
    return function (y) {
        return function () {
            return doSomething(x, y);
        }
    }
}

This definition relies on three things:

1. How to represent arbitrary, non-primitive JS types.
2. The runtime representation of Effect a for arbitrary types a.
3. How currying works. (Of course you could use the Effect.Uncurried module to sidestep currying explicitly, but that's beside the point)

With these three, you can basically use the FFI for anything.

FFI in Idris

Let's type the same example in Idris.

data SomeJsType : Type where [external]

%foreign "javascript:lambda:(ty, x, y) => doSomething(x, y)"
prim__doSomething : a -> a -> PrimIO SomeJsType

doSomething : a -> a -> IO SomeJsType
doSomething x y = primIO $ prim__doSomething x y

Immediately we notice a few things:

1. The difference in syntax when defining foreign data types.
2. The PrimIO and IO conversion.
3. A lack of explicit currying in JS.
4. Most interestingly, an extra parameter in the JS definition.

The extra parameter is an artifact of Idris's implicit parameters. In actuality, the type of prim__doSomething is shorthand for its desugared form:

prim__doSomething : {0 a : Type} -> a -> a -> PrimIO SomeJsType

If you stay in Idris Land, you don't always need to explicitly pass implicit parameters -- after all, they're implicit. But once you cross the FFI boundary into JS, that guarantee no longer holds. For this reason, I prefer not to type JS code as parametrically polymorphic since it's easy to forget the extra argument (and the more type variables there are, the more arguments are required). You could, instead, do the following:

prim__doSomething : AnyPtr -> AnyPtr -> PrimIO SomeJsType

toAnyPtr : a -> AnyPtr
toAnyPtr = believe_me

doSomething : a -> a -> IO SomeJsType
doSomething x y = primIO $ prim__doSomething (toAnyPtr x) (toAnyPtr y)

Idris isn't automatically able to tell whether some foreign code has side-effects or is pure -- that's the job of you, the programmer, when you give a signature for the foreign declaration. If your external code is pure, type it that way! You don't need to have a PrimIO return type for every FFI function.

You'll also notice that, unlike in PS we don't need to provide indirection by wrapping effectful JS code in a function () {...} expression.

The Callback Caveat

The biggest surprise for me was in passing callbacks through the FFI boundary. In PS, we might write a binding as follows:

exports.then_ = function (cb) {
    return function (prom) {
        return prom.then(cb);
    }
}

exports.finally = function (cb) {
    return function (prom) {
        return prom.finally(cb);
    }
}

foreign import then_
    :: forall a b
     . (a -> Effect (Promise b))
    -> Promise a
    -> Effect (Promise b)

foreign import finally
    :: forall a
     . Effect (Promise Unit)
    -> Promise a
    -> Effect (Promise a)

The JS is almost exactly the same, replacing only the words then and finally. In Idris:

%foreign "javascript:lambda:(cb, prom) => prom.finally(cb)"
prim__finally
     : PrimIO (Promise ())
    -> Promise AnyPtr
    -> PrimIO (Promise AnyPtr)

%foreign "javascript:lambda:(cb, prom) => prom.then((x) => cb(x)())"
prim__then
     : (AnyPtr -> PrimIO (Promise AnyPtr))
    -> Promise AnyPtr
    -> PrimIO (Promise AnyPtr)

There is an intentional difference here! While it is documented in the Idris2 example for JS events, it's very subtle.

The difference is as follows: If the callback is nullary, you can pass it as is. If it takes any arguments, you need to pass them in and then call it as a nullary function! If you don't, you may spend an inordinate amount of time trying to figure out why your program isn't doing anything, like I did.