dyokomizo · March 26, 2012 11:39 · Mar 26, 2012
diff --git a/gistfile1.hs b/gistfile1.hs
@@ -0,0 +1,212 @@
+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!