Skip to main content

Hello Web from Idris 2

·676 words·4 mins

Idris is a functional programming language with dependent types. I stumbled upon by accident a couple of years ago while browsing Manning’s newest releases in 2017 when Edwin Brady, Idris’ primary author, published his book Type-Driven Development with Idris. The book targets version one, but (almost) all attention is being directed at the next iteration, Idris 2.

While Idris 2 can compile to native, self-contained executables1, this is of little interest to our students. The JavaScript code generator, however, can target Node.js2. Could this make Idris usable for web development?

Hello Web

Idris’ documentation contains many useful recipes. Here, I have combined them into a minimal working example that wraps Node.js’s Http.Server.

Creating the server

In a standard Node.js application, an HTTP-server is created by calling the function createServer from the http module. This will return a Server object, which can then be instructed to listen on a port

const http = require("http");
const server = http.createServer((req, res) => {
  res.end("Bye!");
});
server.listen(8080);

Let us now assume that we already have a reference to a a Server object in our Idris code that we would like to listen on a given port. Most JavaScript objects are mapped to Idris’ AnyPtr type (notable exceptions being Numbers and Strings).

%foreign "node:lambda: (server) => server.listen(8080)"
prim__listenServer : AnyPtr -> PrimIO ()

The function prim__listenServer takes a reference to a Server object and passes it to the lambda given by the foreign directive. To use a PrimIO action, we pass it to the function primIO, which is implemented by IO3.

main = do
  s <- ?getServer
  primIO $ prim__listenServer s

The hole ?getServer has type IO AnyPtr. Let us create a server now. The complete program is listed below:

%foreign "node:lambda: () => require('http').createServer((req, res) => res.end('Bye!'))"
prim__createServer : PrimIO AnyPtr

%foreign "node:lambda: (server) => server.listen(8080)"
prim__listenServer : AnyPtr -> PrimIO ()

main : IO ()
main = do
  s <- primIO $ prim__createServer
  primIO $ prim__listenServer s

Idris can compile this into JavaScript targeting Node.js through its node code generator. Assuming the code is stored in Server.idr we call

idris2 --cg node -o server Server.idr

The result will be a JavaScript file named server in the build/exec/ directory. Run it using

node build/exec/server

and then send a request to localhost:8080 for instance using curl:

curl http://127.0.0.1:8080

A more sophisticated callback

Now that we have a simple server running, we can add some more sophistication. Let us write a server that echoes the user’s request data back to them. The callback to createServer takes references to an IncomingMessage and ServerResponse and builds the response, in true imperative style, by altering the ServerResponse object. To Idris both are AnyPtrs:

prim__createServer' : (callback : AnyPtr -> AnyPtr -> PrimIO ()) -> PrimIO AnyPtr

Keep in mind that the callback parameter here is curried, whereas by default JavaScript functions are not. We can therefore not directly pass callback to createServer. Instead we need to first apply callback to the IncomingMessage, obtaining a function from AnyPtr -> PrimIO (). Next, we apply the result to the ServerResponse, obtaining an object of PrimIO (). We need to call the result once more, without any parameters to execute the action specified by the object:

%foreign "node:lambda: (callback) => require('http').createServer((req, res) => callback(req)(res)())"
prim__createServer' : (callback : (AnyPtr -> AnyPtr -> PrimIO ())) -> PrimIO AnyPtr

Next, is the function prim__end which builds a callback given a String:

%foreign "node:lambda: (str, req, res) => { res.setHeader('Content-Type', 'text/plain'); res.statusCode = 200; res.end(str); }"
prim__end : String -> AnyPtr -> AnyPtr -> PrimIO ()

Finally, we can put it all together:

main : IO ()
main = do
  s <- primIO $ prim__createServer' $ prim__end "Hello, Web!"
  primIO $ prim__listenServer s

Outlook

This program is a minimal working example. Who knows, I will be able to build a more featured library on top. For now, the code is available on SourceHut.


  1. See the section on Compiling to Executables in Idris 2’s manual↩︎

  2. See JavaScript and Node Code Generators.↩︎

  3. it is a member of the interface HasIO which IO implements↩︎