Writing Flutter apps in Idris

According to the Flutter team, UI=f(state), where f is a pure (mathematical) function. Let's have a look at the sample app provided by the team and see how it might be implemented in Idris 2 (henceforth Idris).

Idris is a purely functional language with dependent types. The main function might look like this:

total main : IO ()
main = do
    let page = makePage
                 "Page title"
                 (MkState "you have clicked the button this many times" 0)
                 pageBuilder
                 (Just $ MkFloatingAction IconAdd "add 1" floatingActionButtonOnPressed)
    let app = makeApp "App title" page
    runApp app

We first create the main page, then an App instance, and run the app.

The state of the app is represented by the following record:

record State where
    constructor MkState
    text : String
    count : Int

The page is built by a function (the f in the UI=f(state) equation):

total pageBuilder : Context -> State -> Center
pageBuilder context state =
    makeCenter $ makeColumn [
        MkSomeWidget $ makeText state.text,
        MkSomeWidget $ makeSizedBox 0 10 MkNoWidget,
        MkSomeWidget $ makeText $ show state.count
    ] MainAxisAlignmentCenter

There's also a floating action button whose functionality is defined by

total floatingActionButtonOnPressed : State -> Action State
floatingActionButtonOnPressed state = do
    let state = { count := state.count + 1 } state
    SetState state

And that's it. Note that the code is purely functional, only the main function returns a monad (IO ()).

Here's the complete code:

module Main

import Flutter

record State where
    constructor MkState
    text : String
    count : Int

total pageBuilder : Context -> State -> Center
pageBuilder context state =
    makeCenter $ makeColumn [
        MkSomeWidget $ makeText state.text,
        MkSomeWidget $ makeSizedBox 0 10 MkNoWidget,
        MkSomeWidget $ makeText $ show state.count
    ] MainAxisAlignmentCenter

total floatingActionButtonOnPressed : State -> Action State
floatingActionButtonOnPressed state = do
    let state = { count := state.count + 1 } state
    SetState state

total main : IO ()
main = do
    let page = makePage
                 "Page title"
                 (MkState "you have clicked the button this many times" 0)
                 pageBuilder
                 (Just $ MkFloatingAction IconAdd "add 1" floatingActionButtonOnPressed)
    let app = makeApp "App title" page
    runApp app

How does it all work? Idris is transpiled to Scheme which we in turn convert into Dart, the language Flutter uses. The FFI is quite straightforward and supports the async/await paradigm.