Skip to content

Instantly share code, notes, and snippets.

@copumpkin
Last active October 2, 2015 07:38
Show Gist options
  • Save copumpkin/2203139 to your computer and use it in GitHub Desktop.
Save copumpkin/2203139 to your computer and use it in GitHub Desktop.
Routing
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!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment