Routing

Routing.agda

module Routing where

open import Function hiding (type-signature)

open import Data.Bool hiding (_≟_)
open import Data.Maybe
open import Data.Char hiding (_≟_)
open import Data.String as String
open import Data.List as List hiding ([_])
open import Data.Product hiding (curry; uncurry)

open import Data.Unit hiding (decTotalOrder; _≤_; _≟_)
open import Data.Nat hiding (_≟_)
open import Data.Fin hiding (_<_; _≤_)
open import Data.Vec hiding ([_]; _∈_)

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- A type tagged with a String name, just because I can
record _∶_ (name : String) (A : Set) : Set where
  constructor inj
  field
    proj : A

open _∶_

-- I don't care about parsing details, but I'll probably slot in NAD's Total Parser Combinators at some point
module Parsers where
  postulate Parser : Set → Set

  postulate _∈_ : ∀ {A} → String → Parser A → Set

  postulate parse : ∀ {A} (p : Parser A) (s : String) → Dec (s ∈ p)

  postulate get : ∀ {A} {p : Parser A} {s} → s ∈ p → A
  
  -- Hah!
  postulate ∈-unique : ∀ {A s} {p : Parser A} (x y : s ∈ p) → x ≡ y

  postulate nat : Parser ℕ
  postulate string : Parser String
  postulate vec : ∀ {A} → Parser A → (n : ℕ) → Parser (Vec A n)
  
open Parsers


infixl 6 _▻_

record Empty : Set where
  constructor ε

mutual
  -- This telescopey thing is probably the most general list-like container possible.
  -- For intuition of how this works, think of how a heterogeneous list generalizes
  -- a non-dependent pair. A Telescope generalizes a dependent pair in a similar way,
  -- by letting types further down the list depend on the value at the head.
  -- This needs to be left-nested for the types to make sense, but that makes it rather uncomfortable for other purposes.
  data Telescope : Set₁ where
    ε   : Telescope
    _▻_ : (xs : Telescope) (x : ⟦ xs ⟧ → Set) → Telescope

  -- An interpretation function of the telescope, letting us create very dependent values (a bunch of nested sigmas)
  -- This is the recursive side of induction-recursion. I'd prefer it to be induction-induction
  -- but Agda isn't clever enough to figure that out yet.
  ⟦_⟧ : Telescope → Set
  ⟦ ε ⟧ = Empty
  ⟦ xs ▻ x ⟧ = Sigma xs x

  -- Just for the sake of having prettier patterns
  record Sigma (xs : Telescope) (x : ⟦ xs ⟧ → Set) : Set where
    constructor _▻_
    field
      fst : ⟦ xs ⟧
      snd : x fst

-- A telescope is an n-ary dependent tuple, so we can curry it just like a regular tuple into an n-ary dependent function
Curried : ∀ t → (⟦ t ⟧ → Set) → Set
Curried ε R = R ε
Curried (xs ▻ x) R = Curried xs (λ q → ∀ r → R (q ▻ r))

-- Transform an uncurried function into a curried one
curry : ∀ {t} (R : ⟦ t ⟧ → Set) → ((v : ⟦ t ⟧) → R v) → Curried t R
curry {ε} R f = f ε
curry {xs ▻ x} R f = curry {xs} _ (λ v r → f (v ▻ r))

-- And back again
uncurry : ∀ {t} (R : ⟦ t ⟧ → Set) → Curried t R → ((v : ⟦ t ⟧) → R v)
uncurry {ε} R c v = c
uncurry {xs ▻ x} R c (vs ▻ v) = uncurry {xs} _ c vs v

-- Sometimes you just want a simple list of types.
-- For example, ⟦ Simple (Bool ∷ ℕ ∷ String ∷ []) ⟧ is just a heterogeneous list
Simple : List Set → Telescope
Simple = List.foldl (λ xs x → xs ▻ const x) ε

infixl 6 _/_ _//_ _//′_

-- A route is an annotated telescope. _/_ is for static path components and _//_ is for parameter parser components
data Route : Telescope → Set₁ where
  ε    : Route ε
  _/_  : ∀ {xs} (rs : Route xs) (k : String) → Route xs
  _//_ : ∀ {xs x} (rs : Route xs) (r : ((q : ⟦ xs ⟧) → Parser (x q)) × String) → Route (xs ▻ x)

-- If you don't want a dependent path component (probably most of the time)
_//′_ : ∀ {xs A} → Route xs → (Parser A × String) → Route (xs ▻ const A)
rs //′ (p , s) = rs // (const p , s)

-- Propagate the annotated parameter parser names into the telescope so we get named arguments
mutual
  Named : ∀ {t} → Route t → Telescope
  Named ε = ε
  Named (rs / k) = Named rs
  Named (_//_ {x = x} rs (p , s)) = Named rs ▻ (λ q → s ∶ x (extract-Named q))

  extract-Named : ∀ {t} {r : Route t} → ⟦ Named r ⟧ → ⟦ t ⟧
  extract-Named {r = ε} v = v
  extract-Named {r = rs / k} v = extract-Named {r = rs} v
  extract-Named {r = rs // r} (vs ▻ v) = extract-Named {r = rs} vs ▻ proj v

-- This type is only inhabited if the list of path components (backwards, due to the inherent left-nesting of telescopes) matches the route
mutual
  data Match : ∀ {t} → Route t → List String → Set₁ where
    ε    : Match ε []
    _/_  : ∀ {ss xs} {rs : Route xs} (ms : Match rs ss) (s : String) → Match (rs / s) (s ∷ ss)
    _//_ : ∀ {ss s xs} {x : ⟦ xs ⟧ → Set} {rs : Route xs} {r : ((q : ⟦ xs ⟧) → Parser (x q)) × String} (ms : Match rs ss) (m : s ∈ proj₁ r (payload ms)) → Match (rs // r) (s ∷ ss)

  -- If we have a match, we can pull out the actual data
  payload : ∀ {t ss} {r : Route t} → Match r ss → ⟦ t ⟧
  payload ε = ε
  payload (ms / s) = payload ms
  payload (ms // m) = payload ms ▻ get m

-- Simple lemma
Match-equal : ∀ {t k ss s} {rs : Route t} → Match (rs / k) (s ∷ ss) → k ≡ s
Match-equal (ms / ._) = refl

-- All matches are unique
Match-unique : ∀ {t ss} {r : Route t} (x y : Match r ss) → x ≡ y
Match-unique ε ε = refl
Match-unique (ms / s) (ms′ / .s) rewrite Match-unique ms ms′ = refl
Match-unique (ms // m) (ms′ // m′) rewrite Match-unique ms ms′ | ∈-unique m m′ = refl

-- Decision procedure to see if the given list of path components (backwards) matches the route
match : ∀ {t} (r : Route t) (s : List String) → Dec (Match r s)
match ε [] = yes ε
match ε (x ∷ xs) = no (λ ())
match (rs / k) [] = no (λ ())
match (rs / k) (x ∷ xs) with k ≟ x
match (rs / k) (x ∷ xs)  | yes p with match rs xs
match (rs / k) (.k ∷ xs) | yes refl | yes q = yes (q / k)
match (rs / k) (.k ∷ xs) | yes refl | no ¬q = no (λ { (ms / .k)  → ¬q ms })
match (rs / k) (x ∷ xs)  | no ¬p = no (λ q → ¬p (Match-equal q))
match (rs // r) [] = no (λ ())
match (rs // r) (x ∷ xs) with match rs xs
match (rs // r) (x ∷ xs) | yes p with parse (proj₁ r (payload p)) x
match (rs // r) (x ∷ xs) | yes p | yes q = yes (p // q)
match (rs // r) (x ∷ xs) | yes p | no ¬q = no (λ { (ms // m) → ¬q (subst (λ q → x ∈ proj₁ r (payload q)) (Match-unique ms p) m) })
match (rs // r) (x ∷ xs) | no ¬p = no (λ { (ms // m) → ¬p ms })

-- A few HTTP methods
module Http where
  data Method : Set where
    HEAD GET POST PUT DELETE OPTIONS : Method

-- We might eventually specify what kind of state modifications different methods are allowed to make
postulate Handler : Http.Method → Set

-- The actual route stores the method (or maybe multiple ones, someday), a route, and a handler function
record RouteSpec : Set₁ where
  constructor rs
  field
    m   : Http.Method
    {t} : Telescope
    r   : Route t
    -- Should we let the method of the Handler depend on its arguments? :P
    -- for example: /foo/5/bar can accept PUT but /foo/4/bar can accept GET
    h   : Curried (Named r) (const (Handler m)) 


Routes = List RouteSpec



module Examples where
  -- A dependent route. Would accept (assuming correct parsers):
  -- "/foo/5/bar/[1,2,3,4,5]"
  -- "/foo/4/bar/[5,25,1,4]"
  -- but would reject:
  -- "/foo/5/bar/[1,2,3,4]"
  r : Route (ε ▻ (λ { ε → ℕ }) ▻ (λ { (ε ▻ n) → Vec ℕ n }))
  r = ε / "foo" //′ (nat , "foo_id") / "bar" // ((λ { (ε ▻ n) → vec nat n }) , "bar_id")

  -- If you only use non-dependent components, the type can be "inferred"!
  s = ε / "bar" //′ (nat , "bar_id") / "mooooo" //′ (string , "mooooo_id")

  -- What a handler might look like
  foo_handler : (n : "foo_id" ∶ ℕ) → ("bar_id" ∶ Vec ℕ (proj n)) → Handler Http.GET
  foo_handler (inj foo_id) (inj bar_id) = {!!}

  bar_handler : ("bar_id" ∶ ℕ) → ("mooooo_id" ∶ String) → Handler Http.PUT
  bar_handler (inj bar_id) (inj mooooo_id) = {!!}

  -- List of handlers
  routes : Routes
  routes
    = rs Http.GET r foo_handler
    ∷ rs Http.PUT s bar_handler
    ∷ []

-- More to come later, including efficient route lookup!