No longer yellow, for your satisfaction [Re: [Agda] some yellow,
for your amusement]
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Mar 27 23:04:35 CEST 2012
Proud to announce that this shade of yellow has disappeared...
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/
More information about the Agda
mailing list