[Agda] some yellow, for your amusement

[Conor McBride]

Dear friends

I append some comical scribblings that I dreamt up down the
pub and typed in this morning. Nothing to get excited about:
the kit all typechecks but the example at the end doesn't.

I think it's a bunch of unsolved constraints that are holding
things up. More particularly, I suspect that

   f (x , y) = t

is not being solved (for f) in situations where

   f x y = t

would be. Is that the trouble? If so, one possibly cheap,
possibly nasty fix is to solve a metavariable which is
functional over a record with another which is functional
over the individual fields. That way, the former reduces
to the latter without any weird poking about inside the
unification algorithm.

A more principled solution, also incorporating patterns
for records, may be worth seeking.

Just a passing thought...

Cheers

Conor

--------------------------------------------------------


module Shad where

data Nat : Set where
   zero : Nat
   suc : Nat -> Nat

nrec : (P : Nat -> Set)(mz : P zero)(ms : (n : Nat) -> P n -> P (suc n))
       (n : Nat) -> P n
nrec P mz ms zero     = mz
nrec P mz ms (suc n)  = ms n (nrec P mz ms n)

data One : Set where
   void : One

record _*_ (S : Set)(T : S -> Set) : Set where
  field
   fst : S
   snd : T fst

open module Sig' {S : Set}{T : S -> Set} = _*_ {S} {T}

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> S * T
s , t = record {fst = s; snd = t}

_>_ : (S : Set)(T : S -> Set) -> Set
S > T = (s : S) -> T s

infixr 40 _*_

mutual
   data Ctxt : Set -> Set1 where
     E : Ctxt One
     _<_ : {G : Set}{S : G -> Set} -> Ctxt G -> Type G S -> Ctxt (G * S)

   data Type : (G : Set) -> (G -> Set) -> Set1 where
     nat : {G : Set} -> Type G (\_ -> Nat)
     pi  : {G : Set}{S : G -> Set}{T : (G * S) -> Set} ->
           Type G S -> Type (G * S) T -> Type G (\g -> (x : S g) -> T  
(g , x))

data Var :  (G : Set)(T : G -> Set) -> ((g : G) -> T g) -> Set1 where
   top : {G : Set}{S : G -> Set} ->
         Var (G * S) (\gs -> S (fst gs)) snd
   pop : {G : Set}{S T : G -> Set}{x : (g : G) -> T g} ->
         Var G T x -> Var (G * S) (\gs -> T (fst gs)) (\gs -> x (fst  
gs))

data Term : (G : Set)(T : G -> Set) -> ((g : G) -> T g) -> Set1 where
   ze : {G : Set} -> Term G (\_ -> Nat) (\_ -> zero)
   su : {G : Set}{n : G -> Nat} -> Term G (\_ -> Nat) n ->
           Term G (\_ -> Nat) (\g -> suc (n g))
   lam : {G : Set}{S : G -> Set}{T : (G * S) -> Set}
         {t : (g : G * S) -> T g} ->
         Term (G * S) T t ->
         Term G (\g -> (x : S g) -> T (g , x))
                (\g x -> t (g , x))
   var : {G : Set}{T : G -> Set}{x : (g : G) -> T g} ->
         Var G T x -> Term G T x
   app : {G : Set}{S : G -> Set}{T : (G * S) -> Set}
         {f : (g : G) -> (s : S g) -> T (g , s)}
         {s : (g : G) -> S g} ->
         Term G (\g -> (s : S g) -> T (g , s)) f -> Term G S s ->
         Term G (\g -> T (g , s g)) (\g -> f g (s g))
   rec : {G : Set}{P : (G * \_ -> Nat) -> Set}
         {mz : (g : G) -> P (g , zero)}
         {ms : (g : G) -> (n : Nat) -> P (g , n) -> P (g , suc n)}
         {n : G -> Nat} ->
         Type (G * \_ -> Nat) P ->
         Term G (\g -> P (g , zero)) mz ->
         Term G (\g -> (n : Nat) -> P (g , n) -> P (g , suc n)) ms ->
         Term G (\g -> Nat) n ->
         Term G (\g -> P (g , n g)) \g ->
           nrec (\n -> P (g , n)) (mz g) (ms g) (n g)

data TERM {G : Set}{T : G -> Set}(G' : Ctxt G)(T' : Type G T) : Set1  
where
   [_] : {t : (g : G) -> T g} -> Term G T t -> TERM G' T'


plus : {G : Set}{G' : Ctxt G} -> TERM G' (pi nat (pi nat nat))
plus =  [ lam (lam (rec nat  (var top ) (lam (lam (su (var top) ) ) )  
(var (pop top) ) ) )  ]