HOME | EDIT | RSS | ABOUT | GITHUB

Type-Driven Development with PureScript

Type-Driven Development with Idris is a good book, but it's not actually very practical in industry.

In industry, Scala is wild adopted as Functional Programming language because it can benefit from both Scala community and Java community.

On the other hand, PureScript is more likely the best language in front-end that play the duel role of Scala in back-end, because it can benefit from both PureScript community and JavaScript community.

Further more PureScript supports Typed Holes, which is an powerful feature that you can Type-Driven your application.

Let us start from Type and drive an simple Todo MVC app.

There are 3 steps in Type-Driven Development.

decide how to continue the process.

line of a definition or breaking it down into smaller components.

type more precise.

Prerequisites

curl https://nixos.org/nix/install | sh
nix-shell
yarn
bower i

Please keep following command handy:

  1. Compile and watch purescript yarn purs-build-w
  2. Link PureScript output file(Only need to do this once) yarn purs-link
  3. Start PureSCript IDE Server yarn purs-ied
  4. Start Dev server and compile JSX files yarn start

User should be able to view a list of Todos

To model the problem accurately, we need to know what behavior of Todo app would expected.

Assuming we already have our restful back end developed.

If you visit: https://jsonplaceholder.typicode.com/todos/

It returns data in such JSON format:

[
  {
    "userId": 1,
    "id": 1,
    "title": "delectus aut autem",
    "completed": false
  },
  {
    "userId": 1,
    "id": 2,
    "title": "quis ut nam facilis et officia qui",
    "completed": false
  }
]

Ok, so this will clearly be the Data Type we need.

Type

module Data.Todo where

type Todo = {
  userId:: Int,
  id:: Int,
  title:: String,
  completed:: Boolean
}

type Todos = Array Todo

To initiating the behavior, the data need to be load from remote server at the first place.

Since all JavaScript request will be async, Effect.Aff would be the best type to describe such behavior. I supposed we need to specify a Path so that we know where to load the data from.

module Behavior.Load where
import Effect.Aff
import Data.Todo
import Prelude

type Path = String
load :: Path -> Aff (Array Todo)

Here is the type we need that can describe our behavior very accurate:

providing the Path, we should able to get an Asynchronous Effect that eventually has value of Array of Todo

Now we have a decent type, let us "Define" it, by pressing C-c C-a

Define

module Behavior.Load where
import Effect.Aff
import Data.Todo
import Prelude

type Path = String
load :: Path -> Aff (Array Todo)
load _ = ?load

Oh, compiler generate an function definition for us, let us hover the cursor on that question mark ?load thing

  Hole 'load' has the inferred type

    Aff
      (Array
         { completed :: Boolean
         , id :: Int
         , title :: String
         , userId :: Int
         }
      )

  You could substitute the hole with one of these values:

    Control.Plus.empty  :: forall a f. Plus f => f a
    Data.Monoid.mempty  :: forall m. Monoid m => m
    Effect.Aff.never    :: forall a. Aff a


in value declaration load
 [HoleInferredType]

Mmm…very clear, compiler is guessing the implementation could be one of:

  • Control.Plus.empty
  • Data.Monoid.mempty
  • Effect.Aff.never

But which one should I use?

Let's try all of them, replace ?load with empty

module Behavior.Load where
import Effect.Aff
import Data.Todo
import Prelude

type Path = String
load :: Path -> Aff (Array Todo)
load _ = empty

C-c C-i editor will ask you which Module to import from? Tell it Control.Plus

module Behavior.Load where

import Data.Todo
import Effect.Aff
import Prelude

import Control.Plus (empty)

type Path = String
load :: Path -> Aff (Array Todo)
load _ = empty

Oh my… it compiled. We just did it.

TODO But Why?

Why Control.Plus.empty works?

Actually all of them work.

Refine

So, if we run it, what will happen?

> runAff_ (\x -> log (show x)) $ load "asdf"
(Left Error: Always fails
    at Object.exports.error (/home/jcouyang/Documents/blog/org/purescript/type-driven-development-with-purescript/.psci_modules/node_modules/Effect.Exception/foreign.js:8:10)
    at Object.<anonymous> (/home/jcouyang/Documents/blog/org/purescript/type-driven-development-with-purescript/.psci_modules/node_modules/Effect.Aff/index.js:417:73)
    at Module._compile (internal/modules/cjs/loader.js:776:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:787:10)
    at Module.load (internal/modules/cjs/loader.js:653:32)
    at tryModuleLoad (internal/modules/cjs/loader.js:593:12)
    at Function.Module._load (internal/modules/cjs/loader.js:585:3)
    at Module.require (internal/modules/cjs/loader.js:690:17)
    at require (internal/modules/cjs/helpers.js:25:18)
    at Object.<anonymous> (/home/jcouyang/Documents/blog/org/purescript/type-driven-development-with-purescript/.psci_modules/node_modules/Behavior.Load/index.js:3:18))
unit

Ok, it resolve as Left Error

Seems we did not finish yet, we probably should be more specific about what should we do in defination

Maybe?

load path = ajax path

There are lot of implementation of making Ajax call for PureScript like Affjax, but I like to show how easy to make your own one by PureScript's FFI.

A little bit JavaScript to call window.fetch, to make it FFI, we need to name it the same Behavior.Load.js

function get(url) {
  return function(onError, onSuccess) {  
    window.fetch(url).then(function(res){
      return res.text()
    })
      .then(onSuccess)
      .catch(onError)
    return function(cancelError, cancelerError, cancelerSuccess) {
      cancelerSuccess()
    };
  }
}
exports._get = get

Type

Now you can foreign import the get function from JavaScript

import Effect.Aff.Compat (EffectFnAff(..))

foreign import _get :: Path -> EffectFnAff String

So the _get function can take a Path and return EffectFnAff String.

But String is not he value we need, what we need is Todos.

Then another layer of abstraction to provide us the domain type is needed.

Just call it ajaxGet for now.

import Data.Either (Either)
import Simple.JSON (class ReadForeign)

ajaxGet :: forall a. ReadForeign a => Path -> Aff (Either Error a)
ajaxGet _ = ?ajaxGet

Type of ajaxGet can read as "given type a which has instance of ReadForeign a, input a Path and it can return an Aff of Either Error a".

Define

C-c C-a compiler will define ajaxGet _ = ?ajaxGet

Move cursor to ?ajaxGet and…

  Hole 'ajaxGet' has the inferred type

    Aff (Either Error a0)

  You could substitute the hole with one of these values:

    Control.Plus.empty  :: forall a f. Plus f => f a
    Effect.Aff.never    :: forall a. Aff a


in value declaration ajaxGet

where a0 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)
 [HoleInferredType]

Hmm, clearly we don't want an empty, look what we have currently

_get :: Path -> EffectFnAff String -- FFI
fromEffectFnAff :: forall a. EffectFnAff a -> Aff a -- from Effect.Aff.Compat
readJSON :: forall a. ReadForeign a => String -> Either MultipleErrors a -- from Simple.JSON

Refine

It's like solve puzzles, return type of _get match fromEffectFnAff input type. Let us we compose, see what we got

ajaxGet :: forall a. ReadForeign a => Path -> Aff (Either Error a)
ajaxGet path = ?toJSON $ fromEffectFnAff (_get path)

Move cursor to ?toJSON see what we need to put in here now.

Hole 'toJson' has the inferred type

  Aff String -> Aff (Either Error a0)

Great, we have

readJSON :: forall a. ReadForeign a => String -> Either MultipleErrors a

which is pretty similar though…

How can we get rid of the high kind Aff?

If we lift String -> Either Error a to Aff level, we should able to get Aff String -> Aff (Either Error a).

That is exactly <> does, put a <> around $ and it will lift the left hand side

ajaxGet :: forall a. ReadForeign a => Path -> Aff (Either Error a)
ajaxGet path = ?toJSON <$> fromEffectFnAff (_get path)

Now compiler says:

Hole 'toJson' has the inferred type

  String -> Either Error a0

Refine

So close, now just need Either MutipleErrors a -> Either Error a, isn't that exactly type signature of lmap?

ajaxGet path = (lmap ?adaptError <<< parseJSON )<$> fromEffectFnAff (_get path)
  where
    parseJSON :: String -> Either MultipleErrors a
    parseJSON = readJSON
Hole 'adaptError' has the inferred type

  NonEmptyList ForeignError -> Error

Seems to be a very easy function to implement, finally!

Define

ajaxGet path = (lmap adaptError <<< parseJSON )<$> fromEffectFnAff (_get path)
  where
    parseJSON :: String -> Either MultipleErrors a
    parseJSON = readJSON
    adaptError :: MultipleErrors -> Error
    adaptError = error <<< show

Without single line of test, and run time red-green. We just follow the compiler's hint, compose different pieces of type together and then form the type that just fit our domain problem. And the most amazing part is even without unit tested, I'm very confident that compiler already proven type is work, the code driven from type should be working fine too.

However, I'm not saying we should not write any unit test, the part FFI calling the JavaScript function can not be proven by compiler that it is working.

Type

Now that we have ajaxGet, we can replace empty in load with the real ajax call function.

load :: Path -> Aff (Array Todo)
load path = do
  resp <- ?ajaxGetTodos path
  ?doSomethingAbout resp
Hole 'ajaxGetTodos' has the inferred type

  String -> Aff t0

Define

That is ajaxGet, let us put that in

load :: Path -> Aff (Array Todo)
load path = do
  resp <- ajaxGetTodos path
  ?doSomethingAbout resp
  where
    ajaxGetTodos :: Path -> Aff (Either Error (Array Todo))
    ajaxGetTodos = ajaxGet

Type

Now what is ?doSomethingAbout

Hole 'doSomethingAbout' has the inferred type

  Either Error
    (Array
       { completed :: Boolean
       , id :: Int
       , title :: String
       , userId :: Int
       }
    )
  -> Aff
       (Array
          { completed :: Boolean
          , id :: Int
          , title :: String
          , userId :: Int
          }
       )

I think we need a liftEither :: forall a. Either Error a -> Aff a, let us define it

load :: Path -> Aff (Array Todo)
load path = do
    resp <- ajaxGetTodos path
    liftEither resp
    where
      ajaxGetTodos :: Path -> Aff (Either Error (Array Todo))
      ajaxGetTodos = ajaxGet
      liftEither :: forall a. Either Error a -> Aff a
      liftEither _ = ?liftEither

Define

C-c C-c on _, compiler will prompt you what type you what to split.

Tell it Either

liftEither :: forall a. Either Error a -> Aff a
liftEither (Left _) = ?liftEither
liftEither (Right _) = ?liftEither

Now it's all clear, ?liftEither is Aff a:

liftEither :: forall a. Either Error a -> Aff a
liftEither (Left e) = throwError e
liftEither (Right v) = pure v

All feature of load function is done since compiler is very happy about it. But, we never rich the Refine yet.

TODO Refine

One thing that is able to refine is liftEither, maybe this is not the best time to refine, since only one place is using it. But it seems like it should be a typeclass not just a scoped function. Because it looks very generic.

class MonadAff m <= MonadEither m where
  liftEither :: Either Error ~> m

instance monadEitherAff :: MonadEither Aff where
  liftEither (Left e) = throwError e
  liftEither (Right v) = pure v

Final Version

module Behavior.Load where

import Data.Todo
import Effect.Aff
import Prelude

import Data.Bifunctor (lmap)
import Data.Either (Either(..))
import Effect.Aff.Class (class MonadAff)
import Effect.Aff.Compat (EffectFnAff(..), fromEffectFnAff)
import Foreign (MultipleErrors)
import Simple.JSON (class ReadForeign, readJSON)

type Path = String
foreign import _get :: Path -> EffectFnAff String

ajaxGet :: forall a. ReadForeign a => Path -> Aff (Either Error a)
ajaxGet path = (lmap adaptError <<< parseJSON ) <$> fromEffectFnAff (_get path)
  where
    parseJSON :: String -> Either MultipleErrors a
    parseJSON = readJSON
    adaptError :: MultipleErrors -> Error
    adaptError = error <<< show

load :: Path -> Aff (Array Todo)
load path = do
    resp <- ajaxGetTodos path
    liftEither resp
    where
      ajaxGetTodos :: Path -> Aff (Either Error (Array Todo))
      ajaxGetTodos = ajaxGet

type State = {
             todos:: Todos
             }
reloadPage :: State -> Aff State
reloadPage _ = do
  entities <- load("https://jsonplaceholder.typicode.com/todos")
  pure {todos: entities}

class MonadAff m <= MonadEither m where
  liftEither :: Either Error ~> m

instance monadEitherAff :: MonadEither Aff where
  liftEither (Left e) = throwError e
  liftEither (Right v) = pure v

User should be able to add new todo into list

Type

New story, similarly let us create a new file src/Behavior.Add.purs.

module Behavior.Add where

addTodo :: Todo -> State -> Aff State

C-c C-a

addTodo :: Todo -> State -> Aff State
addTodo _ _ = ?addTodo

Define

What should we do first? post it to the server? Let us find out.

addTodo todo state = do
  status <- ?ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  purs ?whatnext

ajaxPost :: forall a. Path -> a -> Aff Int
ajaxPost _ _ = ?ajaxPost

ajaxPost is very similar to ajaxGet

we rely on js to actually send out the ajax request

Define

foreign import _post :: Path -> String -> EffectFnAff Int

ajaxPost :: forall a. Path -> a -> Aff Int
ajaxPost path body = fromEffectFnAff (_post path $ ?toJSON body)
Hole 'toJSON' has the inferred type

  a0 -> String

Clearly it should be writeJSON from simple-json, but if you don't know what to put in there try https://pursuit.purescript.org/search?q=a+-%3E+String

Type

writeJSON :: forall a. WriteForeign a => a -> String

Hmm, a need to have Typeclass WriteForeign a instance. Again, don't worry the compile will give you the hint if you did not add the TypeClass bound

No type class instance was found for

  Simple.JSON.WriteForeign a1

All set!

ajaxPost :: forall a. WriteForeign a => Path -> a -> Aff Int
ajaxPost path body = fromEffectFnAff (_post path $ writeJSON body)

Now hover back to ?ajaxPost in addTodo see what happen.

Type

addTodo todo state = do
  status <- ?ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  pure ?whatnext
Hole 'ajaxPost' has the inferred type

  String
  -> { completed :: Boolean
     , id :: Int
     , title :: String
     , userId :: Int
     }
     -> Aff Int

You could substitute the hole with one of these values:

  Behavior.Add.ajaxPost             :: forall a. WriteForeign a => String -> a -> Aff Int
  Data.Variant.Internal.impossible  :: forall a. String -> a
  Partial.Unsafe.unsafeCrashWith    :: forall a. String -> a
  Record.Unsafe.unsafeGet           :: forall r a. String -> Record r -> a
  Unsafe.Coerce.unsafeCoerce        :: forall a b. a -> b

Awesome, compile say you could substitute it with Behavior.Add.ajaxPost

Simply remove the ?.

addTodo todo state = do
  status <- ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  pure ?whatnext

What next?

Hole 'whatnext' has the inferred type

  { todos :: Array
               { completed :: Boolean
               , id :: Int
               , title :: String
               , userId :: Int
               }
  }

Now we are clear, we can put an State there, but what exactly?

Recall our story, it is to post the todo, and based on the response of the request, we can do different things.

Define

addTodo todo state = do
  status <- ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  case status of
    201 -> pure ?success
    _ -> pure ?fail

Of cause ?fail should do nothing, or add some error indicator in State but we do not have that yet, so put it the same for now. Meanwhile what should put into ?success?

For user, the first todo should be updated to the one just added.

addTodo :: Todo -> State -> Aff State
addTodo todo state = do
  status <- ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  case status of
    201 -> pure $ state {todos = todo : state.todos}
    _ -> pure state

And.. do not forget implement the JavaScript FFI _post

function post(url) {
  return function(body) {
    return function(onError, onSuccess) {  
      window.fetch(url, {
        method: 'POST',
        headers: {
          'Content-Type': 'application/json'
        },
        body: body
      }).then(function(res){
        return res.status
      })
        .then(onSuccess)
        .catch(onError)
      return function(cancelError, cancelerError, cancelerSuccess) {
        cancelerSuccess()
      };
    }
  }
}
exports._post = post

The whole piece of Behavior.Add.

module Behavior.Add where

import Data.Array
import Data.Todo
import Effect.Aff
import Prelude

import Effect.Aff.Compat (EffectFnAff(..), fromEffectFnAff)
import Simple.JSON (class WriteForeign, writeJSON)

addTodo :: Todo -> State -> Aff State
addTodo todo state = do
  status <- ajaxPost "https://jsonplaceholder.typicode.com/todos" todo
  case status of
    201 -> pure $ state {todos = todo : state.todos}
    _ -> pure state

foreign import _post :: Path -> String -> EffectFnAff Int

ajaxPost :: forall a. WriteForeign a => Path -> a -> Aff Int
ajaxPost path body = fromEffectFnAff (_post path $ writeJSON body)

Exercise

Now you've got the idea, let us do the rest of the user stories and practice how to Type-Driven the implementation by thinking about Type first.