ccfontes / faas-idris2

An OpenFaaS template for writing Functions in Idris 2.

OpenFaaS Idris 2 template

An OpenFaaS template for writing Functions in Idris 2.

Prerequisites

• OpenFaaS CLI: makes the faas command available.

Usage

Pull OpenFaaS template

To create Idris 2 Functions with this template, use the following command once:

faas template pull https://github.com/ccfontes/faas-idris2

If you ever need to update the template, simply run the command above with the --overwrite flag.

Create an Idris 2 Function

Create Idris 2 Functions as with the following command example:

faas new --lang idris2 my-idris2-function

A new project is created for a function defined as my-idris2-function. It will contain a Function.Handler namespace that is required for the template to work properly. The requirement for this namespace is to have a top-level function defined as handler : String → String.

Specs

Language	Package manager	Dependency file	Codegen
Idris 2	pack	config.ipkg	N/A
Chez	TODO	TODO	chez (default)
Racket	TODO	TODO	racket
Node	yarn	package.json, yarn.lock	node

A Package manager will read dependency files that you provide, using conventions in the table above.

OpenFaaS watchdog is of-watchdog in Streaming fork mode. I couldn’t find a working HTTP server fully written in Idris 2, so that we could use recommended of-watchdog HTTP mode.

Function builds only install the tools required for configured codegen.

Using other code generators

Default code generator is Chez scheme, but you may want to use other code generators, depending on your requirements.

For all code generators, Idris 2 library configuration is the same as in Pack libraries.

Add <codegen> to your <function-name>.yml or stack.yml as in the following example:

  idris2-racket-hello:
    lang: idris2
    handler: ./idris2-racket-hello
    image: ${DOCKER_REGISTRY_IMG_ORG_PATH}/idris2-racket-hello
    build_args:
      CODEGEN: <codegen>

The codegen options can be found in table under Specs.

Pack libraries

You can add new Idris 2 libraries using Pack, which is already configured in the template.
To add new libraries, edit the function.ipkg file present in the root directory of your Function. Example:

depends = dinwiddy

This adds Pack supported dinwiddy library package to the project. This way also supports adding library packages shipped with Idris 2.

It is also possible to add external library packages that aren’t supported yet by Pack. To do this, create a file named pack.toml in the root directory of your Function, as such:

[hashmap]
type   = "github"
url    = "https://github.com/Z-snails/idris2-hashmap"
commit = "58f5a2d2c0a7bb082666d6ce668ee242185a52bf"
ipkg   = "hashmap.ipkg"

Then in function.ipkg, add hashmap library package:

depends = dinwiddy, hashmap

Function examples

See the function-examples directory to find a fully working set of OpenFaaS Functions written in Idris 2.

Production expectations

Hopefully, this effort will bring Idris 2 closer to being production ready on a serverless scenario.

What we get by running Idris 2 Functions in serverless:

• A considerable amount of web stack plumbing requirements is removed by running your Idris 2 programs in serverless.

• We can opt-in to use Idris 2 when it’s viable, and use other language when it’s not.

• Less need for tests. When an Idris 2 program compiles, there is a very high chance it will work as intended. This may be especially important when faced with setting up different test suites for different languages. What usually happens is for teams to choose a single language to use in their serverless project.

Remaining issues:

• Writing FFI bindings for libraries from other languages that you wish to use.

• Not a lot of code examples in stackoverflow, but sometimes ChatGPT can help.

• Code generator may not live to your expectations.

Apple Silicon support

I will not focus on supporting Apple Silicon Docker image. Someone might find useful the following information from the Idris 2 documentation:

The official version of chez scheme does not yet support Apple Silicon. So, on macOS with Apple Silicon (e.g. M1 and M2 macs), you will need to build and install the Racket fork of chez scheme.

Install Chez Scheme on Apple Silicon:

git clone [email protected]:racket/ChezScheme.git
cd ChezScheme
git submodule init
git submodule update
arch=tarm64osx
./configure --pb
make ${arch}.bootquick
./configure --threads
make
sudo make install

Tests

Tests run in CI with Github Actions. Some commands can be found in a Github Actions workflow to help you with testing your changes before pushing them to a topic branch.

Contributing

Contributions are welcome! If you find a bug or have an idea for a new feature, please open an issue or submit a pull request.

License

Copyright (c) 2023 Carlos da Cunha Fontes

The MIT License