problem.agda

--------------------------------------------------------------------------------
---------------------------------- THE SETUP -----------------------------------
--------------------------------------------------------------------------------

-- I like Agda's instance arguments, but I have a problematic use-case; it seems
-- like they'd be good for it, but I get an unexpected ambiguity.

open import Level
open import Data.Product

Rel : ∀{i} -> Set i -> Set _
Rel A = A -> A -> Set

record Trans {i} (A : Set i) (R : Rel A) : Set i where
  field _•_ : ∀{a b c} -> R a b -> R b c -> R a c

open Trans {{...}} public

-- Transitive graphs.
record TG i : Set (suc i) where
  field node : Set i
  field edge : (a b : node) -> Set
  field isTrans : Trans node edge

open TG public

instance
  -- This basically says: "a transitive graph is transitive".
  auto-transitive : ∀{i} {{G : TG i}} -> Trans (node G) (edge G)
  auto-transitive {{G}} = isTrans G


--------------------------------------------------------------------------------
--------------------------------- THE PROBLEM ----------------------------------
--------------------------------------------------------------------------------
pointwise : ∀{A B : Set} -> Rel B -> Rel (A -> B)
pointwise R f g = ∀ x -> R (f x) (g x)

trans:pointwise : ∀{A B R} -> Trans B R -> Trans (A -> B) (pointwise R)
_•_ {{trans:pointwise P}} aRb bRc x = aRb x • bRc x

-- But trans:pointwise doesn't typecheck! The culprit is auto-transitive; if I
-- comment out auto-transitive, this works. But I don't really understand why.

-- I can fix this specific case, of course:

-- _•_ {{trans:pointwise P}} aRb bRc x = _•_ {{P}} (aRb x) (bRc x)

-- But the presence of auto-transitive makes *any* attempt to use _•_ when a
-- variable of type (Trans _ _) is in scope require disambiguation, which
-- defeats the purpose of _•_ as an instance function.


--------------------------------------------------------------------------------
--------------------- WHY NOT JUST REMOVE auto-transitive? ---------------------
--------------------------------------------------------------------------------
-- Here's an example where auto-transitive is quite useful: the product of
-- transitive graphs.
tg× : ∀{i j} -> TG i -> TG j -> TG (i ⊔ j)
node (tg× G H) = node G × node H
edge (tg× G H) (a , x) (b , y) = edge G a b × edge H x y
-- Here's where we use auto-transitive. (Try commenting out auto-transitive.)
_•_ {{isTrans (tg× G H)}} (f₁ , f₂) (g₁ , g₂) = f₁ • g₁ , f₂ • g₂


--------------------------------------------------------------------------------
-------------------------- MORE STUFF _•_ IS GOOD FOR --------------------------
--------------------------------------------------------------------------------

---------- 1. Composing functions ----------
instance
  funcs : TG (suc zero)
  node funcs = Set
  edge funcs a b = a -> b
  _•_ {{isTrans funcs}} f g x = g (f x)

_∘_ : ∀{A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
_∘_ f g = g • f

---------- 2. Proofs by transitivity ----------
open import Data.Nat hiding (zero; suc; _⊔_)
instance
  nats : TG zero
  node nats = ℕ
  edge nats = _≤_
  _•_ {{isTrans nats}} = DecTotalOrder.trans decTotalOrder
    where open import Relation.Binary

-- Now we can use _•_ for proofs by transitivity of _≤_ on ℕ.
foo : 2 ≤ 4
foo = duh • duh'
  where duh : 2 ≤ 3; duh = s≤s (s≤s z≤n)
        duh' : 3 ≤ 4; duh' = s≤s (s≤s (s≤s z≤n))