No longer yellow, for your satisfaction [Re: [Agda] some yellow, for your amusement]

[Conor McBride]

On 27 Mar 2012, at 22:04, Andreas Abel wrote:

> Proud to announce that this shade of yellow has disappeared...

APPLAUSE!

Conor

> 
> Andreas
> 
> On Fri, 25 Jul 2008 11:24:23 +0100, Conor McBride wrote:
>> 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) ) ) )  ]
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> -- 
> Andreas Abel  <><     Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda