Safe web routes in PureScript

SafeWeb.purs

module SafeWeb where

import Prelude
import Data.Array (filter)
import Data.Leibniz (type (~))
import Data.String (Pattern(Pattern), split, joinWith)

type Path = Array String

pathToHtml :: Path -> String
pathToHtml = (<>) "/" <<< joinWith "/"

pathFromString :: String -> Path
pathFromString = filter ((/=) "") <<< split (Pattern "/")

data GET = GET
data POST = POST

data Route m = Route m Path

class Requestable r where
  toRoute :: forall m. r m -> Route m

type WithMethod m r = m -> (m ~ m) -> r m

a :: forall r. Requestable r =>
     WithMethod GET r
     -> String
a r =
  case toRoute (r GET id) of
    Route GET path ->
      "<a href=\""
      <> pathToHtml path
      <> "\"></a>"

form :: forall r. Requestable r =>
        WithMethod POST r
        -> String
form r =
  case toRoute (r POST id) of
    Route POST path ->
      "<form method=\"post\" action=\""
      <> pathToHtml path
      <> "\"></form>"

SafeWebSpec.purs

module SafeWebSpec where

import Prelude
import SafeWebSpec
import Data.Leibniz (type (~))
import SafeWeb (form, POST, GET, a, Route(Route), class Requestable)
import Test.Spec (Spec, it, describe)
import Test.Spec.Assertions (shouldEqual)

type Id = Int

type Project = { name :: String }

-- Here we create the routes in our application, and restrain
-- them to specific HTTP methods, using the Leibniz type equality
-- operator `~`. The framework takes care of providing `m` and the
-- proof `m ~ <METHOD>`.
data MyRoutes m
  = Home m (m ~ GET)
  | GetProjects Id m (m ~ GET)
  | SaveProject Project m (m ~ POST)

-- This part would be very nice to derive generically.
instance requestableMyRoutes :: Requestable MyRoutes where
  toRoute r =
    case r of
      Home m _ ->
        Route m ["about"]
      GetProjects id m _ ->
        Route m ["projects"]
      SaveProject project m _ ->
        Route m ["projects"]

spec :: forall e. Spec e Unit
spec = do
  describe "a" do
    it "produces an anchor tag for a GETable resource" do
      -- Here we create an anchor tag to GetProjects. We cannot pass
      -- this value to `form`.
      a (GetProjects 1) `shouldEqual` "<a href=\"/projects\"></a>"
  describe "form" do
    it "produces an form tag for a POSTable resource" do
      let project = { name : "SafeWeb" }
      -- Same safety here, we can pass `SafeProject project` to `form`, but not
      -- to `a`.
      form (SaveProject project)
        `shouldEqual`
        "<form method=\"post\" action=\"/projects\"></form>"

Things to consider:

• We are never using the proof in the Leibniz value, just demanding that it exists.
• The Requestable instance must be hand-written, and it's quite repetitive. Could perhaps be generically derived. The question there is how to handle the paths automatically?